Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_Mathlib_RingTheory_KmfloorsFiberPolynomialRegularAscent.lean

definition module

Regularity ascends to polynomial and multivariate polynomial rings

This module proves, entirely in terms of Mathlib's predicates IsRegularLocalRing and IsRegularRing, that regularity is stable under adjoining a polynomial variable. Three transport lemmas come first: if two prime ideals I=J of a commutative semiring A agree, then an A-algebra that is a localization at A\setminus I is one at A\setminus J; and for a prime J of a commutative ring A and an A-algebra S with S a localization of A at J^{\mathrm{c}}, regularity of S and of Localization.AtPrime J are equivalent (each direction stated separately).

The substantive chain concerns a prime P of R[X] and its contraction P\cap R (written P.under R). First, for a domain D and a prime Q of D[X] such that C d\in Q forces d=0, the local ring D[X]_Q is regular: D[X]_Q is a localization of \operatorname{Frac}(D)[X] at the prime generated by Q, where regularity of localizations of a polynomial ring over a field is available. Applying this to R[X]/(P\cap R)R[X]\cong (R/(P\cap R))[X] gives regularity of the localization at the image of P, provided that image is prime; consequently the quotient of R[X]_P by the ideal generated by the image of C(P\cap R) — the closed fibre of R_{P\cap R}\to R[X]_P — is a regular local ring. If R is a regular ring, then R[X] is free, hence flat, over R, the map R_{P\cap R}\to R[X]_P is a flat local homomorphism, and flat local ascent yields regularity of R[X]_P; since R[X] is Noetherian, R[X] is a regular ring.

Two corollaries follow: k[X_1,\dots,X_n] is a regular ring for a field k and every n, by induction on n, which together with smoothness of k\to k[X_1,\dots,X_n] gives the conjunction of Algebra.Smooth and regularity of all stalks; and \mathbb{Z}[X] is a regular ring.

Relation to Mathlib

All notions used are Mathlib's (IsRegularRing, IsRegularLocalRing, Localization.AtPrime, Ideal.under, Ideal.polynomialQuotientEquivQuotientPolynomial, Algebra.Smooth); nothing new is defined. The ascent step invoked, RegularFlatLocalAscent.isRegularLocalRing_of_flat_of_isRegularLocalRing_quotient (regularity of a flat local extension from regularity of its closed fibre), belongs to the project's own development.

Where it is used

These results supply the commutative-algebra input that polynomial algebras over a field or over \mathbb{Z} have regular local rings at all primes, which is the model case in the argument that a smooth algebra over a field has regular stalks (the predicate SmoothFieldFiberRegularStalksInput).

References

  1. H. Matsumura, Commutative Ring Theory, Cambridge Studies in Advanced Mathematics 8, Cambridge University Press, 1986, §19
  2. D. Eisenbud, Commutative Algebra with a View Toward Algebraic Geometry, Graduate Texts in Mathematics 150, Springer, 1995, Ch. 19

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_Mathlib_RingTheory_RegularLocalRingFlatLocalAscent
import Definitions.Def_Mathlib_RingTheory_SmoothFieldFiberRegularStalksStandardSmoothReduction

set_option autoImplicit false
set_option maxHeartbeats 800000
set_option synthInstance.maxHeartbeats 400000

universe u

open Polynomial

theorem kmf2_polyasc_isLocalization_primeCompl_congr {A : Type*} [CommSemiring A]
    {I J : Ideal A} [I.IsPrime] [J.IsPrime] (h : I = J)
    (S : Type*) [CommSemiring S] [Algebra A S]
    (hloc : IsLocalization I.primeCompl S) :
    IsLocalization J.primeCompl S := by
  subst h
  exact hloc

