FiniteSubgroupBounds.lean

theorem generatorRankLE_add_of_two_subgroups
    (G : Type u) [Group G] (r : Nat) (A B : Subgroup G)
    (hABtop : Subgroup.closure ((A : Set G) ∪ (B : Set G)) = ⊤)
    (hA : AbstractGeneratorRankLE A r)
    (hB : AbstractGeneratorRankLE B r) :
    AbstractGeneratorRankLE G (r + r)

theorem finite_subgroup_family_generator_bound
    {ι : Type v} [Finite ι] (G : Type u) [Group G]
    (subgroups : ι → Subgroup G) (r s : Nat)
    (hcard : Nat.card ι = s)
    (hgenerates : Subgroup.closure (Set.iUnion fun i => (subgroups i : Set G)) = ⊤)
    (hEach : ∀ i, AbstractGeneratorRankLE (subgroups i) r) :
    AbstractGeneratorRankLE G (s * r) := by
  classical
  have hprod : Nat.card (ι × Fin r) = s * r := by
    rw [Nat.card_prod, hcard, Nat.card_fin]
  let e : Fin (s * r) ≃ ι × Fin r := (Finite.equivFinOfCardEq hprod).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)