Module

PrimeRootCover.lean

Nyll.EtaleFundamentalGroups.Kummer.LocalGeometry.HeightTwo.PrimeRootCover

3 declarations indexed from sourceView source ↗

Module documentation

Rooting a prime regular divisor in dimension two

Let p be a prime element in a two-dimensional regular local domain. If the quotient by p is regular local, then the class of p in the cotangent space is nonzero. Thus p extends to a regular parameter pair, and every positive Kummer root of p is again a two-dimensional regular local domain.

The quotient regularity is used to produce, rather than assume, the missing second parameter: the quotient has dimension one, so its maximal ideal is principal. A lift of a generator, together with p, generates the original maximal ideal. If p belonged to its square, the two-dimensional cotangent space would then be generated by one element, a contradiction.

Imports2

Imported by6

theorem

prime_not_mem_maximalIdeal_sq_of_regular_quotient_dimension_two

L37 ↗

EtaleFundamentalGroups.Kummer.prime_not_mem_maximalIdeal_sq_of_regular_quotient_dimension_two

Documentation

A prime divisor with regular quotient in a two-dimensional regular local domain has nonzero cotangent class.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

theorem prime_not_mem_maximalIdeal_sq_of_regular_quotient_dimension_two
    {R : Type u} [CommRing R] [IsDomain R] [IsRegularLocalRing R]
    {p : R} (hp : Prime p)
    (hquot : IsRegularLocalRing (R ⧸ Ideal.span ({p} : Set R)))
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞)) :
    p ∉ maximalIdeal R ^ 2

theorem

exists_regular_pair_of_prime_regular_quotient_dimension_two

L157 ↗

EtaleFundamentalGroups.Kummer.exists_regular_pair_of_prime_regular_quotient_dimension_two

Documentation

A prime divisor with regular quotient extends to a regular parameter pair in dimension two.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · statement

theorem exists_regular_pair_of_prime_regular_quotient_dimension_two
    {R : Type u} [CommRing R] [IsDomain R] [IsRegularLocalRing R]
    {p : R} (hp : Prime p)
    (hquot : IsRegularLocalRing (R ⧸ Ideal.span ({p} : Set R)))
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞)) :
    ∃ z : R, IsRegular R [p, z] ∧
      Ideal.ofList [p, z] = maximalIdeal R

theorem

heightTwoPrimeRootCover_geometry

L180 ↗

EtaleFundamentalGroups.Kummer.heightTwoPrimeRootCover_geometry

Documentation

Rooting a prime divisor with regular quotient in dimension two produces another two-dimensional regular local domain. The new root is prime, and its quotient is again a regular local domain.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open Polynomial
open RingTheory.Sequence
universe u

Lean source · full declaration

theorem heightTwoPrimeRootCover_geometry
    {R : Type u} [CommRing R] [IsDomain R] [IsRegularLocalRing R]
    {n : ℕ} (hn : 0 < n) {p : R} (hp : Prime p)
    (hquot : IsRegularLocalRing (R ⧸ Ideal.span ({p} : Set R)))
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞)) :
    let f : R[X] := X ^ n - C p
    let B := AdjoinRoot f
    IsRegularLocalRing B ∧ IsDomain B ∧
      ringKrullDim B = ((2 : ℕ∞) : WithBot ℕ∞) ∧
      Prime (AdjoinRoot.root f) ∧
      IsDomain (B ⧸ Ideal.span ({AdjoinRoot.root f} : Set B)) ∧
      IsRegularLocalRing
        (B ⧸ Ideal.span ({AdjoinRoot.root f} : Set B)) := by
  dsimp only
  obtain ⟨z, hreg, hgen⟩ :=
    exists_regular_pair_of_prime_regular_quotient_dimension_two hp hquot hdim
  let f : R[X] := X ^ n - C p
  let B := AdjoinRoot f
  have hpMem : p ∈ maximalIdeal R := by
    rw [mem_maximalIdeal]
    exact hp.not_isUnit
  let : IsLocalRing B := by
    simpa only [B, f] using isLocalRing_adjoinRoot_X_pow_sub_C hn hpMem
  have hgeometry := localRootCover_regularSystem_geometry hn hreg hgen
  have hnoetherianB : IsNoetherianRing B := by
    simpa only [B, f] using hgeometry.1
  let : IsNoetherianRing B := hnoetherianB
  have hdomainB : IsDomain B := by
    simpa only [B, f] using hgeometry.2.1
  let : IsDomain B := hdomainB
  have hregB : IsRegular B (localRootCoverParameterList R n p [z]) := by
    simpa only [B, f] using hgeometry.2.2.1
  have hgenB : Ideal.ofList (localRootCoverParameterList R n p [z]) =
      maximalIdeal B := by
    simpa only [B, f] using hgeometry.2.2.2.1
  have hregularLocalB : IsRegularLocalRing B :=
    isRegularLocalRing_of_regularSystem _ hregB hgenB
  let : IsRegularLocalRing B := hregularLocalB
  have hdimB : ringKrullDim B = ((2 : ℕ∞) : WithBot ℕ∞) := by
    calc
      ringKrullDim B =
          ((localRootCoverParameterList R n p [z]).length : WithBot ℕ∞) := by
        simpa only [B, f] using
          (localRootCoverParameterList_length_eq_ringKrullDim hn hreg hgen)
      _ = ((2 : ℕ∞) : WithBot ℕ∞) := by
        norm_num [localRootCoverParameterList]
  have hrootMem : AdjoinRoot.root f ∈
      localRootCoverParameterList R n p [z] := by
    simp only [f, localRootCoverParameterList, List.mem_cons, true_or]
  have hrootPrime : Prime (AdjoinRoot.root f) := by
    exact prime_of_mem_regularSystem hregB hgenB hrootMem
  have hrootQuotient :=
    quotient_geometry_of_mem_regularSystem hregB hgenB hrootMem
  exact ⟨hregularLocalB, hdomainB, hdimB, hrootPrime,
    hrootQuotient.1, hrootQuotient.2⟩

Module documentation

Rooting a prime regular divisor in dimension two

Declarations

prime_not_mem_maximalIdeal_sq_of_regular_quotient_dimension_two

exists_regular_pair_of_prime_regular_quotient_dimension_two

heightTwoPrimeRootCover_geometry