EtaleFundamentalGroups.Inertia.finiteNormalizationWildOrder_exists_expChar_pow
Every nonzero prime of the actual finite normalization has primary wild order.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v wLean source · full declaration
theorem finiteNormalizationWildOrder_exists_expChar_pow
(A : Type u) [rA : CommRing A] [dedA : IsDedekindDomain A]
(K : Type v) (L : Type w) [fK : Field K] [fL : Field L]
[aAK : Algebra A K] [frAK : IsFractionRing A K]
[aKL : Algebra K L] [aAL : Algebra A L] [tAKL : IsScalarTower A K L]
[IsGalois K L] (E : FiniteGaloisIntermediateField K L) :
let : IsDedekindDomain (finiteAbsoluteNormalizationAlgebra A K L E).carrier :=
finiteAbsoluteNormalizationAlgebra_isDedekindDomain A K L E
∀ (Q : Ideal (finiteAbsoluteNormalizationAlgebra A K L E).carrier)
[Q.IsPrime] (hQ : Q ≠ ⊥),
∃ n : ℕ, commAlgIdealWildOrder A (finiteAbsoluteNormalizationAlgebra A K L E) Q hQ =
(ringExpChar Q.ResidueField) ^ n := by
exact nativeFiniteNormalizationWildOrder_exists_expChar_pow A K
(finiteLevelFieldAlgebra A K L E)
(Field.toIsField (finiteLevelFieldAlgebra A K L E).carrier)