EtaleFundamentalGroups.Kummer.splitStrictNormalCrossings_normalizationInertia_coprime_of_isIntegrallyClosed
Over an integrally closed regular local domain, normalization inertia along a component of a split strict-normal-crossings boundary has order prime to every prime residue characteristic reached from that component.
The normalization is finite because a regular ring is noetherian and the generic extension is finite separable.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u ukLean source · statement
theorem splitStrictNormalCrossings_normalizationInertia_coprime_of_isIntegrallyClosed
{A K L : Type u} {k : Type uk}
[CommRing A] [IsDomain A] [IsLocalRing A] [IsRegularRing A]
[IsIntegrallyClosed 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]
{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