NYLL
Module

FullRootCoverResidue.lean

Nyll.EtaleFundamentalGroups.Kummer.NormalCrossings.HeightTwo.FullRootCoverResidue
5 declarations indexed from sourceView source ↗

Module documentation

Residue characteristic on the height-two full root cover

Characteristic zero along the active branches of the original strict-normal-crossings chart is transported first to the height-two localization and then through the conditional radical cover. For an actual radical branch, its principal root prime is used as a concrete height-one prime; the existing contraction theorem identifies its contraction with the localized radicand prime, so the quotient algebra map is injective.

The same quotient-injection mechanism transports characteristic zero further to the closed quotient of a full-cover prime and to the closed quotient of its height-one localization. No residue comparison is assumed.

Imports2
Imported by3

Declarations

theorem

charZero_quotient_map_of_faithfullyFlat

L38 ↗
EtaleFundamentalGroups.Kummer.charZero_quotient_map_of_faithfullyFlat
Documentation

A faithfully flat extension preserves characteristic zero after quotienting by the extension of an ideal.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open IsLocalRing
universe u v
attribute [local instance] Classical.propDecidable
Lean source · statement
theorem charZero_quotient_map_of_faithfullyFlat
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [Algebra R S] [Module.FaithfullyFlat R S]
    (I : Ideal R) (hCharZero : CharZero (R ⧸ I)) :
    CharZero (S ⧸ I.map (algebraMap R S))
theorem

charZero_quotient_of_charZero_under

L56 ↗
EtaleFundamentalGroups.Kummer.charZero_quotient_of_charZero_under
Documentation

Characteristic zero of the quotient by a contraction injects into the corresponding quotient upstairs.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open IsLocalRing
universe u v
attribute [local instance] Classical.propDecidable
Lean source · statement
theorem charZero_quotient_of_charZero_under
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [Algebra R S] (Q : Ideal S)
    (hCharZero : CharZero (R ⧸ Q.under R)) :
    CharZero (S ⧸ Q)
theorem

charZero_localizationAtPrime_quotient_maximalIdeal

L67 ↗
EtaleFundamentalGroups.Kummer.charZero_localizationAtPrime_quotient_maximalIdeal
Documentation

Characteristic zero of a prime quotient is preserved by passing to the closed quotient of its local ring.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open IsLocalRing
universe u v
attribute [local instance] Classical.propDecidable
Lean source · statement
theorem charZero_localizationAtPrime_quotient_maximalIdeal
    {R : Type u} [CommRing R] (Q : Ideal R) [Q.IsPrime]
    (hCharZero : CharZero (R ⧸ Q)) :
    CharZero
      (Localization.AtPrime Q ⧸
        maximalIdeal (Localization.AtPrime Q))
theorem

charZero_quotient_iteratedRadicalRoot

L91 ↗
EtaleFundamentalGroups.Kummer.charZero_quotient_iteratedRadicalRoot
Documentation

Characteristic zero along a base radicand passes to the quotient by its actual prime root in a positive iterated radical cover. The required contraction equality is generated by applying the height-one contraction theorem to the principal root prime.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open IsLocalRing
universe u v
attribute [local instance] Classical.propDecidable
Lean source · statement
theorem charZero_quotient_iteratedRadicalRoot
    {A : Type u} [CommRing A] [IsDomain A] [IsNoetherianRing A]
    {s : ℕ} (n : Fin s → ℕ) (a : Fin s → A)
    (hn : ∀ j, 0 < n j)
    [IsDomain (iteratedRadical A s n a)]
    (k : Fin s) (haPrime : Prime (a k))
    (hrootPrime : Prime (iteratedRadicalRoot A n a k))
    (hCharZero : CharZero (A ⧸ Ideal.span ({a k} : Set A))) :
    CharZero
      (iteratedRadical A s n a ⧸
        Ideal.span
          ({iteratedRadicalRoot A n a k} :
            Set (iteratedRadical A s n a)))
theorem

splitStrictNormalCrossings_heightTwo_fullRootCover_heightOnePrime_trichotomy_charZero

L132 ↗
EtaleFundamentalGroups.Kummer.splitStrictNormalCrossings_heightTwo_fullRootCover_heightOnePrime_trichotomy_charZero
Documentation

