Module

PrimeOverRootCover.lean

Nyll.EtaleFundamentalGroups.Kummer.LocalGeometry.HeightOne.PrimeOverRootCover

4 declarations indexed from sourceView source ↗

Module documentation

Height-one primes over a one-root cover

For D = B[X] / (X^N - p), the root equation sharpens contraction data in two useful ways. A height-one prime of the domain D whose contraction is the principal radicand prime is exactly the principal root prime. Conversely, if the radicand is absent from the contraction, then the root is absent from the prime and becomes a unit after localizing there.

The final theorem feeds the first sharpening into the height-two strict-normal-crossings full-cover endpoint: its selected-contraction branch is upgraded to an equality of primes on the full cover.

Imports1

Nyll.EtaleFundamentalGroups.Kummer.NormalCrossings.HeightTwo.FullRootCoverHeightOne

Imported by3

theorem

heightOnePrime_eq_span_root_of_under_eq_span_radicand

L37 ↗

EtaleFundamentalGroups.Kummer.heightOnePrime_eq_span_root_of_under_eq_span_radicand

Documentation

If a height-one prime over a one-root cover contracts to the radicand prime, then it is the root prime itself. Positivity of the exponent is not needed in this direction: the root equation and primality of q suffice.

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
attribute [local instance] Classical.propDecidable

Lean source · statement

theorem heightOnePrime_eq_span_root_of_under_eq_span_radicand
    {B : Type u} [CommRing B] {N : ℕ} {p : B}
    [IsDomain (AdjoinRoot (X ^ N - C p))]
    (hrootPrime : Prime (AdjoinRoot.root (X ^ N - C p)))
    (q : Ideal (AdjoinRoot (X ^ N - C p))) [q.IsPrime]
    (hqHeight : q.height = 1)
    (hunder : q.under B = Ideal.span ({p} : Set B)) :
    q = Ideal.span
      ({AdjoinRoot.root (X ^ N - C p)} :
        Set (AdjoinRoot (X ^ N - C p)))

theorem

root_not_mem_of_radicand_not_mem_under

L60 ↗

EtaleFundamentalGroups.Kummer.root_not_mem_of_radicand_not_mem_under

Documentation

If the radicand is absent from the contraction of a prime on a positive one-root cover, then the root is absent from that 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
attribute [local instance] Classical.propDecidable

Lean source · statement

theorem root_not_mem_of_radicand_not_mem_under
    {B : Type u} [CommRing B] {N : ℕ} (hN : 0 < N) {p : B}
    (q : Ideal (AdjoinRoot (X ^ N - C p)))
    (hp : p ∉ q.under B) :
    AdjoinRoot.root (X ^ N - C p) ∉ q

theorem

isUnit_root_localizationAtPrime_of_radicand_not_mem_under

L78 ↗

EtaleFundamentalGroups.Kummer.isUnit_root_localizationAtPrime_of_radicand_not_mem_under

Documentation

In the preceding non-contraction case, the root becomes a unit in the local ring at the 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
attribute [local instance] Classical.propDecidable

Lean source · statement

theorem isUnit_root_localizationAtPrime_of_radicand_not_mem_under
    {B : Type u} [CommRing B] {N : ℕ} (hN : 0 < N) {p : B}
    (q : Ideal (AdjoinRoot (X ^ N - C p))) [q.IsPrime]
    (hp : p ∉ q.under B) :
    IsUnit
      (algebraMap (AdjoinRoot (X ^ N - C p)) (Localization.AtPrime q)
        (AdjoinRoot.root (X ^ N - C p)))

theorem

splitStrictNormalCrossings_heightTwo_fullRootCover_heightOnePrime_trichotomy

L92 ↗

EtaleFundamentalGroups.Kummer.splitStrictNormalCrossings_heightTwo_fullRootCover_heightOnePrime_trichotomy

Documentation

Full-cover refinement of the height-two contraction trichotomy. In the selected branch, the prime on the full cover is now identified exactly with the principal ideal generated by the newly adjoined root.

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
attribute [local instance] Classical.propDecidable

Lean source · full declaration

theorem splitStrictNormalCrossings_heightTwo_fullRootCover_heightOnePrime_trichotomy
    {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)
    (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 ℕ∞) ∧
      (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) ∨
            (∃ k : Fin d,
              (i.succAbove (σ k)).1 < r ∧
              t (i.succAbove (σ k)) ∈ P ∧
              n k = e (σ k) ∧
              Prime (iteratedRadicalRoot R n a k) ∧
              q.under B = Ideal.span
                ({iteratedRadicalRoot R n a k} : Set B)) ∨
            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
  refine ⟨σ, hgeometryB, hn, hdimB, hgeometryD, ?_⟩
  intro q _ hqHeight
  rcases htrichotomy q hqHeight with
    ⟨hqUnderPrime, hqUnderHeight, hselected | hother | haway⟩
  · refine ⟨hqUnderPrime, hqUnderHeight, Or.inl ?_⟩
    simpa only [F, D] using
      (heightOnePrime_eq_span_root_of_under_eq_span_radicand
        hgeometryD.2.2.2.1 q hqHeight hselected)
  · exact ⟨hqUnderPrime, hqUnderHeight, Or.inr (Or.inl hother)⟩
  · exact ⟨hqUnderPrime, hqUnderHeight, Or.inr (Or.inr haway)⟩

Module documentation

Height-one primes over a one-root cover

Declarations

heightOnePrime_eq_span_root_of_under_eq_span_radicand

root_not_mem_of_radicand_not_mem_under

isUnit_root_localizationAtPrime_of_radicand_not_mem_under

splitStrictNormalCrossings_heightTwo_fullRootCover_heightOnePrime_trichotomy