EtaleFundamentalGroups.Inertia.finiteIdealCanonicalTameCharacterGroupMap_ker
Actual exponential-characteristic normalization preserves the original finite principal-unit kernel. The required power is supplied by the actual finite arithmetic endpoint, independently of this group calculation.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
namespace EtaleFundamentalGroups.Inertia
open RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u v
variable (A : Type u) (B : Type v) [CommRing A] [CommRing B] [IsDedekindDomain B]
[Algebra A B] (G : Type v) [Group G] [Finite G] [MulSemiringAction G B]
(Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)
(p : ℕ) [ExpChar (IsLocalRing.ResidueField (Localization.AtPrime Q)) p]
(hq : ∃ a : ℕ, finiteIdealNormalizationExponent A B G Q hQ = p ^ a)
include p hqLean source · statement
theorem finiteIdealCanonicalTameCharacterGroupMap_ker :
(finiteIdealCanonicalTameCharacterGroupMap A B G Q hQ).ker =
finiteIdealWildSubgroup B G Q hQ