theorem kmf2_polyasc_isRegularLocalRing_of_isLocalization_primeCompl
    {A : Type*} [CommRing A] (J : Ideal A) [J.IsPrime]
    (S : Type*) [CommRing S] [Algebra A S]
    (h : IsLocalization J.primeCompl S)
    (hreg : IsRegularLocalRing (Localization.AtPrime J)) :
    IsRegularLocalRing S := by
  haveI := h
  haveI := hreg
  exact IsRegularLocalRing.of_ringEquiv (R := Localization.AtPrime J)
    (IsLocalization.algEquiv J.primeCompl (Localization.AtPrime J) S).toRingEquiv

theorem kmf2_polyasc_isRegularLocalRing_atPrime_of_isLocalization_primeCompl
    {A : Type*} [CommRing A] (J : Ideal A) [J.IsPrime]
    (S : Type*) [CommRing S] [Algebra A S]
    (h : IsLocalization J.primeCompl S)
    (hreg : IsRegularLocalRing S) :
    IsRegularLocalRing (Localization.AtPrime J) := by
  haveI := h
  haveI := hreg
  exact IsRegularLocalRing.of_ringEquiv (R := S)
    (IsLocalization.algEquiv J.primeCompl S (Localization.AtPrime J)).toRingEquiv

theorem kmf2_polyasc_isRegularLocalRing_localization_atPrime_of_comap_C_eq_bot
    (D : Type u) [CommRing D] [IsDomain D]
    (Q : Ideal (Polynomial D)) [Q.IsPrime]
    (hQ0 : ∀ d : D, Polynomial.C d ∈ Q → d = 0) :
    IsRegularLocalRing (Localization.AtPrime Q) := by
  letI : Algebra (Polynomial D) (Polynomial (FractionRing D)) :=
    Polynomial.algebra D (FractionRing D)
  haveI hloc : IsLocalization
      ((nonZeroDivisors D).map (Polynomial.C : D →+* Polynomial D))
      (Polynomial (FractionRing D)) :=
    Polynomial.isLocalization (nonZeroDivisors D) (FractionRing D)

  have hdisj : Disjoint
      (((nonZeroDivisors D).map (Polynomial.C : D →+* Polynomial D) : Submonoid (Polynomial D)) :
        Set (Polynomial D)) (Q : Set (Polynomial D)) := by
    rw [Set.disjoint_left]
    intro x hx hxQ
    obtain ⟨d, hd, rfl⟩ := Submonoid.mem_map.mp hx
    exact mem_nonZeroDivisors_iff_ne_zero.mp hd (hQ0 d hxQ)

  haveI hq'' : (Q.map (algebraMap (Polynomial D) (Polynomial (FractionRing D)))).IsPrime :=
    IsLocalization.isPrime_of_isPrime_disjoint
      ((nonZeroDivisors D).map (Polynomial.C : D →+* Polynomial D))
      (Polynomial (FractionRing D)) Q inferInstance hdisj
  have hcom : (Q.map (algebraMap (Polynomial D) (Polynomial (FractionRing D)))).comap
      (algebraMap (Polynomial D) (Polynomial (FractionRing D))) = Q :=
    IsLocalization.comap_map_of_isPrime_disjoint
      ((nonZeroDivisors D).map (Polynomial.C : D →+* Polynomial D))
      (Polynomial (FractionRing D)) inferInstance hdisj
  have htrans := IsLocalization.isLocalization_isLocalization_atPrime_isLocalization
      (M := (nonZeroDivisors D).map (Polynomial.C : D →+* Polynomial D))
      (T := Localization.AtPrime
        (Q.map (algebraMap (Polynomial D) (Polynomial (FractionRing D)))))
      (p := Q.map (algebraMap (Polynomial D) (Polynomial (FractionRing D))))
  have hQloc : IsLocalization Q.primeCompl
      (Localization.AtPrime
        (Q.map (algebraMap (Polynomial D) (Polynomial (FractionRing D))))) :=
    kmf2_polyasc_isLocalization_primeCompl_congr hcom
      (Localization.AtPrime
        (Q.map (algebraMap (Polynomial D) (Polynomial (FractionRing D))))) htrans

  have hregq : IsRegularLocalRing
      (Localization.AtPrime
        (Q.map (algebraMap (Polynomial D) (Polynomial (FractionRing D))))) :=
    kmf2_fiber_isRegularLocalRing_localization_atPrime_polynomial (FractionRing D) _
  exact kmf2_polyasc_isRegularLocalRing_atPrime_of_isLocalization_primeCompl Q
    (Localization.AtPrime
      (Q.map (algebraMap (Polynomial D) (Polynomial (FractionRing D)))))
    hQloc hregq

