Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_TensorProductDomain.lean

definition module

Tensor products of domains over an algebraically closed field

Throughout, K (respectively k) is an algebraically closed field. The module's single definition is IsAlgClosed.pointOfMaximal: for a commutative K-algebra A of finite type and a maximal ideal m \subseteq A, it is the K-algebra homomorphism A \to K obtained by composing the quotient map A \to A/m with the inverse of the structure map K \to A/m. That this structure map is bijective is the accompanying lemma IsAlgClosed.algebraMap_quotient_bijective, proved from the fact that a finite-type algebra over a field is a Jacobson ring, so that the residue field A/m is finite over K, hence equal to K by algebraic closedness; this is the Nullstellensatz in the form 'every maximal ideal of a finite-type K-algebra is the kernel of a K-point'. The companion IsAlgClosed.pointOfMaximal_eq_zero_iff records exactly that kernel description: \mathrm{pointOfMaximal}\,K\,m\,(a) = 0 if and only if a \in m.

The two substantive results are statements about tensor products. IsAlgClosed.isDomain_tensorProduct_of_finiteType asserts that if A is a commutative K-algebra which is of finite type and a domain, and B is any commutative K-algebra which is a domain, then A \otimes_K B is a domain; the argument writes elements of A \otimes_K B in coordinates with respect to a K-basis of B, tests the vanishing of products at the K-points \mathrm{pointOfMaximal}\,K\,m, and uses that A is Jacobson with zero Jacobson radical. IsAlgClosed.isDomain_tensorProduct_of_field drops the finiteness: for a field extension F of k and a commutative k-algebra B which is a domain, F \otimes_k B is a domain. Here the two given elements are written as finite sums of pure tensors, lifted to A \otimes_k B for the finitely generated subalgebra A \subseteq F generated by the F-components, the lift being injective by flatness of A \hookrightarrow F over the field k.

Relation to Mathlib

Mathlib supplies the nontriviality of such tensor products (Algebra.TensorProduct.nontrivial_of_algebraMap_injective_of_isDomain) and the Jacobson-ring input; the two domain statements and the K-point construction IsAlgClosed.pointOfMaximal are the project's own additions in the IsAlgClosed namespace.

Where it is used

These are commutative-algebra inputs for situations where a domain has to remain a domain after base change along a field extension of an algebraically closed base field, as when passing from an integral object to its base change in the geometric part of the argument.

References

  1. A. Grothendieck and J. Dieudonné, Éléments de géométrie algébrique IV, §4, Publ. Math. IHÉS 24 (1965)
  2. M. F. Atiyah and I. G. Macdonald, Introduction to Commutative Algebra, Addison-Wesley, 1969

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_TensorProductDomain.lean

Declarations

Source

import Mathlib.FieldTheory.IsAlgClosed.Basic ↗
import Mathlib.RingTheory.Jacobson.Ring ↗
import Mathlib.RingTheory.TensorProduct.Nontrivial ↗
import Mathlib.RingTheory.TensorProduct.Free ↗
import Mathlib.RingTheory.Flat.Basic ↗
import Mathlib.LinearAlgebra.TensorProduct.Finiteness ↗

universe u v w

open scoped TensorProduct

namespace IsAlgClosed

section FiniteType

variable {K : Type u} [Field K]

theorem algebraMap_quotient_bijective [IsAlgClosed K] {A : Type v} [CommRing A]
    [Algebra K A] [Algebra.FiniteType K A] (m : Ideal A) [m.IsMaximal] :
    Function.Bijective (algebraMap K (A ⧸ m)) := by
  letI : Field (A ⧸ m) := Ideal.Quotient.field m
  have : Module.Finite K (A ⧸ m) := finite_of_finite_type_of_isJacobsonRing K (A ⧸ m)
  have : Algebra.IsIntegral K (A ⧸ m) := inferInstance
  exact IsAlgClosed.algebraMap_bijective_of_isIntegral

variable (K) in

