FiniteFrattini.lean

theorem powerSubgroup_le_isCoatom_of_isPGroup
    {p : ℕ} {G : Type u} [Group G] [Finite G] [Fact (Nat.Prime p)]
    (hG : IsPGroup p G) {M : Subgroup G} (hM : IsCoatom M) :
    powerSubgroup p G ≤ M

theorem commutator_le_isCoatom_of_isPGroup
    {p : ℕ} {G : Type u} [Group G] [Finite G] [Fact (Nat.Prime p)]
    (hG : IsPGroup p G) {M : Subgroup G} (hM : IsCoatom M) :
    commutator G ≤ M

theorem closedPowerCommutator_le_isCoatom_of_isPGroup
    {p : ℕ} {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [T1Space G] [Finite G] [Fact (Nat.Prime p)]
    (hG : IsPGroup p G) {M : Subgroup G} (hM : IsCoatom M) :
    closedPowerCommutator p G ≤ M

theorem closedPowerCommutator_le_frattini_of_isPGroup
    {p : ℕ} {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [T1Space G] [Finite G] [Fact (Nat.Prime p)]
    (hG : IsPGroup p G) :
    closedPowerCommutator p G ≤ frattini G

theorem powerCommutatorQuotient_frattini_eq_bot
    {p : ℕ} {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [T1Space G] [Finite G] [Fact (Nat.Prime p)] :
    letI : (closedPowerCommutator p G).Normal :=
      closedPowerCommutator_normal p G
    frattini (powerCommutatorQuotient p G) = ⊥ := by
  let _ : (closedPowerCommutator p G).Normal :=
    closedPowerCommutator_normal p G
  let : IsMulCommutative (powerCommutatorQuotient p G) :=
    powerCommutatorQuotient_isMulCommutative p G
  have hpow (x : Additive (powerCommutatorQuotient p G)) : p • x = 0 := by
    change (Additive.toMul x) ^ p = 1
    exact powerCommutatorQuotient_pow_eq_one p G (Additive.toMul x)
  let : Module (ZMod p) (Additive (powerCommutatorQuotient p G)) :=
    AddCommGroup.zmodModule hpow
  let Fadd : AddSubgroup (Additive (powerCommutatorQuotient p G)) :=
    Subgroup.toAddSubgroup (frattini (powerCommutatorQuotient p G))
  let Fmod : Submodule (ZMod p) (Additive (powerCommutatorQuotient p G)) :=
    AddSubgroup.toZModSubmodule p Fadd
  obtain ⟨Kmod, hKmod⟩ := Fmod.exists_isCompl
  obtain ⟨hdisjmod, hcodisjmod⟩ := hKmod
  let Kadd : AddSubgroup (Additive (powerCommutatorQuotient p G)) :=
    Kmod.toAddSubgroup
  let K : Subgroup (powerCommutatorQuotient p G) :=
    AddSubgroup.toSubgroup' Kadd
  have hsup : frattini (powerCommutatorQuotient p G) ⊔ K = ⊤ := by
    apply top_unique
    intro x _
    obtain ⟨a, b, ha, hb, hab⟩ :=
      Submodule.codisjoint_iff_exists_add_eq.mp hcodisjmod (Additive.ofMul x)
    have haF : Additive.toMul a ∈ frattini (powerCommutatorQuotient p G) := by
      simpa [Fmod, Fadd] using ha
    have hbK : Additive.toMul b ∈ K := by
      simpa [K, Kadd] using hb
    change Additive.toMul a * Additive.toMul b = x at hab
    rw [← hab]
    exact Subgroup.mul_mem _
      ((le_sup_left : frattini (powerCommutatorQuotient p G) ≤
        frattini (powerCommutatorQuotient p G) ⊔ K) haF)
      ((le_sup_right : K ≤ frattini (powerCommutatorQuotient p G) ⊔ K) hbK)
  have hKtop : K = ⊤ :=
    frattini_nongenerating (by simpa [sup_comm] using hsup)
  rw [Subgroup.eq_bot_iff_forall]
  intro x hx
  have hxK : x ∈ K := by rw [hKtop]; exact Subgroup.mem_top x
  have hz : Additive.ofMul x = 0 :=
    (Submodule.disjoint_def.mp hdisjmod) (Additive.ofMul x)
      (by simpa [Fmod, Fadd] using hx)
      (by simpa [K, Kadd] using hxK)
  change x = 1 at hz
  exact hz

theorem frattini_le_closedPowerCommutator_of_finite
    {p : ℕ} {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [T1Space G] [Finite G] [Fact (Nat.Prime p)] :
    frattini G ≤ closedPowerCommutator p G

theorem frattini_eq_closedPowerCommutator_of_isPGroup
    {p : ℕ} {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [T1Space G] [Finite G] [Fact (Nat.Prime p)]
    (hG : IsPGroup p G) :
    frattini G = closedPowerCommutator p G