Product-one triples generating a subgroup

The Frobenius formula counts all product-one triples in three conjugacy classes of a finite group. To count covers with prescribed monodromy, one must also require that the first two entries generate the specified subgroup. Every product-one triple belongs to exactly one generation stratum, indexed by the subgroup generated by its first two entries. This file states the resulting subgroup-lattice recursion for the counts.

The classes remain classes of the ambient group throughout: intersecting them with a subgroup does not in general produce a single conjugacy class of that subgroup.

def TauCeti.productOneGeneratedSubgroup {G : Type u_1} [Group G] (p : G × G × G) : Subgroup G

The subgroup generated by the first two entries of a triple. For a product-one triple, the third entry belongs to this subgroup as well.

Equations

• TauCeti.productOneGeneratedSubgroup p = Subgroup.closure {p.1, p.2.1}

theorem TauCeti.productOneGeneratedSubgroup_def {G : Type u_1} [Group G] (p : G × G × G) : productOneGeneratedSubgroup p = Subgroup.closure {p.1, p.2.1}

The subgroup generated by a triple is the closure of its first two entries.

@[simp]

theorem TauCeti.productOneGeneratedSubgroup_map {G : Type u_1} [Group G] {H : Type u_2} [Group H] (f : G →* H) (p : G × G × G) : productOneGeneratedSubgroup (f p.1, f p.2.1, f p.2.2) = Subgroup.map f (productOneGeneratedSubgroup p)

A homomorphism sends the subgroup generated by the first two entries to the subgroup generated by their images.

@[simp]

theorem TauCeti.productOneGeneratedSubgroup_le_iff {G : Type u_1} [Group G] (p : G × G × G) (H : Subgroup G) : productOneGeneratedSubgroup p ≤ H ↔ p.1 ∈ H ∧ p.2.1 ∈ H

noncomputable def TauCeti.productOneTriplesIn {G : Type u_1} [Group G] [Fintype G] (C0 C1 Cinf : ConjClasses G) (H : Subgroup G) : Finset (G × G × G)

The product-one triples in three ambient conjugacy classes whose entries lie in H. It suffices to check the first two entries, since the product-one equation determines the third.

Equations

• TauCeti.productOneTriplesIn C0 C1 Cinf H = {p ∈ TauCeti.productOneTriples C0 C1 Cinf | p.1 ∈ H ∧ p.2.1 ∈ H}

@[simp]

theorem TauCeti.mem_productOneTriplesIn {G : Type u_1} [Group G] [Fintype G] {C0 C1 Cinf : ConjClasses G} {H : Subgroup G} {p : G × G × G} : p ∈ productOneTriplesIn C0 C1 Cinf H ↔ p ∈ productOneTriples C0 C1 Cinf ∧ p.1 ∈ H ∧ p.2.1 ∈ H

theorem TauCeti.productOneTriplesIn.third_mem {G : Type u_1} [Group G] [Fintype G] {C0 C1 Cinf : ConjClasses G} {H : Subgroup G} {p : G × G × G} (hp : p ∈ productOneTriplesIn C0 C1 Cinf H) : p.2.2 ∈ H

The third entry also lies in H: the product-one equation forces it to be the inverse of the product of the first two entries.

noncomputable def TauCeti.generatingProductOneTriples {G : Type u_1} [Group G] [Fintype G] (C0 C1 Cinf : ConjClasses G) (H : Subgroup G) : Finset (G × G × G)

The triples in three ambient classes that generate exactly H.

Equations

• TauCeti.generatingProductOneTriples C0 C1 Cinf H = {p ∈ TauCeti.productOneTriples C0 C1 Cinf | TauCeti.productOneGeneratedSubgroup p = H}

@[simp]

theorem TauCeti.mem_generatingProductOneTriples {G : Type u_1} [Group G] [Fintype G] {C0 C1 Cinf : ConjClasses G} {H : Subgroup G} {p : G × G × G} : p ∈ generatingProductOneTriples C0 C1 Cinf H ↔ p ∈ productOneTriples C0 C1 Cinf ∧ productOneGeneratedSubgroup p = H

theorem TauCeti.generatingProductOneTriples_subset_in {G : Type u_1} [Group G] [Fintype G] (C0 C1 Cinf : ConjClasses G) (H : Subgroup G) : generatingProductOneTriples C0 C1 Cinf H ⊆ productOneTriplesIn C0 C1 Cinf H

A generating product-one triple lies in the subgroup it generates.

@[simp]

theorem TauCeti.productOneTriplesIn_top {G : Type u_1} [Group G] [Fintype G] (C0 C1 Cinf : ConjClasses G) : productOneTriplesIn C0 C1 Cinf ⊤ = productOneTriples C0 C1 Cinf

Restricting product-one triples to the whole group changes nothing.

theorem TauCeti.card_productOneTriplesIn_eq_sum_generating {G : Type u_1} [Group G] [Fintype G] (C0 C1 Cinf : ConjClasses G) (H : Subgroup G) : (productOneTriplesIn C0 C1 Cinf H).card = ∑ K : Subgroup G with K ≤ H, (generatingProductOneTriples C0 C1 Cinf K).card

Subgroup-lattice partition. Every product-one triple in H generates a unique subgroup K ≤ H. The conjugacy classes are those of G, even when K is proper.

theorem TauCeti.card_productOneTriples_eq_sum_generating {G : Type u_1} [Group G] [Fintype G] (C0 C1 Cinf : ConjClasses G) : (productOneTriples C0 C1 Cinf).card = ∑ K : Subgroup G, (generatingProductOneTriples C0 C1 Cinf K).card

The Frobenius count splits into generating counts over all subgroups.

theorem TauCeti.card_generatingProductOneTriples {G : Type u_1} [Group G] [Fintype G] (C0 C1 Cinf : ConjClasses G) (H : Subgroup G) : (generatingProductOneTriples C0 C1 Cinf H).card = (productOneTriplesIn C0 C1 Cinf H).card - ∑ K : Subgroup G with K < H, (generatingProductOneTriples C0 C1 Cinf K).card

Downward recursion. The count generating H is the total count of product-one triples in H minus the counts generating its proper subgroups.

theorem TauCeti.generatingProductOneTriples_card_eq_of_recursion {G : Type u_1} [Group G] [Fintype G] (C0 C1 Cinf : ConjClasses G) (f : Subgroup G → ℕ) (hf : ∀ (H : Subgroup G), f H = (productOneTriplesIn C0 C1 Cinf H).card - ∑ K : Subgroup G with K < H, f K) (H : Subgroup G) : f H = (generatingProductOneTriples C0 C1 Cinf H).card

The downward recursion determines the generating counts uniquely. Thus one can compute them from the total counts in subgroups without enumerating the generating triples themselves.