noncomputable def pointOfMaximal [IsAlgClosed K] {A : Type v} [CommRing A]
    [Algebra K A] [Algebra.FiniteType K A] (m : Ideal A) [m.IsMaximal] : A →ₐ[K] K :=
  let e := RingEquiv.ofBijective (algebraMap K (A ⧸ m)) (algebraMap_quotient_bijective m)
  { toRingHom := e.symm.toRingHom.comp (Ideal.Quotient.mk m)
    commutes' := fun k => by
      change e.symm (Ideal.Quotient.mk m (algebraMap K A k)) = k
      rw [Ideal.Quotient.mk_algebraMap]
      exact e.symm_apply_apply k }

theorem pointOfMaximal_eq_zero_iff [IsAlgClosed K] {A : Type v} [CommRing A] [Algebra K A]
    [Algebra.FiniteType K A] (m : Ideal A) [m.IsMaximal] (a : A) :
    pointOfMaximal K m a = 0 ↔ a ∈ m := by
  change (RingEquiv.ofBijective (algebraMap K (A ⧸ m))
    (algebraMap_quotient_bijective m)).symm (Ideal.Quotient.mk m a) = 0 ↔ a ∈ m
  rw [map_eq_zero_iff _ (RingEquiv.injective _), Ideal.Quotient.eq_zero_iff_mem]

theorem isDomain_tensorProduct_of_finiteType [IsAlgClosed K] (A : Type v) (B : Type w)
    [CommRing A] [Algebra K A] [Algebra.FiniteType K A] [IsDomain A]
    [CommRing B] [Algebra K B] [IsDomain B] :
    IsDomain (A ⊗[K] B) := by
  classical
  haveI : Nontrivial (A ⊗[K] B) :=
    Algebra.TensorProduct.nontrivial_of_algebraMap_injective_of_isDomain K A B
      (algebraMap K A).injective (algebraMap K B).injective

  let bB := Module.Free.chooseBasis K B
  let 𝔅 := Algebra.TensorProduct.basis A bB
  let I : A ⊗[K] B → Ideal A := fun x => Ideal.span (Set.range (𝔅.repr x))
  have hI : ∀ x, I x = ⊥ → x = 0 := by
    intro x hx
    apply 𝔅.repr.injective
    rw [map_zero]
    ext i
    exact (Ideal.span_eq_bot.mp hx) _ ⟨i, rfl⟩

  have hpt : ∀ (x y : A ⊗[K] B), x * y = 0 →
      ∀ (m : Ideal A) [m.IsMaximal], I x ≤ m ∨ I y ≤ m := by
    intro x y hxy m _
    let φ : A →ₐ[K] K := pointOfMaximal K m
    let ψ : A ⊗[K] B →ₐ[K] B :=
      Algebra.TensorProduct.lift ((Algebra.ofId K B).comp φ) (AlgHom.id K B)
        (fun _ _ => Commute.all _ _)
    have hψ : ∀ (z : A ⊗[K] B) (i), bB.repr (ψ z) i = φ (𝔅.repr z i) := by
      intro z i
      induction z using TensorProduct.induction_on with
      | zero => simp
      | tmul a b =>
        simp only [ψ, 𝔅, Algebra.TensorProduct.lift_tmul, AlgHom.coe_comp, Function.comp_apply,
          Algebra.ofId_apply, AlgHom.coe_id, id_eq, Algebra.TensorProduct.basis_repr_tmul,
          Finsupp.smul_apply, Finsupp.mapRange_apply, smul_eq_mul, map_mul, AlgHom.commutes]
        rw [← Algebra.smul_def, map_smul, Finsupp.smul_apply, smul_eq_mul, Algebra.algebraMap_self,
          RingHom.id_apply]
      | add z w hz hw => simp [map_add, hz, hw]
    have hker : ∀ z : A ⊗[K] B, ψ z = 0 → I z ≤ m := by
      intro z hz
      rw [Ideal.span_le]
      rintro _ ⟨i, rfl⟩
      rw [SetLike.mem_coe, ← pointOfMaximal_eq_zero_iff (K := K), ← hψ, hz, map_zero,
        Finsupp.zero_apply]
    have h0 : ψ x * ψ y = 0 := by rw [← map_mul, hxy, map_zero]
    rcases mul_eq_zero.mp h0 with h | h
    · exact Or.inl (hker x h)
    · exact Or.inr (hker y h)

  haveI : IsJacobsonRing A := isJacobsonRing_of_finiteType (A := K) (B := A)
  refine @NoZeroDivisors.to_isDomain _ _ _ ⟨fun {x y} hxy => ?_⟩
  have hle : I x * I y ≤ (⊥ : Ideal A) := by
    rw [← Ideal.radical_bot_of_noZeroDivisors, Ideal.radical_eq_jacobson]
    refine le_sInf ?_
    rintro J ⟨-, hJ⟩
    rcases hpt x y hxy J with h | h
    · exact Ideal.mul_le_left.trans h
    · exact Ideal.mul_le_right.trans h
  rcases (Ideal.mul_eq_bot.mp (le_bot_iff.mp hle)) with h | h
  · exact Or.inl (hI x h)
  · exact Or.inr (hI y h)

