NYLL
Module

Parameters.lean

Nyll.SchemeTheory.Divisors.NormalCrossings.HeightTwo.Parameters
5 declarations indexed from sourceView source ↗

Module documentation

Strict-normal-crossings parameters at height two

A branch of a strict normal crossings divisor stays a regular parameter after localization at every height-two point on that branch. The key input is the scheme-level regularity of the branch quotient. Quotienting after localizing is identified with localizing the branch quotient; hence the former is a one-dimensional regular local ring. If the branch equation lay in the square of the localized maximal ideal, Nakayama would make that maximal ideal principal, contradicting its two-dimensional cotangent space.

Imports5
Imported by3

Declarations

def

quotientPrimeOfLe

L34 ↗
EtaleFundamentalGroups.quotientPrimeOfLe
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open RingTheory.Sequence
universe u
Lean source · statement
def quotientPrimeOfLe
    {R : Type u} [CommRing R] {I P : Ideal R} [P.IsPrime] (hIP : I ≤ P) :
    PrimeSpectrum (R ⧸ I)
theorem

primeCompl_map_quotient_eq

L40 ↗
EtaleFundamentalGroups.primeCompl_map_quotient_eq
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open RingTheory.Sequence
universe u
Lean source · statement
theorem primeCompl_map_quotient_eq
    {R : Type u} [CommRing R] {I P : Ideal R} [P.IsPrime] (hIP : I ≤ P) :
    P.primeCompl.map (Ideal.Quotient.mk I) =
      (quotientPrimeOfLe hIP).asIdeal.primeCompl
def

quotientLocalizationEquiv

L63 ↗
EtaleFundamentalGroups.quotientLocalizationEquiv
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open RingTheory.Sequence
universe u
Lean source · full declaration
def quotientLocalizationEquiv
    {R : Type u} [CommRing R] {I P : Ideal R} [P.IsPrime] (hIP : I ≤ P) :
    let Q := quotientPrimeOfLe hIP
    let Rₚ := Localization.AtPrime P
    let J := I.map (algebraMap R Rₚ)
    letI : Algebra (R ⧸ I) (Rₚ ⧸ J) :=
      Ideal.Quotient.algebraQuotientOfLEComap (R := R) (A := Rₚ)
        (p := I) (P := J)
        (by
          intro x hx
          exact Ideal.mem_comap.mpr
            (Ideal.mem_map_of_mem (algebraMap R Rₚ) hx))
    Localization.AtPrime Q.asIdeal ≃ₐ[R ⧸ I] (Rₚ ⧸ J) := by
  dsimp only
  let Q := quotientPrimeOfLe hIP
  let Rₚ := Localization.AtPrime P
  let J := I.map (algebraMap R Rₚ)
  letI : Algebra (R ⧸ I) (Rₚ ⧸ J) :=
    Ideal.Quotient.algebraQuotientOfLEComap (R := R) (A := Rₚ)
      (p := I) (P := J)
      (by
        intro x hx
        exact Ideal.mem_comap.mpr
          (Ideal.mem_map_of_mem (algebraMap R Rₚ) hx))
  have hloc :
      IsLocalization (P.primeCompl.map (Ideal.Quotient.mk I)) (Rₚ ⧸ J) := by
    refine IsLocalization.of_surjective
      (M := P.primeCompl) (S := Rₚ)
      (f := Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective
      (g := Ideal.Quotient.mk J) Ideal.Quotient.mk_surjective ?_ ?_
    · ext x
      rfl
    · simp [J, Ideal.mk_ker]
  haveI : IsLocalization Q.asIdeal.primeCompl (Rₚ ⧸ J) := by
    simpa [Q, primeCompl_map_quotient_eq hIP] using hloc
  exact IsLocalization.algEquiv Q.asIdeal.primeCompl
    (Localization.AtPrime Q.asIdeal) (Rₚ ⧸ J)
theorem

regularParameter_not_mem_localized_maximalIdeal_sq

L103 ↗
EtaleFundamentalGroups.regularParameter_not_mem_localized_maximalIdeal_sq
Documentation

A member of a regular system whose quotient is regular on the spectrum has nonzero cotangent class at every height-two prime containing it.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open RingTheory.Sequence
universe u
Lean source · statement
theorem regularParameter_not_mem_localized_maximalIdeal_sq
    {A : Type u} [CommRing A] [IsDomain A] [IsLocalRing A]
    [IsRegularRing A] {d : ℕ} (t : Fin d → A)
    (hreg : IsRegular A (List.ofFn t))
    (hgen : Ideal.ofList (List.ofFn t) = maximalIdeal A)
    (i : Fin d) (hBranch : IsRegularRing (A ⧸ Ideal.span {t i}))
    (P : Ideal A) [P.IsPrime] (hP : P.height = 2) (htiP : t i ∈ P) :
    algebraMap A (Localization.AtPrime P) (t i) ∉
      maximalIdeal (Localization.AtPrime P) ^ 2
theorem

exists_regular_pair_localizationAtPrime_of_splitStrictNormalCrossings

L256 ↗
EtaleFundamentalGroups.exists_regular_pair_localizationAtPrime_of_splitStrictNormalCrossings
Documentation

At a height-two point of a strict normal crossings chart, a selected branch equation extends to a regular pair generating the localized maximal ideal.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open RingTheory.Sequence
universe u
Lean source · statement
theorem exists_regular_pair_localizationAtPrime_of_splitStrictNormalCrossings
    {A : Type u} [CommRing A] [IsDomain A] [IsLocalRing A]
    [IsRegularRing A] {d r : ℕ} {f : A} {t : Fin d → A}
    (hNC : IsSplitStrictNormalCrossingsAt f t r)
    (i : Fin d) (hi : i.1 < r)
    (P : Ideal A) [P.IsPrime] (hP : P.height = 2) (htiP : t i ∈ P) :
    ∃ y : Localization.AtPrime P,
      IsRegular (Localization.AtPrime P)
        [algebraMap A (Localization.AtPrime P) (t i), y] ∧
      Ideal.ofList [algebraMap A (Localization.AtPrime P) (t i), y] =
        maximalIdeal (Localization.AtPrime P)

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