theorem kmf2_polyasc_isRegularLocalRing_localization_atPrime_fiberPrime
    (R : Type u) [CommRing R] (P : Ideal (Polynomial R)) [P.IsPrime]
    [hPbar : (P.map (Ideal.Quotient.mk (Ideal.map Polynomial.C (P.under R)))).IsPrime] :
    IsRegularLocalRing (Localization.AtPrime
      (P.map (Ideal.Quotient.mk (Ideal.map Polynomial.C (P.under R))))) := by
  have hIP : Ideal.map Polynomial.C (P.under R) ≤ P := by
    rw [Ideal.map_le_iff_le_comap, ← Polynomial.algebraMap_eq]

  haveI : IsRegularLocalRing (Localization.AtPrime
      ((P.map (Ideal.Quotient.mk (Ideal.map Polynomial.C (P.under R)))).comap
        (P.under R).polynomialQuotientEquivQuotientPolynomial)) := by
    apply kmf2_polyasc_isRegularLocalRing_localization_atPrime_of_comap_C_eq_bot
      (R ⧸ P.under R)
    intro d hd
    obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective d
    rw [Ideal.mem_comap,
      show (Polynomial.C ((Ideal.Quotient.mk (P.under R)) r)) =
        (Polynomial.C r).map (Ideal.Quotient.mk (P.under R)) from (Polynomial.map_C _).symm,
      Ideal.polynomialQuotientEquivQuotientPolynomial_map_mk] at hd
    obtain ⟨a, haP, hab⟩ :=
      (Ideal.mem_map_iff_of_surjective _ Ideal.Quotient.mk_surjective).mp hd
    have hsub : a - Polynomial.C r ∈ Ideal.map Polynomial.C (P.under R) :=
      (Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _).mp hab
    have hCrP : Polynomial.C r ∈ P := by
      have h2 := P.sub_mem haP (hIP hsub)
      rwa [sub_sub_cancel] at h2
    rw [Ideal.Quotient.eq_zero_iff_mem]
    show r ∈ P.under R
    rw [Ideal.mem_comap]
    rwa [Polynomial.algebraMap_eq]
  exact IsRegularLocalRing.of_ringEquiv
    (R := Localization.AtPrime
      ((P.map (Ideal.Quotient.mk (Ideal.map Polynomial.C (P.under R)))).comap
        (P.under R).polynomialQuotientEquivQuotientPolynomial))
    (IsLocalization.ringEquivOfRingEquiv
      (Localization.AtPrime
        ((P.map (Ideal.Quotient.mk (Ideal.map Polynomial.C (P.under R)))).comap
          (P.under R).polynomialQuotientEquivQuotientPolynomial))
      (Localization.AtPrime
        (P.map (Ideal.Quotient.mk (Ideal.map Polynomial.C (P.under R)))))
      (P.under R).polynomialQuotientEquivQuotientPolynomial
      (((P.under R).polynomialQuotientEquivQuotientPolynomial).map_primeCompl_comap_eq
        (P.map (Ideal.Quotient.mk (Ideal.map Polynomial.C (P.under R))))))

