Nyll.EtaleFundamentalGroups.Kummer.Main

Module documentation

Main one-point inertia statement

This leaf records the final source-facing composition. The strict-normal- crossings chart, boundary characteristic-zero hypotheses, and primitive Away etaleness feed the produced local selected-exponent theorem. Height-two globalization and the normalization-inertia cardinality comparison then produce the final coprimality statement; no local unit, ramification index, or inertia comparison is a hypothesis.

theorem

splitStrictNormalCrossings_normalizationInertia_coprime

L31 ↗

EtaleFundamentalGroups.Kummer.splitStrictNormalCrossings_normalizationInertia_coprime

Documentation

Normalization inertia along a component of a split strict-normal-crossings boundary has order prime to every prime residue characteristic reached from that component.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u uk

Lean source · statement

theorem splitStrictNormalCrossings_normalizationInertia_coprime
    {A K L : Type u} {k : Type uk}
    [CommRing A] [IsDomain A] [IsLocalRing A] [IsRegularRing A]
    [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    [FiniteDimensional K L] [IsGalois K L]
    [Module.Finite A (integralClosure A L)]
    [CommRing k] [Nontrivial k]
    {d r : ℕ} {f : A} {t : Fin (d + 1) → A}
    (hNC : IsSplitStrictNormalCrossingsAt f t r)
    (i : Fin (d + 1)) (hi : i.1 < r)
    (hCharZero : ∀ j, j.1 < r →
      CharZero (A ⧸ Ideal.span ({t j} : Set A)))
    (hAwayBase : (Localization.awayMap
      (algebraMap A (integralClosure A L)) f).Etale)
    (Q : Ideal (integralClosure A L)) [Q.IsPrime]
    [Q.LiesOver (Ideal.span ({t i} : Set A))]
    (phi : (A ⧸ Ideal.span ({t i} : Set A)) →+* k)
    (p : ℕ) [CharP k p] (hp : p.Prime) :
    Nat.Coprime
      (Nat.card (Q.toAddSubgroup.inertia Gal(L/K))) p

Module documentation

Main one-point inertia statement

Declarations

splitStrictNormalCrossings_normalizationInertia_coprime