Fixed-point averaging for finite transitive actions

This file isolates the Burnside-counting identity used in the fixed-field part of the Hasse--Weil argument.

theorem BGS.HasseWeil.sum_card_fixedBy_eq_card_group_of_isPretransitive (G : Type u_1) (X : Type u_2) [Group G] [Fintype G] [MulAction G X] [Finite X] [MulAction.IsPretransitive G X] [Nonempty X] : ∑ g : G, Nat.card ↑(MulAction.fixedBy X g) = Nat.card G

For a nonempty finite transitive G-set, the sum over group elements of the number of fixed points is exactly the order of G.

theorem BGS.HasseWeil.sum_card_fixedBy_fibers_eq_card_mul_card_group {ι : Type u_1} {G : Type u_2} [Fintype ι] [Group G] [Fintype G] (X : ι → Type u_3) [(i : ι) → MulAction G (X i)] [∀ (i : ι), Finite (X i)] [∀ (i : ι), MulAction.IsPretransitive G (X i)] [∀ (i : ι), Nonempty (X i)] : ∑ g : G, ∑ i : ι, Nat.card ↑(MulAction.fixedBy (X i) g) = Nat.card ι * Nat.card G

A finite family of nonempty transitive G-sets contributes |G| fixed points per fiber after summing over all group elements.

theorem BGS.HasseWeil.MonoidHom.ker_isPretransitive_of_stabilizer_surjective {G : Type u_1} {C : Type u_2} {X : Type u_3} [Group G] [Group C] [MulAction G X] [MulAction.IsPretransitive G X] (π : G →* C) (hstab : ∀ (x : X), Function.Surjective ⇑(π.comp (MulAction.stabilizer G x).subtype)) : MulAction.IsPretransitive (↥π.ker) X

If every point stabilizer maps onto a quotient group, then the kernel of that quotient map still acts transitively. This is the transitivity input for the Frobenius-coset form of Burnside averaging.

theorem BGS.HasseWeil.MonoidHom.surjective_of_card_eq_card_ker_mul_card {G : Type u_1} {C : Type u_2} [Group G] [Group C] [Finite G] [Finite C] (π : G →* C) (hcard : Nat.card G = Nat.card ↥π.ker * Nat.card C) : Function.Surjective ⇑π

A homomorphism of finite groups is surjective when the source cardinality is the product of the kernel and target cardinalities.

