NYLL
Module

MaximalAdicCompletionGeometry.lean

Nyll.EtaleFundamentalGroups.Kummer.LocalGeometry.HeightTwo.MaximalAdicCompletionGeometry
6 declarations indexed from sourceView source ↗

Module documentation

Height-two regular geometry after maximal-adic completion

Mathlib does not currently expose a general theorem saying that the maximal-adic completion of a regular local ring is again a regular local ring. The height-two argument needs less.

For a regular pair, quotienting by either parameter gives a DVR. Completion base change identifies the quotient by the extended parameter with the completion of that DVR, hence the extended parameter remains prime. Flatness preserves the regular pair, and adic separatedness together with one prime regular parameter then proves that the completed ring is a domain.

Thus all geometry used below is produced from existing completion, tensor, regular-sequence, and standard-DVR APIs; no analytic-irreducibility or completion-regularity assumption is introduced.

Imports6
Imported by3

Declarations

theorem

isDomain_of_prime_isSMulRegular_of_isHausdorff_maximalIdeal

L49 ↗
EtaleFundamentalGroups.Kummer.isDomain_of_prime_isSMulRegular_of_isHausdorff_maximalIdeal
Documentation

A prime regular element in a local ring separated for its maximal-ideal adic topology forces the ring to be a domain.

This is the separated analogue of isDomain_of_prime_isSMulRegular: the only use of Noetherianity in that theorem is Krull intersection, which is supplied here directly by IsHausdorff.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped BigOperators
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open RingTheory.Sequence
universe u
Lean source · statement
theorem isDomain_of_prime_isSMulRegular_of_isHausdorff_maximalIdeal
    {R : Type u} [CommRing R] [IsLocalRing R]
    [IsHausdorff (maximalIdeal R) R]
    {p : R} (hp : Prime p) (hpreg : IsSMulRegular R p) : IsDomain R
theorem

maximalAdicCompletion_mappedIdeal_isPrime_of_quotientDVR

L132 ↗
EtaleFundamentalGroups.Kummer.maximalAdicCompletion_mappedIdeal_isPrime_of_quotientDVR
Documentation

If a prime quotient of a Noetherian local ring is a DVR, extension of that prime to the maximal-adic completion remains prime.

The completed quotient is first written as a tensor product, then as the completion of the quotient DVR at its maximal ideal. The latter is a domain because it is canonically the valuation subring in the standard valued-field completion.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped BigOperators
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open RingTheory.Sequence
universe u
Lean source · statement
theorem maximalAdicCompletion_mappedIdeal_isPrime_of_quotientDVR
    {B : Type u} [CommRing B] [IsLocalRing B] [IsNoetherianRing B]
    (I : Ideal B) [I.IsPrime]
    [IsDiscreteValuationRing (B ⧸ I)] :
    (I.map (algebraMap B
      (AdicCompletion (maximalIdeal B) B))).IsPrime
theorem

prime_first_maximalAdicCompletion_of_regularPair

L187 ↗
EtaleFundamentalGroups.Kummer.prime_first_maximalAdicCompletion_of_regularPair
Documentation

The first member of a regular pair remains prime after maximal-adic completion. Its source quotient is shown internally to be a DVR from the one-element quotient regular system.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped BigOperators
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open RingTheory.Sequence
universe u
Lean source · statement
theorem prime_first_maximalAdicCompletion_of_regularPair
    {B : Type u} [CommRing B] [IsLocalRing B] [IsNoetherianRing B]
    {x y : B}
    (hreg : IsRegular B [x, y])
    (hgen : Ideal.ofList [x, y] = maximalIdeal B) :
    Prime (algebraMap B (AdicCompletion (maximalIdeal B) B) x)
theorem

maximalAdicCompletion_regularPair_geometry

L251 ↗
EtaleFundamentalGroups.Kummer.maximalAdicCompletion_regularPair_geometry
Documentation

