Subgroups of an abelian group generated by finitely many involutions

Let G be a commutative group and f : ι → G a family whose values on a finite index set s are involutions, f i ^ 2 = 1. The subgroup they generate is then the set of sub-products ∏_{i ∈ S} f i over the subsets S ⊆ s (TauCeti.closure_image_eq_image_powerset), so it has at most 2 ^ #s elements, with equality exactly when distinct subsets give distinct sub-products (TauCeti.natCard_closure_image_eq_two_pow). A single relation — a nonempty R ⊆ s with ∏_{i ∈ R} f i = 1 — halves that count: replacing S by its symmetric difference with R leaves the sub-product unchanged and toggles membership of a fixed q ∈ R, so every value is already attained by a subset avoiding q (TauCeti.natCard_closure_image_le_two_pow_card_sub_one).

This is the counting step of genus theory, where f runs over the classes of the primes above the ramified rational primes of a quadratic field: those classes are involutions, and one relation between them cuts the bound from 2 ^ t to 2 ^ (t - 1). Both the ordinary class group (TauCeti.Multiquadratic.natCard_closure_image_classGroupMk0_le) and the narrow class group (TauCeti.Multiquadratic.natCard_closure_image_narrowMk0_le) consume it, with different relations.

Main results

• TauCeti.prod_sdiff_union_sdiff: a sub-product over a symmetric difference is the product of the two sub-products; this step needs only a commutative monoid.
• TauCeti.closure_image_eq_image_powerset: the subgroup generated by involutions is the set of sub-products.
• TauCeti.natCard_closure_image_eq_two_pow: with no relation at all — distinct subsets giving distinct sub-products — that subgroup has exactly 2 ^ #s elements.
• TauCeti.natCard_closure_image_le_two_pow_card_sub_one: one relation bounds that subgroup by 2 ^ (#s - 1) elements.

theorem TauCeti.prod_sdiff_union_sdiff {G : Type u_1} {ι : Type u_2} [CommMonoid G] [DecidableEq ι] (f : ι → G) {S D : Finset ι} (hsq : ∀ i ∈ S ∩ D, f i ^ 2 = 1) : ∏ i ∈ S \ D ∪ D \ S, f i = (∏ i ∈ S, f i) * ∏ i ∈ D, f i

Sub-products over a symmetric difference, when the factors shared by the two index sets are involutions: ∏_{S Δ D} f = (∏_S f) * (∏_D f), because the terms of S ∩ D occur twice on the right and cancel.

theorem TauCeti.closure_image_eq_image_powerset {G : Type u_1} {ι : Type u_2} [CommGroup G] (s : Finset ι) (f : ι → G) (hsq : ∀ i ∈ s, f i ^ 2 = 1) : ↑(Subgroup.closure (f '' ↑s)) = (fun (S : Finset ι) => ∏ i ∈ S, f i) '' ↑s.powerset

A subgroup generated by involutions is the set of sub-products of its generators. For a family f of involutions indexed by a finite set s, the subgroup ⟨f i : i ∈ s⟩ consists exactly of the products ∏_{i ∈ S} f i over the subsets S ⊆ s.

theorem TauCeti.natCard_closure_image_eq_two_pow {G : Type u_1} {ι : Type u_2} [CommGroup G] (s : Finset ι) (f : ι → G) (hsq : ∀ i ∈ s, f i ^ 2 = 1) (hinj : Set.InjOn (fun (S : Finset ι) => ∏ i ∈ S, f i) ↑s.powerset) : Nat.card ↥(Subgroup.closure (f '' ↑s)) = 2 ^ s.card

A family of involutions with distinct sub-products generates a group of order 2 ^ #s. Let f i be an involution for each i in a finite index set s, and suppose distinct subsets of s have distinct sub-products. Then the subgroup generated by the f i for i ∈ s has exactly 2 ^ #s elements: it is the set of sub-products, and the 2 ^ #s subsets of s index them without repetition.

theorem TauCeti.natCard_closure_image_le_two_pow_card_sub_one {G : Type u_1} {ι : Type u_2} [CommGroup G] (s : Finset ι) (f : ι → G) (hsq : ∀ i ∈ s, f i ^ 2 = 1) {R : Finset ι} (hR : R ⊆ s) (hRne : R.Nonempty) (hrel : ∏ i ∈ R, f i = 1) : Nat.card ↥(Subgroup.closure (f '' ↑s)) ≤ 2 ^ (s.card - 1)

One relation halves the number of sub-products of a family of involutions. Let f i be an involution for each i in a finite index set s, and suppose the sub-product over some nonempty R ⊆ s is trivial. Then the subgroup generated by the f i for i ∈ s has at most 2 ^ (#s - 1) elements.

Fix q ∈ R. Replacing an index set S by its symmetric difference with R multiplies the sub-product by the trivial ∏_{i ∈ R} f i, so leaves it unchanged, while toggling whether q belongs to the index set. Hence every sub-product is already attained by a subset of s avoiding q, and there are 2 ^ (#s - 1) such subsets.