Residue-characteristic refinement of the full-cover trichotomy. The selected quotient of the conditional cover has characteristic zero. In an actual-other-root branch, the corresponding root quotient does too. In both boundary branches this characteristic-zero statement is transported to the full prime quotient and to the closed quotient of its local ring.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open IsLocalRing
universe u v
attribute [local instance] Classical.propDecidable
Lean source · full declaration
theorem splitStrictNormalCrossings_heightTwo_fullRootCover_heightOnePrime_trichotomy_charZero
    {A : Type u} [CommRing A] [IsDomain A] [IsLocalRing A]
    [IsRegularRing A]
    {d r : ℕ} {f : A} {t : Fin (d + 1) → A}
    (hNC : IsSplitStrictNormalCrossingsAt f t r)
    (hCharZero : ∀ j : Fin (d + 1), j.1 < r →
      CharZero (A ⧸ Ideal.span ({t j} : Set A)))
    (i : Fin (d + 1)) (hi : i.1 < r)
    (P : Ideal A) [P.IsPrime] (hP : P.height = 2)
    (htiP : t i ∈ P)
    (e : Fin d → ℕ) (he : ∀ k, 0 < e k)
    (N : ℕ) (hN : 0 < N) :
    ∃ σ : Equiv.Perm (Fin d),
      let R := Localization.AtPrime P
      let n := heightTwoConditionalOtherExponent t i r P e σ
      let a : Fin d → R :=
        heightTwoConditionalOtherRadicand t i P σ
      let B := iteratedRadical R d n a
      let y : R := algebraMap A R (t i)
      let F : B[X] := X ^ N - C (algebraMap R B y)
      let D := AdjoinRoot F
      (IsRegularLocalRing B ∧ IsDomain B ∧
        Prime (algebraMap R B y) ∧
        IsDomain (B ⧸ Ideal.span ({algebraMap R B y} : Set B)) ∧
        IsRegularLocalRing
          (B ⧸ Ideal.span ({algebraMap R B y} : Set B))) ∧
      (∀ k, 0 < n k) ∧
      ringKrullDim B = ((2 : ℕ∞) : WithBot ℕ∞) ∧
      CharZero (B ⧸ Ideal.span ({algebraMap R B y} : Set B)) ∧
      (IsRegularLocalRing D ∧ IsDomain D ∧
        ringKrullDim D = ((2 : ℕ∞) : WithBot ℕ∞) ∧
        Prime (AdjoinRoot.root F) ∧
        IsDomain (D ⧸ Ideal.span ({AdjoinRoot.root F} : Set D)) ∧
        IsRegularLocalRing
          (D ⧸ Ideal.span ({AdjoinRoot.root F} : Set D))) ∧
      ∀ (q : Ideal D) [q.IsPrime], q.height = 1 →
        (q.under B).IsPrime ∧ (q.under B).height = 1 ∧
          ((q = Ideal.span ({AdjoinRoot.root F} : Set D) ∧
              CharZero (D ⧸ q) ∧
              CharZero
                (Localization.AtPrime q ⧸
                  maximalIdeal (Localization.AtPrime q))) ∨
            (∃ k : Fin d,
              (i.succAbove (σ k)).1 < r ∧
              t (i.succAbove (σ k)) ∈ P ∧
              n k = e (σ k) ∧
              Prime (iteratedRadicalRoot R n a k) ∧
              CharZero
                (B ⧸ Ideal.span
                  ({iteratedRadicalRoot R n a k} : Set B)) ∧
              q.under B = Ideal.span
                ({iteratedRadicalRoot R n a k} : Set B) ∧
              CharZero (D ⧸ q) ∧
              CharZero
                (Localization.AtPrime q ⧸
                  maximalIdeal (Localization.AtPrime q))) ∨
            Disjoint
              (((Submonoid.powers
                (algebraMap R B (algebraMap A R f)) : Submonoid B) : Set B))
              (q.under B : Set B)) := by
  classical
  rcases
      splitStrictNormalCrossings_heightTwo_fullRootCover_heightOnePrime_contraction_trichotomy
        hNC i hi P hP htiP e he N hN with
    ⟨σ, hgeometryB, hn, hdimB, hgeometryD, htrichotomy⟩
  let R := Localization.AtPrime P
  let n := heightTwoConditionalOtherExponent t i r P e σ
  let a : Fin d → R := heightTwoConditionalOtherRadicand t i P σ
  let B := iteratedRadical R d n a
  let y : R := algebraMap A R (t i)
  let F : B[X] := X ^ N - C (algebraMap R B y)
  let D := AdjoinRoot F
  let : IsDomain B := hgeometryB.2.1
  let : IsDomain D := hgeometryD.2.1
  let : Module.FaithfullyFlat R B := faithfullyFlat_iteratedRadical n a hn
  have hCharSelectedR :
      CharZero (R ⧸ Ideal.span ({y} : Set R)) := by
    simpa only [R, y] using
      (charZero_quotient_algebraMap_localizationAtPrime P
        (hNC.2.2.2.1 i hi) htiP (hCharZero i hi))
  have hCharSelectedB :
      CharZero (B ⧸ Ideal.span ({algebraMap R B y} : Set B)) := by
    have hmap := charZero_quotient_map_of_faithfullyFlat
      (S := B) (Ideal.span ({y} : Set R)) hCharSelectedR
    have hmapIdeal :
        (Ideal.span ({y} : Set R)).map (algebraMap R B) =
          Ideal.span ({algebraMap R B y} : Set B) := by
      simp [Ideal.map_span]
    rw [← hmapIdeal]
    exact hmap
  refine ⟨σ, hgeometryB, hn, hdimB, hCharSelectedB, hgeometryD, ?_⟩
  intro q _ hqHeight
  rcases htrichotomy q hqHeight with
    ⟨hqUnderPrime, hqUnderHeight, hselected | hother | haway⟩
  · have hqEq : q = Ideal.span ({AdjoinRoot.root F} : Set D) := by
      simpa only [F, D] using
        (heightOnePrime_eq_span_root_of_under_eq_span_radicand
          hgeometryD.2.2.2.1 q hqHeight hselected)
    have hCharUnder : CharZero (B ⧸ q.under B) := by
      rw [hselected]
      exact hCharSelectedB
    have hCharQ : CharZero (D ⧸ q) :=
      charZero_quotient_of_charZero_under q hCharUnder
    have hCharLocal :
        CharZero
          (Localization.AtPrime q ⧸
            maximalIdeal (Localization.AtPrime q)) :=
      charZero_localizationAtPrime_quotient_maximalIdeal q hCharQ
    exact ⟨hqUnderPrime, hqUnderHeight,
      Or.inl ⟨hqEq, hCharQ, hCharLocal⟩⟩
  · rcases hother with
      ⟨k, hkActive, htkP, hnk, hrootPrime, hunder⟩
    let j : Fin (d + 1) := i.succAbove (σ k)
    have htPrime : Prime (t j) := hNC.2.2.2.1 j hkActive
    have haPrime : Prime (a k) := by
      rcases prime_or_isUnit_algebraMap_localizationAtPrime P htPrime with
        hprime | hunit
      · change Prime (algebraMap A (Localization.AtPrime P) (t j))
        exact hprime
      · have htCompl : t j ∈ P.primeCompl :=
          (IsLocalization.AtPrime.isUnit_to_map_iff
            (Localization.AtPrime P) P (t j)).mp hunit
        exact (htCompl htkP).elim
    have hCharRadicandR :
        CharZero (R ⧸ Ideal.span ({a k} : Set R)) := by
      change CharZero
        (Localization.AtPrime P ⧸
          Ideal.span
            ({algebraMap A (Localization.AtPrime P) (t j)} :
              Set (Localization.AtPrime P)))
      exact charZero_quotient_algebraMap_localizationAtPrime P
        htPrime htkP (hCharZero j hkActive)
    have hCharRootB :
        CharZero
          (B ⧸ Ideal.span
            ({iteratedRadicalRoot R n a k} : Set B)) :=
      charZero_quotient_iteratedRadicalRoot n a hn k haPrime
        hrootPrime hCharRadicandR
    have hCharUnder : CharZero (B ⧸ q.under B) := by
      rw [hunder]
      exact hCharRootB
    have hCharQ : CharZero (D ⧸ q) :=
      charZero_quotient_of_charZero_under q hCharUnder
    have hCharLocal :
        CharZero
          (Localization.AtPrime q ⧸
            maximalIdeal (Localization.AtPrime q)) :=
      charZero_localizationAtPrime_quotient_maximalIdeal q hCharQ
    exact ⟨hqUnderPrime, hqUnderHeight, Or.inr (Or.inl
      ⟨k, hkActive, htkP, hnk, hrootPrime, hCharRootB, hunder,
        hCharQ, hCharLocal⟩)⟩
  · exact ⟨hqUnderPrime, hqUnderHeight, Or.inr (Or.inr haway)⟩

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