Generating tuples

A group generated by a pair of elements is generated by a tuple of any larger length, the extra entries being the identity. Generation statements by a fixed number of elements are stated for tuples, in which repetitions are allowed, so that they are monotone in the number of entries. A surjective homomorphism carries generating sets, and so generating tuples, to generating sets. Two elements τ and σ with τ³ = σ² = 1 and σ τ σ = τ² σ τ², the relations of the tetrahedral group, generate a subgroup whose elements are the products τ^a and τ^a σ τ^b with a, b < 3. If left multiplication by every element of a set S maps R * K into itself, for a finite subgroup K and a finite nonempty set R, then the subgroup generated by S stabilizes the finite set R * K and so has at most |R| * |K| elements.

Main results

• Subgroup.exists_closure_range_eq_top_of_closure_pair_eq_top: a group generated by two elements is generated by an (n + 2)-tuple.
• Subgroup.mem_closure_pair_iff_of_tetrahedral: the normal forms τ^a and τ^a σ τ^b of the subgroup generated by two elements satisfying the tetrahedral relations.
• MonoidHom.closure_image_eq_top_of_surjective, AddMonoidHom.closure_image_eq_top_of_surjective: a surjective homomorphism carries a generating set to a generating set.
• Subgroup.exists_injective_closure_to_mul, Subgroup.finite_closure_of_forall_mul_mem: a set S whose left multiplications map R * K into itself generates a subgroup embedding into R * K, hence a finite one.
• Subgroup.natCard_closure_le_ncard_mul: the covering bound |⟨S⟩| ≤ |R| * |K| for a set S whose left multiplications map R * K into itself.

theorem Subgroup.exists_closure_range_eq_top_of_closure_pair_eq_top {G : Type u_1} [Group G] (n : ℕ) {σ τ : G} (hστ : closure {σ, τ} = ⊤) : ∃ (g : Fin (n + 2) → G), closure (Set.range g) = ⊤

A group generated by two elements is generated by an (n + 2)-tuple, for every n: pad the pair with identity elements.

theorem Subgroup.mem_closure_pair_iff_of_tetrahedral {G : Type u_1} [Group G] {τ σ g : G} (hτ3 : τ ^ 3 = 1) (hσ2 : σ * σ = 1) (hrel : σ * τ * σ = τ ^ 2 * σ * τ ^ 2) : g ∈ closure {τ, σ} ↔ ∃ a < 3, ∃ b < 3, g = τ ^ a ∨ g = τ ^ a * σ * τ ^ b

If τ³ = σ² = 1 and σ τ σ = τ² σ τ², every element of the subgroup generated by τ and σ is one of the twelve products τ^a and τ^a σ τ^b with a, b < 3: left multiplication by either generator preserves these normal forms.

theorem Subgroup.exists_injective_closure_to_mul {G : Type u_1} [Group G] {S R : Set G} {K : Subgroup G} (hR : R.Finite) (hR' : R.Nonempty) [Finite ↥K] (h : ∀ s ∈ S, ∀ r ∈ R, s * r ∈ R * ↑K) : ∃ (f : ↥(closure S) → ↑(R * ↑K)), Function.Injective f

If left multiplication by every element of S maps R * K into itself, for a finite subgroup K and a finite nonempty set R, then S generates a subgroup stabilizing the finite set R * K, and right multiplication by a point of R * K embeds that subgroup into R * K.

theorem Subgroup.finite_closure_of_forall_mul_mem {G : Type u_1} [Group G] {S R : Set G} {K : Subgroup G} (hR : R.Finite) (hR' : R.Nonempty) [Finite ↥K] (h : ∀ s ∈ S, ∀ r ∈ R, s * r ∈ R * ↑K) : Finite ↥(closure S)

A subgroup is finite if it is generated by a set S such that left multiplication by every element of S maps R * K into itself, for a finite subgroup K and a finite nonempty set R.

theorem Subgroup.natCard_closure_le_ncard_mul {G : Type u_1} [Group G] {S R : Set G} {K : Subgroup G} (hR : R.Finite) (hR' : R.Nonempty) [Finite ↥K] (h : ∀ s ∈ S, ∀ r ∈ R, s * r ∈ R * ↑K) : Nat.card ↥(closure S) ≤ R.ncard * Nat.card ↥K

The covering bound. If left multiplication by every element of S maps R * K into itself, for a finite subgroup K and a finite nonempty set R, then the subgroup generated by S has at most |R| * |K| elements.

A related covering bound, Subgroup.natCard_closure_le_mul, phrased with inverse transitions and correction words, appears in https://github.com/TauCetiProject/TauCeti/pull/12300 (feat: prove the M24 permutation image has order 244823040).

theorem MonoidHom.closure_image_eq_top_of_surjective {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) (hf : Function.Surjective ⇑f) {s : Set G} (hs : Subgroup.closure s = ⊤) : Subgroup.closure (⇑f '' s) = ⊤

A surjective homomorphism carries a generating set to a generating set.

theorem AddMonoidHom.closure_image_eq_top_of_surjective {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (f : G →+ H) (hf : Function.Surjective ⇑f) {s : Set G} (hs : AddSubgroup.closure s = ⊤) : AddSubgroup.closure (⇑f '' s) = ⊤

A surjective additive homomorphism carries a generating set to a generating set.