Cardinalities of Frobenius place stabilizers

This file supplies the local cardinality identities required by the Frobenius-coset form of Burnside averaging.

Suppose a place of a relative Galois extension has absolute degree [S : C] and lies above a degree-one place. Multiplicativity of place degree then says that its relative inertia degree is [S : C]. The decomposition-group formula and the finite-field identity

|Aut_C(S)| = [S : C]

show that its stabilizer has cardinality

|restricted quotient kernel| * |Aut_C(S)|,

provided the restricted quotient kernel is identified with inertia. Both finite places and places above infinity are covered, first for the underlying decomposition groups and then in the restriction-fiber actions used by sum_card_fixedBy_quotientFiber_eq_card_ker_of_stabilizer_card.

theorem BGS.HasseWeil.finitePlaceDecompositionGroup_card_eq_restrictedKernel_mul_card_constantAut (C : Type u_1) [Field C] [DecidableEq C] [DecidableEq (RatFunc C)] (M : Type u_2) [Field M] [Algebra (RatFunc C) M] [FiniteDimensional (RatFunc C) M] [Algebra.IsSeparable (RatFunc C) M] (L : Type u_3) [Field L] [Algebra (RatFunc C) L] [FiniteDimensional (RatFunc C) L] [Algebra.IsSeparable (RatFunc C) L] [Algebra M L] [IsScalarTower (RatFunc C) M L] [IsGalois M L] (S : Type u_4) [Field S] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] [Finite C] (π : Gal(L/M) →* Gal(S/C)) (Q : CorvajaZannier.FiniteExtensionFinitePlace C L) (hTop : CorvajaZannier.finiteExtensionPlaceDegree C L (Sum.inl Q) = Module.finrank C S) (hBase : CorvajaZannier.finiteExtensionPlaceDegree C M (Sum.inl (finitePlaceUnder C M L Q)) = 1) (hker : (π.comp (finitePlaceDecompositionGroup C M L Q).subtype).ker = Ideal.inertia (↥(finitePlaceDecompositionGroup C M L Q)) Q.asIdeal) : Nat.card ↥(finitePlaceDecompositionGroup C M L Q) = Nat.card ↥(π.comp (finitePlaceDecompositionGroup C M L Q).subtype).ker * Nat.card Gal(S/C)

A finite place of degree [S : C] above a degree-one place has the decomposition-group cardinality required by Frobenius-coset averaging, once the restricted constant quotient kernel is identified with inertia.

theorem BGS.HasseWeil.infinityPlaceDecompositionGroup_card_eq_restrictedKernel_mul_card_constantAut (C : Type u_1) [Field C] [DecidableEq C] [DecidableEq (RatFunc C)] (M : Type u_2) [Field M] [Algebra (RatFunc C) M] [FiniteDimensional (RatFunc C) M] [Algebra.IsSeparable (RatFunc C) M] (L : Type u_3) [Field L] [Algebra (RatFunc C) L] [FiniteDimensional (RatFunc C) L] [Algebra.IsSeparable (RatFunc C) L] [Algebra M L] [IsScalarTower (RatFunc C) M L] [IsGalois M L] (S : Type u_4) [Field S] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] [Finite C] (π : Gal(L/M) →* Gal(S/C)) (Q : ↑(CorvajaZannier.FiniteExtensionInfinityPlace C L)) (hTop : CorvajaZannier.finiteExtensionPlaceDegree C L (Sum.inr Q) = Module.finrank C S) (hBase : CorvajaZannier.finiteExtensionPlaceDegree C M (Sum.inr (infinityPlaceUnder C M L Q)) = 1) (hker : (π.comp (infinityPlaceDecompositionGroup C M L Q).subtype).ker = Ideal.inertia ↥(infinityPlaceDecompositionGroup C M L Q) ↑Q) : Nat.card ↥(infinityPlaceDecompositionGroup C M L Q) = Nat.card ↥(π.comp (infinityPlaceDecompositionGroup C M L Q).subtype).ker * Nat.card Gal(S/C)

The corresponding decomposition-group cardinality identity for a place above infinity.

theorem BGS.HasseWeil.finitePlaceUnderFiber_stabilizer_card_eq_restrictedKernel_mul_card_constantAut (C : Type u_1) [Field C] [DecidableEq C] [DecidableEq (RatFunc C)] (M : Type u_2) [Field M] [Algebra (RatFunc C) M] [FiniteDimensional (RatFunc C) M] [Algebra.IsSeparable (RatFunc C) M] (L : Type u_3) [Field L] [Algebra (RatFunc C) L] [FiniteDimensional (RatFunc C) L] [Algebra.IsSeparable (RatFunc C) L] [Algebra M L] [IsScalarTower (RatFunc C) M L] [IsGalois M L] (S : Type u_4) [Field S] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] [Finite C] (π : Gal(L/M) →* Gal(S/C)) (P : CorvajaZannier.FiniteExtensionFinitePlace C M) (Q : FinitePlaceUnderFiber C M L P) (hTop : CorvajaZannier.finiteExtensionPlaceDegree C L (Sum.inl ↑Q) = Module.finrank C S) (hBase : CorvajaZannier.finiteExtensionPlaceDegree C M (Sum.inl P) = 1) (hker : (π.comp (MulAction.stabilizer Gal(L/M) Q).subtype).ker = Ideal.inertia (↥(MulAction.stabilizer Gal(L/M) Q)) (↑Q).asIdeal) : Nat.card ↥(MulAction.stabilizer Gal(L/M) Q) = Nat.card ↥(π.comp (MulAction.stabilizer Gal(L/M) Q).subtype).ker * Nat.card Gal(S/C)

Restriction-fiber form of the finite-place cardinality identity. Its conclusion is exactly the stabilizer hypothesis consumed by the cardinality form of Frobenius-coset Burnside averaging.

theorem BGS.HasseWeil.infinityPlaceUnderFiber_stabilizer_card_eq_restrictedKernel_mul_card_constantAut (C : Type u_1) [Field C] [DecidableEq C] [DecidableEq (RatFunc C)] (M : Type u_2) [Field M] [Algebra (RatFunc C) M] [FiniteDimensional (RatFunc C) M] [Algebra.IsSeparable (RatFunc C) M] (L : Type u_3) [Field L] [Algebra (RatFunc C) L] [FiniteDimensional (RatFunc C) L] [Algebra.IsSeparable (RatFunc C) L] [Algebra M L] [IsScalarTower (RatFunc C) M L] [IsGalois M L] (S : Type u_4) [Field S] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] [Finite C] (π : Gal(L/M) →* Gal(S/C)) (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace C M)) (Q : InfinityPlaceUnderFiber C M L P) (hTop : CorvajaZannier.finiteExtensionPlaceDegree C L (Sum.inr ↑Q) = Module.finrank C S) (hBase : CorvajaZannier.finiteExtensionPlaceDegree C M (Sum.inr P) = 1) (hker : (π.comp (MulAction.stabilizer Gal(L/M) Q).subtype).ker = Ideal.inertia ↥(MulAction.stabilizer Gal(L/M) Q) ↑↑Q) : Nat.card ↥(MulAction.stabilizer Gal(L/M) Q) = Nat.card ↥(π.comp (MulAction.stabilizer Gal(L/M) Q).subtype).ker * Nat.card Gal(S/C)

Restriction-fiber form of the infinity-place cardinality identity.