theorem kmf2_polyasc_isRegularLocalRing_quotient_fiber
    (R : Type u) [CommRing R] (P : Ideal (Polynomial R)) [P.IsPrime] :
    IsRegularLocalRing
      (Localization.AtPrime P ⧸
        Ideal.map (algebraMap (Polynomial R) (Localization.AtPrime P))
          (Ideal.map Polynomial.C (P.under R))) := by
  have hIP : Ideal.map Polynomial.C (P.under R) ≤ P := by
    rw [Ideal.map_le_iff_le_comap, ← Polynomial.algebraMap_eq]
  haveI hPbar : (P.map (Ideal.Quotient.mk (Ideal.map Polynomial.C (P.under R)))).IsPrime := by
    refine Ideal.map_isPrime_of_surjective Ideal.Quotient.mk_surjective ?_
    rw [Ideal.mk_ker]
    exact hIP

  have hsub : Algebra.algebraMapSubmonoid
      (Polynomial R ⧸ Ideal.map Polynomial.C (P.under R)) P.primeCompl
      = (P.map (Ideal.Quotient.mk (Ideal.map Polynomial.C (P.under R)))).primeCompl := by
    ext x
    constructor
    · intro hx
      obtain ⟨b, hb, rfl⟩ := Submonoid.mem_map.mp hx
      rw [Ideal.mem_primeCompl_iff]
      rw [Ideal.Quotient.algebraMap_eq]
      intro hmem
      obtain ⟨a, haP, hab⟩ :=
        (Ideal.mem_map_iff_of_surjective _ Ideal.Quotient.mk_surjective).mp hmem
      have hd : a - b ∈ Ideal.map Polynomial.C (P.under R) :=
        (Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _).mp hab
      have hbP : b ∈ P := by
        have h2 := P.sub_mem haP (hIP hd)
        rwa [sub_sub_cancel] at h2
      exact (Ideal.mem_primeCompl_iff.mp hb) hbP
    · intro hx
      obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective x
      refine Submonoid.mem_map.mpr ⟨b, ?_, by rw [Ideal.Quotient.algebraMap_eq]⟩
      rw [Ideal.mem_primeCompl_iff]
      intro hbP
      exact (Ideal.mem_primeCompl_iff.mp hx) (Ideal.mem_map_of_mem _ hbP)

  haveI hloc2 : IsLocalization
      (P.map (Ideal.Quotient.mk (Ideal.map Polynomial.C (P.under R)))).primeCompl
      (Localization.AtPrime P ⧸
        Ideal.map (algebraMap (Polynomial R) (Localization.AtPrime P))
          (Ideal.map Polynomial.C (P.under R))) := by
    have h0 : IsLocalization
        (Algebra.algebraMapSubmonoid
          (Polynomial R ⧸ Ideal.map Polynomial.C (P.under R)) P.primeCompl)
        (Localization.AtPrime P ⧸
          Ideal.map (algebraMap (Polynomial R) (Localization.AtPrime P))
            (Ideal.map Polynomial.C (P.under R))) := inferInstance
    rwa [hsub] at h0

  have hPbarReg : IsRegularLocalRing (Localization.AtPrime
      (P.map (Ideal.Quotient.mk (Ideal.map Polynomial.C (P.under R))))) :=
    kmf2_polyasc_isRegularLocalRing_localization_atPrime_fiberPrime R P
  exact kmf2_polyasc_isRegularLocalRing_of_isLocalization_primeCompl
    (P.map (Ideal.Quotient.mk (Ideal.map Polynomial.C (P.under R))))
    (Localization.AtPrime P ⧸
      Ideal.map (algebraMap (Polynomial R) (Localization.AtPrime P))
        (Ideal.map Polynomial.C (P.under R)))
    hloc2 hPbarReg