def BGS.HasseWeil.MonoidHom.sigmaFiberFixedByEquivSigmaStabilizerFiber {G : Type u_1} {C : Type u_2} {X : Type u_3} [Group G] [Group C] [MulAction G X] (π : G →* C) (c : C) : (g : ↑(⇑π ⁻¹' {c})) × ↑(MulAction.fixedBy X ↑g) ≃ (x : X) × ↑(⇑(π.comp (MulAction.stabilizer G x).subtype) ⁻¹' {c})

Incidence pairs between elements in one quotient fiber and their fixed points can be transposed into stabilizer elements in that fiber.

Equations

• One or more equations did not get rendered due to their size.

def BGS.HasseWeil.MonoidHom.sigmaStabilizerKerEquivSigmaKerFixedBy {G : Type u_1} {C : Type u_2} {X : Type u_3} [Group G] [Group C] [MulAction G X] (π : G →* C) : (x : X) × ↥(π.comp (MulAction.stabilizer G x).subtype).ker ≃ (g : ↥π.ker) × ↑(MulAction.fixedBy X g)

Stabilizer kernels, summed over points, are the same incidence type as fixed points of elements in the global kernel.

Equations

• One or more equations did not get rendered due to their size.

theorem BGS.HasseWeil.sum_card_fixedBy_quotientFiber_eq_card_ker {G : Type u_1} {C : Type u_2} {X : Type u_3} [Group G] [Group C] [Finite G] [MulAction G X] [Finite X] [MulAction.IsPretransitive G X] [Nonempty X] (π : G →* C) (hstab : ∀ (x : X), Function.Surjective ⇑(π.comp (MulAction.stabilizer G x).subtype)) (c : C) : ∑ g : ↑(⇑π ⁻¹' {c}), Nat.card ↑(MulAction.fixedBy X ↑g) = Nat.card ↥π.ker

Coset form of Burnside's lemma. For a finite transitive G-set, if the restriction of π : G → C to every point stabilizer is surjective, then the sum of fixed-point counts over any fiber of π is exactly |ker π|.

In Stichtenoth's fixed-field argument, π is the constant-field Frobenius quotient and the fiber is a Frobenius coset.

theorem BGS.HasseWeil.sum_card_fixedBy_quotientFiber_fibers_eq_card_mul_card_ker {ι : Type u_1} {G : Type u_2} {C : Type u_3} [Fintype ι] [Group G] [Group C] [Finite G] (X : ι → Type u_4) [(i : ι) → MulAction G (X i)] [∀ (i : ι), Finite (X i)] [∀ (i : ι), MulAction.IsPretransitive G (X i)] [∀ (i : ι), Nonempty (X i)] (π : G →* C) (hstab : ∀ (i : ι) (x : X i), Function.Surjective ⇑(π.comp (MulAction.stabilizer G x).subtype)) (c : C) : ∑ g : ↑(⇑π ⁻¹' {c}), ∑ i : ι, Nat.card ↑(MulAction.fixedBy (X i) ↑g) = Nat.card ι * Nat.card ↥π.ker

Finite-family form of Frobenius-coset Burnside averaging. If the constant-quotient map is surjective on every stabilizer in every transitive fiber, then summing the fixed-point counts first over the quotient fiber and then over the family contributes one copy of |ker π| per family member.

For a function-field cover, the family is the finite set of rational base places and X i is the corresponding restriction fiber of top places.

@[implicit_reducible]

def BGS.HasseWeil.invariantFiberMulAction {G : Type u_1} {X : Type u_2} {ι : Type u_3} [Group G] [MulAction G X] (base : X → ι) (hbase : ∀ (g : G) (x : X), base (g • x) = base x) (i : ι) : MulAction G { x : X // base x = i }

A group action restricted to a fiber of an invariant map.

Equations

• BGS.HasseWeil.invariantFiberMulAction base hbase i = { smul := fun (g : G) (x : { x : X // base x = i }) => ⟨g • ↑x, ⋯⟩, mul_smul := ⋯, one_smul := ⋯ }

def BGS.HasseWeil.fixedByEquivSigmaInvariantFiberFixedBy {G : Type u_1} {X : Type u_2} {ι : Type u_3} [Group G] [MulAction G X] (base : X → ι) (hbase : ∀ (g : G) (x : X), base (g • x) = base x) (g : G) : ↑(MulAction.fixedBy X g) ≃ (i : ι) × ↑(MulAction.fixedBy { x : X // base x = i } g)

Fixed points of an invariant global type are the disjoint union of the fixed points in its fibers. This is the nonduplicating assembly used when a top place is indexed by its restricted base place.

Equations

• One or more equations did not get rendered due to their size.

theorem BGS.HasseWeil.natCard_fixedBy_eq_sum_natCard_invariantFiberFixedBy {G : Type u_1} {X : Type u_2} {ι : Type u_3} [Group G] [MulAction G X] [Finite X] [Fintype ι] (base : X → ι) (hbase : ∀ (g : G) (x : X), base (g • x) = base x) (g : G) : Nat.card ↑(MulAction.fixedBy X g) = ∑ i : ι, Nat.card ↑(MulAction.fixedBy { x : X // base x = i } g)

Cardinal form of the invariant-fiber fixed-point decomposition.

theorem BGS.HasseWeil.sum_card_fixedBy_quotientFiber_eq_card_ker_of_stabilizer_card {G : Type u_1} {C : Type u_2} {X : Type u_3} [Group G] [Group C] [Finite G] [Finite C] [MulAction G X] [Finite X] [MulAction.IsPretransitive G X] [Nonempty X] (π : G →* C) (hcard : ∀ (x : X), Nat.card ↥(MulAction.stabilizer G x) = Nat.card ↥(π.comp (MulAction.stabilizer G x).subtype).ker * Nat.card C) (c : C) : ∑ g : ↑(⇑π ⁻¹' {c}), Nat.card ↑(MulAction.fixedBy X ↑g) = Nat.card ↥π.ker

Cardinality form of the Frobenius-coset Burnside lemma. It replaces stabilizer-surjectivity by the exact decomposition-group order identity used in the function-field argument.