EtaleFundamentalGroups.Inertia.finiteIdealNormalizationExponent_exists_expChar_pow
The actual e/n exponent is a power of the actual residue exponential characteristic, derived from the same principal-unit wild group and both original inertia-cardinality formulas. No power assertion is an input.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Inertia
open RamificationTheory.HilbertRamification
universe u vLean source · statement
theorem finiteIdealNormalizationExponent_exists_expChar_pow
(A : Type u) (B : Type v)
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[CommRing B] [IsDedekindDomain B] [Algebra A B]
[Module.Finite A B] [Module.IsTorsionFree A B]
[IsGaloisGroup (B ≃ₐ[A] B) A B]
(Q : Ideal B) [Q.IsMaximal] [Q.LiesOver (IsLocalRing.maximalIdeal A)] (hQ : Q ≠ ⊥) :
∃ a : ℕ, finiteIdealNormalizationExponent A B (B ≃ₐ[A] B) Q hQ =
(ringExpChar Q.ResidueField) ^ a