ProCGroups.FreeConstructions.FiniteSubgroupBounds
structure FiniteSubgroupConjugacyData
(C : ProCGroups.FiniteGroupClass.{u})
{G A B : Type u} [Group G] [Group A] [Group B]
[TopologicalSpace G] [TopologicalSpace A] [TopologicalSpace B]
[IsTopologicalGroup G] [IsTopologicalGroup A] [IsTopologicalGroup B]
(ιA : A →ₜ* G) (ιB : B →ₜ* G)
(H : Subgroup G) : Prop where
isFreeProduct :
ProCGroups.FreeProducts.IsFreeProCProduct
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) ιA ιB
finite : IsFiniteSubgroup H
conjugate_into_factor :
IsConjugateIntoClosedContinuousImage H ιA ∨
IsConjugateIntoClosedContinuousImage H ιBtheorem finite_group_coprime_factor_generator_bound
(G : Type u) [Group G] (r : Nat) :
GeneratedByTwoFiniteCoprimeSubgroupsAtRank G r →
AbstractGeneratorRankLE G (r + r)Finite groups generated by two subgroups each generated by at most \(r\) elements are generated by the concatenated list of \(r+r\) generators. The stronger bound \(r\) is not forced by two independently supplied rank-\(r\) generating data: the definition gives two independent length-\(r\) generating tuples, so the direct mathematical consequence is the concatenated bound.
Show proof
by
intro hG
rcases hG with ⟨A, B, _hAfinite, _hBfinite, _hcoprime, hABtop, ⟨genA, hgenA⟩,
⟨genB, hgenB⟩⟩
let gen : Fin (r + r) → G :=
Fin.append (fun i => (genA i : G)) (fun i => (genB i : G))
let S : Set G := Set.range gen
refine ⟨gen, ?_⟩
have hA_le : (A : Set G) ⊆ Subgroup.closure S := by
intro a ha
let aA : A := ⟨a, ha⟩
have haA : aA ∈ Subgroup.closure (Set.range genA) := by
rw [hgenA]
trivial
exact Subgroup.closure_induction
(p := fun (x : A) _ => (x : G) ∈ Subgroup.closure S)
(fun x hx => by
rcases hx with ⟨i, rfl⟩
exact Subgroup.subset_closure (by
refine ⟨Fin.castAdd r i, ?_⟩
simp only [Fin.append_left, gen]))
(by simp only [OneMemClass.coe_one, one_mem])
(fun x y _ _ hx hy => by
simpa using (Subgroup.mul_mem (Subgroup.closure S) hx hy))
(fun x _ hx => by
simpa using (Subgroup.inv_mem (Subgroup.closure S) hx))
haA
have hB_le : (B : Set G) ⊆ Subgroup.closure S := by
intro b hb
let bB : B := ⟨b, hb⟩
have hbB : bB ∈ Subgroup.closure (Set.range genB) := by
rw [hgenB]
trivial
exact Subgroup.closure_induction
(p := fun (x : B) _ => (x : G) ∈ Subgroup.closure S)
(fun x hx => by
rcases hx with ⟨i, rfl⟩
exact Subgroup.subset_closure (by
refine ⟨Fin.natAdd r i, ?_⟩
simpa [gen] using
(Fin.append_right (fun i => (genA i : G)) (fun i => (genB i : G)) i)))
(by simp only [OneMemClass.coe_one, one_mem])
(fun x y _ _ hx hy => by
simpa using (Subgroup.mul_mem (Subgroup.closure S) hx hy))
(fun x _ hx => by
simpa using (Subgroup.inv_mem (Subgroup.closure S) hx))
hbB
apply le_antisymm
· exact le_top
· rw [← hABtop]
exact (Subgroup.closure_le (K := Subgroup.closure S)).2 (by
intro x hx
exact hx.elim (fun hxA => hA_le hxA) (fun hxB => hB_le hxB))Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. For density or closed-generation statements, the calculation is first made on the algebraic span of the group-like generators. The image of this span is dense in the completed target, and closedness of the kernel, image, or generated submodule allows the containment obtained on generators to pass to the completed closure.
□theorem finite_solvable_coprime_subgroups_generator_bound
{ι : Type v} [Finite ι] (G : Type u) [Group G] (subgroups : ι → Subgroup G) (r s : Nat) :
SubgroupFamilyCardinality (ι := ι) s →
SubgroupFamilyGenerates subgroups →
SubgroupFamilyEachGeneratedByAtMost subgroups r →
AbstractGeneratorRankLE G (s * r)If a finite family has cardinality \(s\), generates the ambient group, and each member is generated by at most \(r\) elements, then the ambient group is generated by the concatenated family of \(s\cdot r\) generators. Sharper bounds require additional group-theoretic input beyond the concatenation data alone.
Show proof
by
classical
intro hcard hgenerates hEach
letI : Fintype ι := Fintype.ofFinite ι
have hcard' : Fintype.card ι = s := by
simpa [SubgroupFamilyCardinality, Nat.card_eq_fintype_card] using hcard
have hprod : Fintype.card (ι × Fin r) = s * r := by
simp only [Fintype.card_prod, hcard', Fintype.card_fin]
let e : Fin (s * r) ≃ ι × Fin r :=
(Fin.castOrderIso hprod.symm).toEquiv.trans (Fintype.equivFin (ι × Fin r)).symm
let genSub : (i : ι) → Fin r → subgroups i :=
fun i => Classical.choose (hEach i)
have hgenSub : ∀ i, Subgroup.closure (Set.range (genSub i)) = ⊤ :=
fun i => Classical.choose_spec (hEach i)
let gen : Fin (s * r) → G := fun a => (genSub (e a).1 (e a).2 : G)
let S : Set G := Set.range gen
refine ⟨gen, ?_⟩
let K : Subgroup G := Subgroup.closure S
have hsub_le : ∀ i, (subgroups i : Set G) ⊆ K := by
intro i x hx
let xi : subgroups i := ⟨x, hx⟩
have hxi : xi ∈ Subgroup.closure (Set.range (genSub i)) := by
rw [hgenSub i]
trivial
exact Subgroup.closure_induction
(p := fun (y : subgroups i) _ => (y : G) ∈ K)
(fun y hy => by
rcases hy with ⟨j, rfl⟩
exact Subgroup.subset_closure (by
refine ⟨e.symm (i, j), ?_⟩
simpa [gen] using
congrArg (fun p : ι × Fin r => (genSub p.1 p.2 : G))
(e.apply_symm_apply (i, j))))
(by simp only [OneMemClass.coe_one, one_mem, K])
(fun y z _ _ hy hz => by
simpa [K] using Subgroup.mul_mem K hy hz)
(fun y _ hy => by
simpa [K] using Subgroup.inv_mem K hy)
hxi
apply le_antisymm
· exact le_top
· rw [← hgenerates]
exact (Subgroup.closure_le (K := K)).2 (by
intro x hx
rcases Set.mem_iUnion.mp hx with ⟨i, hxi⟩
exact hsub_le i hxi)Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□