A regular pair stays regular and continues to generate the closed point after maximal-adic completion. Both parameters remain prime, and the completed ring is a domain.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped BigOperators
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open RingTheory.Sequence
universe u
Lean source · full declaration
theorem maximalAdicCompletion_regularPair_geometry
    {B : Type u} [CommRing B] [IsLocalRing B] [IsNoetherianRing B]
    {x y : B}
    (hreg : IsRegular B [x, y])
    (hgen : Ideal.ofList [x, y] = maximalIdeal B) :
    let Bhat := AdicCompletion (maximalIdeal B) B
    IsDomain Bhat ∧
      IsRegular Bhat [algebraMap B Bhat x, algebraMap B Bhat y] ∧
      Ideal.ofList [algebraMap B Bhat x, algebraMap B Bhat y] =
        maximalIdeal Bhat ∧
      Prime (algebraMap B Bhat x) ∧
      Prime (algebraMap B Bhat y) := by
  dsimp only
  let Bhat := AdicCompletion (maximalIdeal B) B
  let : Module.FaithfullyFlat B Bhat :=
    Module.FaithfullyFlat.of_flat_of_isLocalHom
  have hregHat :
      IsRegular Bhat [algebraMap B Bhat x, algebraMap B Bhat y] := by
    simpa only [List.map_cons, List.map_nil] using
      hreg.of_faithfullyFlat (S := Bhat)
  have hgenHat :
      Ideal.ofList [algebraMap B Bhat x, algebraMap B Bhat y] =
        maximalIdeal Bhat := by
    calc
      Ideal.ofList [algebraMap B Bhat x, algebraMap B Bhat y] =
          (Ideal.ofList [x, y]).map (algebraMap B Bhat) := by
        simpa only [List.map_cons, List.map_nil] using
          (Ideal.map_ofList (algebraMap B Bhat) [x, y]).symm
      _ = (maximalIdeal B).map (algebraMap B Bhat) := by rw [hgen]
      _ = maximalIdeal Bhat :=
        (AdicCompletion.maximalIdeal_eq_map (R := B)).symm
  have hxPrime : Prime (algebraMap B Bhat x) :=
    prime_first_maximalAdicCompletion_of_regularPair hreg hgen
  have hregSwap : IsRegular B [y, x] := by
    exact IsLocalRing.isRegular_of_perm hreg
      (List.Perm.swap x y []).symm
  have hgenSwap : Ideal.ofList [y, x] = maximalIdeal B := by
    calc
      Ideal.ofList [y, x] = Ideal.ofList [x, y] := by
        apply congrArg Ideal.span
        ext z
        simp [or_comm]
      _ = maximalIdeal B := hgen
  have hyPrime : Prime (algebraMap B Bhat y) :=
    prime_first_maximalAdicCompletion_of_regularPair hregSwap hgenSwap
  have hxRegular : IsSMulRegular Bhat (algebraMap B Bhat x) :=
    ((isRegular_cons_iff Bhat (algebraMap B Bhat x)
      [algebraMap B Bhat y]).mp hregHat).1
  have hdomain : IsDomain Bhat :=
    isDomain_of_prime_isSMulRegular_of_isHausdorff_maximalIdeal
      hxPrime hxRegular
  exact ⟨hdomain, hregHat, hgenHat, hxPrime, hyPrime⟩
theorem

charZero_quotient_mappedIdeal_maximalAdicCompletion

L306 ↗
EtaleFundamentalGroups.Kummer.charZero_quotient_mappedIdeal_maximalAdicCompletion
Documentation

Characteristic zero of a divisor quotient is preserved after extending the divisor to the maximal-adic completion.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped BigOperators
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open RingTheory.Sequence
universe u
Lean source · statement
theorem charZero_quotient_mappedIdeal_maximalAdicCompletion
    {B : Type u} [CommRing B] [IsLocalRing B] [IsNoetherianRing B]
    (I : Ideal B) (hCharZero : CharZero (B ⧸ I)) :
    CharZero
      (AdicCompletion (maximalIdeal B) B ⧸
        I.map (algebraMap B
          (AdicCompletion (maximalIdeal B) B)))
theorem

associated_fintypeProduct_maximalAdicCompletion

L331 ↗
EtaleFundamentalGroups.Kummer.associated_fintypeProduct_maximalAdicCompletion
Documentation

Association with a finite product is preserved by the canonical map to the maximal-adic completion.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped BigOperators
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open RingTheory.Sequence
universe u
Lean source · statement
theorem associated_fintypeProduct_maximalAdicCompletion
    {B : Type u} [CommRing B] [IsLocalRing B]
    {ι : Type*} [Fintype ι]
    (f : B) (s : ι → B)
    (hAssoc : Associated f (∏ i, s i)) :
    Associated
      (algebraMap B (AdicCompletion (maximalIdeal B) B) f)
      (∏ i, algebraMap B (AdicCompletion (maximalIdeal B) B) (s i))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.