EtaleFundamentalGroups.Inertia.finiteIdealTameOrder_eq_card_quotient_wild
The original-prime tame degree is the literal quotient cardinality for its independently transported principal-unit wild subgroup.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped Pointwise
namespace EtaleFundamentalGroups.Inertia
open RamificationTheory.HilbertRamification.DiscreteValuationRing
universe uLean source · statement
theorem finiteIdealTameOrder_eq_card_quotient_wild
(B : Type u) [CommRing B] [IsDedekindDomain B]
(G : Type u) [Group G] [MulSemiringAction G B]
(Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥) :
finiteIdealTameOrder B G Q hQ =
Nat.card (idealInertiaGroupObject B G Q ⧸ finiteIdealWildSubgroup B G Q hQ)