end FiniteType

section Fields

variable (k : Type u) [Field k] [IsAlgClosed k]

theorem isDomain_tensorProduct_of_field (F : Type v) (B : Type w) [Field F] [Algebra k F]
    [CommRing B] [Algebra k B] [IsDomain B] : IsDomain (F ⊗[k] B) := by
  classical
  haveI : Nontrivial (F ⊗[k] B) :=
    Algebra.TensorProduct.nontrivial_of_algebraMap_injective_of_isDomain k F B
      (algebraMap k F).injective (algebraMap k B).injective
  refine @NoZeroDivisors.to_isDomain _ _ _ ⟨fun {x y} hxy => ?_⟩
  obtain ⟨sx, hx⟩ := TensorProduct.exists_finset x
  obtain ⟨sy, hy⟩ := TensorProduct.exists_finset y

  let A : Subalgebra k F := Algebra.adjoin k ↑(sx.image Prod.fst ∪ sy.image Prod.fst)
  haveI : Algebra.FiniteType k A :=
    A.fg_iff_finiteType.mp ⟨sx.image Prod.fst ∪ sy.image Prod.fst, rfl⟩
  let ι : A ⊗[k] B →ₐ[k] F ⊗[k] B := Algebra.TensorProduct.map A.val (AlgHom.id k B)
  have hι : Function.Injective ι := by
    have h : Function.Injective (A.val.toLinearMap.rTensor B) :=
      Module.Flat.rTensor_preserves_injective_linearMap (M := B) A.val.toLinearMap
        Subtype.val_injective
    intro a b hab
    exact h hab
  have hlift : ∀ s : Finset (F × B), (∀ p ∈ s, p.1 ∈ A) →
      ∃ z : A ⊗[k] B, ι z = ∑ p ∈ s, p.1 ⊗ₜ[k] p.2 := by
    intro s hs
    refine ⟨∑ p ∈ s.attach, (⟨p.1.1, hs p.1 p.2⟩ : A) ⊗ₜ[k] p.1.2, ?_⟩
    rw [map_sum, ← Finset.sum_attach s]
    refine Finset.sum_congr rfl fun p _ => ?_
    simp [ι]
  have hxA : ∀ p ∈ sx, p.1 ∈ A := fun p hp =>
    Algebra.subset_adjoin (Finset.mem_coe.mpr
      (Finset.mem_union_left _ (Finset.mem_image_of_mem Prod.fst hp)))
  have hyA : ∀ p ∈ sy, p.1 ∈ A := fun p hp =>
    Algebra.subset_adjoin (Finset.mem_coe.mpr
      (Finset.mem_union_right _ (Finset.mem_image_of_mem Prod.fst hp)))
  obtain ⟨x', hx'⟩ := hlift sx hxA
  obtain ⟨y', hy'⟩ := hlift sy hyA
  rw [← hx] at hx'
  rw [← hy] at hy'
  subst hx' hy'
  haveI : IsDomain (A ⊗[k] B) := isDomain_tensorProduct_of_finiteType (K := k) A B
  have hxy' : x' * y' = 0 := hι (by rw [map_mul, hxy, map_zero])
  rcases mul_eq_zero.mp hxy' with h | h
  · exact Or.inl (by rw [h, map_zero])
  · exact Or.inr (by rw [h, map_zero])

end Fields

end IsAlgClosed

Statements phrased using this module (0)

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