Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_Mathlib_RingTheory_Localization_BaseChange.lean

definition moduleadapted from the Imperial College London FLT project: FLT/Mathlib/RingTheory/Localization/BaseChange.lean

Base change along a localization: tensor identifications and extensionality

Working over a commutative semiring R with a submonoid S and a localization A of R at S, this module supplies computational lemmas and two refinements of the canonical identifications for tensor products of modules over A. For an A-module M_1 that is also an R-module compatibly (an IsScalarTower R A M₁ assumption), moduleLid_symm_apply records that the inverse of the identification of A \otimes_R M_1 with M_1 sends m to 1 \otimes_R m; for a second such module M_2, map_moduleTensorEquiv_tmul and map_moduleTensorEquiv_symm_tmul record that the identification M_1 \otimes_A M_2 \cong M_1 \otimes_R M_2 (an isomorphism because A is a localization of R) and its inverse send m_1 \otimes m_2 to m_1 \otimes m_2 in either direction.

tensorProduct_ext is an extensionality principle in the following situation: S is a submonoid of a commutative semiring A, B an A-algebra, K a localization of A at S, and L a B-algebra which is simultaneously an A- and K-algebra with compatible scalars and which, as a B-module via the structure map B \to L, is the localization of B at (the image of) S. Then two K-linear maps L \otimes_K M \to P between K-modules that agree on all elements (\mathrm{algebraMap}\,x) \otimes_K y with x \in B, y \in M are equal, since every element of L becomes the image of an element of B after multiplication by a unit coming from S.

leftModuleTensorEquiv upgrades the identification M_1 \otimes_A M_2 \cong M_1 \otimes_R M_2 to an M'-linear equivalence, where M' is a semiring acting on the left factor M_1 so as to commute with the R- and A-actions; the M'-action on either tensor product is the one through M_1. Finally, leftModuleTensorEquiv_restrictScalars_eq states that, when M' is commutative and fits into algebra maps A \to M' \to R with the corresponding towers, restricting this equivalence to A-linear maps returns the underlying identification of A-modules.

Relation to Mathlib

These are additions to the setting of Mathlib's IsLocalization base-change file: the simp lemmas compute Mathlib's IsLocalization.moduleLid and IsLocalization.moduleTensorEquiv on pure tensors, and IsLocalization.leftModuleTensorEquiv is the latter equivalence promoted to linearity over a semiring acting on the left tensor factor.

References

  1. M. F. Atiyah and I. G. Macdonald, Introduction to Commutative Algebra, Addison-Wesley, 1969, ch. 3
  2. N. Bourbaki, Commutative Algebra, Chapters 1–7, Springer, 1989, ch. II

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_Mathlib_RingTheory_Localization_BaseChange.lean

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib

section

namespace IsLocalization

section

variable {R : Type*} [CommSemiring R] (S : Submonoid R)
  (A : Type*) [CommSemiring A] [Algebra R A] [IsLocalization S A]
  (M₁ : Type*) [AddCommMonoid M₁] [Module R M₁] [Module A M₁] [IsScalarTower R A M₁]

@[simp]
lemma moduleLid_symm_apply (m : M₁) : (moduleLid S A M₁).symm m = 1 ⊗ₜ[R] m := rfl

variable (M₂ : Type*) [AddCommMonoid M₂] [Module R M₂] [Module A M₂] [IsScalarTower R A M₂]

@[simp]
lemma map_moduleTensorEquiv_tmul (m₁ : M₁) (m₂ : M₂) :
    moduleTensorEquiv S A M₁ M₂ (m₁ ⊗ₜ[A] m₂) = m₁ ⊗ₜ[R] m₂ := rfl

@[simp]
lemma map_moduleTensorEquiv_symm_tmul (m₁ : M₁) (m₂ : M₂) :
    (moduleTensorEquiv S A M₁ M₂).symm (m₁ ⊗ₜ[R] m₂) = m₁ ⊗ₜ[A] m₂ := rfl

end

section

open TensorProduct

variable {A : Type*} [CommSemiring A] (S : Submonoid A)
  (B : Type*) [CommSemiring B] [Algebra A B]
  (K : Type*) [CommSemiring K] [Algebra A K] [IsLocalization S K]
  (L : Type*) [CommSemiring L] [Algebra B L] [Algebra A L] [Algebra K L] [IsScalarTower A B L]
    [IsScalarTower A K L] [IsLocalizedModule (M := B) (M' := L) S (Algebra.linearMap B L)]
  (M : Type*) [AddCommMonoid M] [Module K M]
  (P : Type*) [AddCommMonoid P] [Module K P]

include S in
theorem tensorProduct_ext {g h : L ⊗[K] M →ₗ[K] P}
    (H : ∀ (x : B) (y : M), g ((algebraMap _ L x) ⊗ₜ[K] y) = h ((algebraMap _ L x) ⊗ₜ[K] y))
    : g = h := by
  apply TensorProduct.ext'
  intro l m
  obtain ⟨⟨x, s⟩, hl : (s : A) • l = algebraMap B L x⟩ :=
    IsLocalizedModule.surj (M:=B) (M':=L) S (Algebra.linearMap B L) l
  rw [← IsUnit.smul_left_cancel <| map_units K s]
  simpa [← map_smul, TensorProduct.smul_tmul', IsScalarTower.algebraMap_smul K, hl] using H x m

@[simps!]
noncomputable def leftModuleTensorEquiv {R : Type*} (M' : Type*)
    [Semiring M'] [CommSemiring R] (S : Submonoid R) (A : Type*) [CommSemiring A] [Algebra R A]
    [IsLocalization S A] (M₁ : Type*) (M₂ : Type*) [AddCommMonoid M₁] [AddCommMonoid M₂]
    [Module M' M₁] [Module R M₁] [Module R M₂] [Module A M₁] [Module A M₂]
    [SMulCommClass A M' M₁] [SMulCommClass R M' M₁] [IsScalarTower R A M₁]
    [IsScalarTower R A M₂] :
    M₁ ⊗[A] M₂ ≃ₗ[M'] M₁ ⊗[R] M₂ where
  __ := IsLocalization.moduleTensorEquiv S A M₁ M₂
  map_smul' r x := by
    induction x with
    | zero => simp
    | tmul m₁ m₂ => simp [TensorProduct.smul_tmul']
    | add => simp_all

lemma leftModuleTensorEquiv_restrictScalars_eq {R M' : Type*} [CommSemiring M']
    [CommSemiring R] (S : Submonoid R) (A : Type*) [CommSemiring A] [Algebra R A] [Algebra A M']
    [Algebra M' R] [IsLocalization S A] (M₁ : Type*) (M₂ : Type*) [AddCommMonoid M₁]
    [AddCommMonoid M₂] [Module M' M₁] [Module R M₁] [Module R M₂] [Module A M₁]
    [Module A M₂] [IsScalarTower A M' M₁] [IsScalarTower M' R M₁] [IsScalarTower R A M₁]
    [IsScalarTower R A M₂] :
    (IsLocalization.leftModuleTensorEquiv M' S A M₁ M₂).restrictScalars A =
      IsLocalization.moduleTensorEquiv S A M₁ M₂ := by
  rfl

end

end IsLocalization

Statements phrased using this module (0)

No statement module imports it directly (it is used through other definition modules or by proofs).