Nyll.EtaleFundamentalGroups.Inertia.Normalization.Coprimality

Module documentation

Coprimality of normalization inertia from a ramification-index unit

At a characteristic-zero height-one divisor, the cardinality of the ideal-theoretic inertia subgroup equals the ramification index. A unit ramification index therefore remains prime to every prime residue characteristic reached from that divisor.

theorem

normalizationInertia_coprime_of_ramificationIdx_isUnit

L29 ↗

EtaleFundamentalGroups.normalizationInertia_coprime_of_ramificationIdx_isUnit

Documentation

A ramification index that is invertible on a prime divisor forces the normalization inertia group to have order prime to any prime characteristic of a residue ring receiving that divisor's function field.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL uk

Lean source · statement

theorem normalizationInertia_coprime_of_ramificationIdx_isUnit
    {A : Type uA} {K : Type uK} {L : Type uL} {k : Type uk}
    [CommRing A] [IsDomain 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]
    [CommRing k] [Nontrivial k]
    (t : A) (ht : Prime t)
    [CharZero (A ⧸ Ideal.span {t})]
    (Q : Ideal (integralClosure A L)) [Q.IsPrime]
    [Q.LiesOver (Ideal.span {t})]
    (hunit : IsUnit
      ((Q.ramificationIdx A : ℕ) : A ⧸ Ideal.span {t}))
    (phi : (A ⧸ Ideal.span {t}) →+* k)
    (p : ℕ) [CharP k p] (hp : p.Prime) :
    Nat.Coprime
      (Nat.card (Q.toAddSubgroup.inertia Gal(L/K))) p

Module documentation

Coprimality of normalization inertia from a ramification-index unit

Declarations

normalizationInertia_coprime_of_ramificationIdx_isUnit