theorem kmf2_polyasc_isRegularLocalRing_localization_atPrime_polynomial_of_isRegularRing
    (R : Type u) [CommRing R] [IsRegularRing R]
    (P : Ideal (Polynomial R)) [P.IsPrime] :
    IsRegularLocalRing (Localization.AtPrime P) := by
  letI := Localization.AtPrime.algebraOfLiesOver (P.under R) P
  haveI : IsRegularLocalRing (Localization.AtPrime (P.under R)) :=
    IsRegularRing.isRegularLocalRing_localization (P.under R)
  haveI : Module.Free R (Polynomial R) := Module.Free.of_basis (Polynomial.basisMonomials R)
  haveI : Module.Flat R (Polynomial R) := inferInstance
  haveI : Module.Flat (Localization.AtPrime (P.under R)) (Localization.AtPrime P) :=
    inferInstance
  haveI : IsLocalHom (algebraMap (Localization.AtPrime (P.under R))
      (Localization.AtPrime P)) := by
    rw [Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq (p := P.under R) (P := P)]
    infer_instance
  have hfiber : IsRegularLocalRing
      (Localization.AtPrime P ⧸
        Ideal.map (algebraMap (Localization.AtPrime (P.under R)) (Localization.AtPrime P))
          (IsLocalRing.maximalIdeal (Localization.AtPrime (P.under R)))) := by
    have h1 : Ideal.map
        (algebraMap (Localization.AtPrime (P.under R)) (Localization.AtPrime P))
        (IsLocalRing.maximalIdeal (Localization.AtPrime (P.under R)))
        = Ideal.map (algebraMap (Polynomial R) (Localization.AtPrime P))
            (Ideal.map Polynomial.C (P.under R)) := by
      rw [← IsLocalization.AtPrime.map_eq_maximalIdeal (P.under R)
          (Localization.AtPrime (P.under R)),
        Ideal.map_map, Ideal.map_map, ← IsScalarTower.algebraMap_eq,
        ← Polynomial.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
    rw [h1]
    exact kmf2_polyasc_isRegularLocalRing_quotient_fiber R P
  exact RegularFlatLocalAscent.isRegularLocalRing_of_flat_of_isRegularLocalRing_quotient
    (Localization.AtPrime (P.under R)) (Localization.AtPrime P) hfiber

theorem kmf2_polyasc_isRegularRing_polynomial_of_isRegularRing
    (R : Type u) [CommRing R] [IsRegularRing R] :
    IsRegularRing (Polynomial R) := by
  haveI : IsNoetherianRing (Polynomial R) := Polynomial.isNoetherianRing
  refine isRegularRing_iff.mpr ?_
  intro P hP
  exact kmf2_polyasc_isRegularLocalRing_localization_atPrime_polynomial_of_isRegularRing R P

theorem kmf2_polyasc_isRegularRing_mvPolynomial_fin
    (k : Type u) [Field k] (n : ℕ) :
    IsRegularRing (MvPolynomial (Fin n) k) := by
  induction n with
  | zero =>
    haveI : IsRegularRing k := by
      haveI : IsDedekindDomain k := inferInstance
      infer_instance
    exact IsRegularRing.of_ringEquiv (MvPolynomial.isEmptyAlgEquiv k (Fin 0)).symm.toRingEquiv
  | succ n ih =>
    haveI := ih
    haveI : IsRegularRing (Polynomial (MvPolynomial (Fin n) k)) :=
      kmf2_polyasc_isRegularRing_polynomial_of_isRegularRing (MvPolynomial (Fin n) k)
    exact IsRegularRing.of_ringEquiv (MvPolynomial.finSuccEquiv k n).symm.toRingEquiv

theorem kmf2_polyasc_gate_input_clause_mvPolynomial
    (k : Type u) [Field k] (n : ℕ) :
    Algebra.Smooth k (MvPolynomial (Fin n) k) ∧
      ∀ (P : Ideal (MvPolynomial (Fin n) k)) [P.IsPrime],
        IsRegularLocalRing (Localization.AtPrime P) := by
  refine ⟨{ formallySmooth := inferInstance, finitePresentation := inferInstance }, ?_⟩
  intro P hP
  haveI := kmf2_polyasc_isRegularRing_mvPolynomial_fin k n
  exact IsRegularRing.isRegularLocalRing_localization P

theorem kmf2_polyasc_gate_isRegularRing_polynomial_int :
    IsRegularRing (Polynomial ℤ) := by
  haveI : IsRegularRing ℤ := by
    haveI : IsDedekindDomain ℤ := inferInstance
    infer_instance
  exact kmf2_polyasc_isRegularRing_polynomial_of_isRegularRing ℤ

Statements phrased using this module (0)

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