SlimnessAndTorsion.lean

def IsTorsionFreeGroup
    (G : Type u) [Group G] : Prop

def IsSlim
    (G : Type u) [TopologicalSpace G] [Group G] : Prop

def IsSlimModulo
    (G : Type u) [TopologicalSpace G] [Group G]
    (K : Subgroup G) : Prop

def IsRelativelySlim
    {G : Type u} [TopologicalSpace G] [Group G]
    {H : Type v} [TopologicalSpace H] [Group H]
    (f : G →ₜ* H) : Prop

theorem isSlim_iff_isRelativelySlim_id
    {G : Type u} [TopologicalSpace G] [Group G] :
    IsSlim G ↔
      IsRelativelySlim
        ({ toMonoidHom := MonoidHom.id G
           continuous_toFun := continuous_id } : G →ₜ* G)

theorem center_eq_bot_of_isSlim
    {G : Type u} [TopologicalSpace G] [Group G]
    (hSlim : IsSlim G) :
    Subgroup.center G = ⊥

theorem center_le_of_isSlimModulo
    {G : Type u} [TopologicalSpace G] [Group G]
    {K : Subgroup G} (hSlim : IsSlimModulo G K) :
    Subgroup.center G ≤ K

theorem isSlim_of_isSlimModulo_bot
    {G : Type u} [TopologicalSpace G] [Group G]
    (hSlim : IsSlimModulo G (⊥ : Subgroup G)) :
    IsSlim G

theorem isMulTorsionFree_of_isAbTorsionFree_isMulCommutative
    {G : Type u} [TopologicalSpace G] [Group G] [IsMulCommutative G]
    [IsTopologicalGroup G] [T1Space G]
    (hG : IsAbTorsionFree G) :
    IsMulTorsionFree G

theorem isTorsionFreeGroup_of_isMulTorsionFree
    {G : Type u} [Group G] [IsMulTorsionFree G] :
    IsTorsionFreeGroup G

theorem eq_one_mulAut_of_forall_mem_subgroup
    {A : Type u} [Group A] [IsMulTorsionFree A]
    (φ : MulAut A) (B : Subgroup A) [B.FiniteIndex]
    (hφ : ∀ b : A, b ∈ B → φ b = b) :
    φ = 1

theorem exists_openSubgroup_nontrivial_topologicalAbelianizationImage
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (T : ClosedSubgroup G)
    {a : TopologicalAbelianization ↥(T : Subgroup G)} (hne : a ≠ 1) :
    ∃ H : OpenSubgroup G,
      (T : Subgroup G) ≤ (H : Subgroup G) ∧
      ∃ f : TopologicalAbelianization ↥(T : Subgroup G) →*
          TopologicalAbelianization ↥(H : Subgroup G),
        f a ≠ 1

theorem isMulTorsionFree_topologicalAbelianization_of_closedSubgroup
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (hG : IsAbTorsionFree G)
    (T : ClosedSubgroup G) :
    IsMulTorsionFree (TopologicalAbelianization ↥(T : Subgroup G))

theorem isAbTorsionFree_closedSubgroup
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (hG : IsAbTorsionFree G)
    {K : Subgroup G} (hKClosed : IsClosed (K : Set G)) :
    IsAbTorsionFree ↥K

theorem isTorsionFreeGroup_of_isAbTorsionFree_of_closedCommSubgroup
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    {K : Subgroup G} (hKClosed : IsClosed (K : Set G))
    [IsMulCommutative ↥K]
    (hG : IsAbTorsionFree G) :
    IsTorsionFreeGroup ↥K

theorem isTorsionFreeGroup_of_isAbTorsionFree
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (hG : IsAbTorsionFree G) :
    IsTorsionFreeGroup G

theorem isTorsionFreeGroup_maxSolvQuot_of_isAbTorsionFree
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (hG : IsAbTorsionFree G)
    {m : ℕ} (hm : 1 ≤ m) :
    IsTorsionFreeGroup (MaxSolvQuot G m)

theorem isTorsionFreeGroup_of_isAbTorsionFree_of_closedSubgroup
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    {K : Subgroup G} (hKClosed : IsClosed (K : Set G))
    (hG : IsAbTorsionFree G) :
    IsTorsionFreeGroup ↥K

theorem isSlim_iff_openSubgroups_center_eq_bot
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    IsSlim G ↔ ∀ H : OpenSubgroup G, Subgroup.center ↥((H : Subgroup G)) = ⊥

theorem openSubgroup_center_eq_bot_of_isSlim
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (hslim : IsSlim G) (H : OpenSubgroup G) :
    Subgroup.center ↥((H : Subgroup G)) = ⊥

theorem isSlim_of_openSubgroups_center_eq_bot
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (hcenter : ∀ H : OpenSubgroup G, Subgroup.center ↥((H : Subgroup G)) = ⊥) :
    IsSlim G

theorem isSlim_of_isAbFaithful
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (hG : IsAbFaithful G) :
    IsSlim G

theorem mem_openNormal_of_action_trivial_on_finiteIndexSubgroup
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    (U : OpenNormalSubgroup Q)
    (hUtf : IsMulTorsionFree (TopologicalAbelianization ↥(U : Subgroup Q)))
    (hρinj :
      Function.Injective
        (quotientConjugationTopologicalAbelianizationMap (G := Q) (N := (U : Subgroup Q))))
    {c : Q}
    (B : Subgroup (TopologicalAbelianization ↥(U : Subgroup Q))) [B.FiniteIndex]
    (htriv :
      ∀ a : TopologicalAbelianization ↥(U : Subgroup Q),
        a ∈ B →
          quotientConjugationTopologicalAbelianizationMap (G := Q) (N := (U : Subgroup Q))
            (QuotientGroup.mk' (U : Subgroup Q) c) a = a) :
    c ∈ (U : Subgroup Q)

theorem centralizer_subgroup_le_of_torsionFree_and_inj_action_on_openNormalSupergroups
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    [CompactSpace Q] [TotallyDisconnectedSpace Q]
    {K : Subgroup Q} (hKClosed : IsClosed (K : Set Q)) (hKNormal : K.Normal)
    (hTF :
      ∀ U : OpenNormalSubgroup Q, K ≤ (U : Subgroup Q) →
        IsMulTorsionFree (TopologicalAbelianization ↥(U : Subgroup Q)))
    (hFaithful :
      ∀ U : OpenNormalSubgroup Q, K ≤ (U : Subgroup Q) →
        Function.Injective
          (quotientConjugationTopologicalAbelianizationMap
            (G := Q) (N := (U : Subgroup Q))))
    (S : Subgroup Q)
    (hLarge :
      ∀ U : OpenNormalSubgroup Q, K ≤ (U : Subgroup Q) →
        Finite
          ((TopologicalAbelianization ↥(U : Subgroup Q)) ⧸
            subgroupImageInTopologicalAbelianization (Q := Q) S U)) :
    Subgroup.centralizer (S : Set Q) ≤ K

theorem centralizer_openSubgroup_le_of_torsionFree_and_inj_action_on_openNormalSupergroups
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    [CompactSpace Q] [TotallyDisconnectedSpace Q]
    {K : Subgroup Q} (hKClosed : IsClosed (K : Set Q)) (hKNormal : K.Normal)
    (hTF :
      ∀ U : OpenNormalSubgroup Q, K ≤ (U : Subgroup Q) →
        IsMulTorsionFree (TopologicalAbelianization ↥(U : Subgroup Q)))
    (hFaithful :
      ∀ U : OpenNormalSubgroup Q, K ≤ (U : Subgroup Q) →
        Function.Injective
          (quotientConjugationTopologicalAbelianizationMap
            (G := Q) (N := (U : Subgroup Q))))
    (H : OpenSubgroup Q) :
    Subgroup.centralizer (H : Set Q) ≤ K

theorem centralizer_subgroup_le_of_open_topologicalClosure
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    [CompactSpace Q] [T2Space Q] [TotallyDisconnectedSpace Q]
    {K S : Subgroup Q} (hKClosed : IsClosed (K : Set Q)) (hKNormal : K.Normal)
    (hTF :
      ∀ U : OpenNormalSubgroup Q, K ≤ (U : Subgroup Q) →
        IsMulTorsionFree (TopologicalAbelianization ↥(U : Subgroup Q)))
    (hFaithful :
      ∀ U : OpenNormalSubgroup Q, K ≤ (U : Subgroup Q) →
        Function.Injective
          (quotientConjugationTopologicalAbelianizationMap
            (G := Q) (N := (U : Subgroup Q))))
    (hSOpen : IsOpen (((S.topologicalClosure : Subgroup Q) : Set Q))) :
    Subgroup.centralizer (S : Set Q) ≤ K

def topologicalAbelianizationInclusion
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {S T : Subgroup G} (hST : S ≤ T) :
    TopologicalAbelianization ↥S →ₜ* TopologicalAbelianization ↥T

theorem fixedPoint_eq_one_of_openNormal_torsionFreeAb
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (N : OpenNormalSubgroup G) [Finite (G ⧸ (N : Subgroup G))]
    (hNtf : IsMulTorsionFree (TopologicalAbelianization ↥(N : Subgroup G)))
    {a : TopologicalAbelianization ↥(N : Subgroup G)}
    (hfix :
      ∀ q : G ⧸ (N : Subgroup G),
        quotientConjugationTopologicalAbelianizationMap (G := G) (N := (N : Subgroup G)) q a = a)
    (ha :
      TopologicalAbelianization.map
        { toMonoidHom := (N : Subgroup G).subtype
          continuous_toFun := continuous_subtype_val } a = 1) :
    a = 1

theorem exists_openNormalSubgroup_nontrivial_topologicalAbelianizationInclusion
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    {K : Subgroup G} (hKClosed : IsClosed (K : Set G)) (hKNormal : K.Normal)
    {a : TopologicalAbelianization ↥K} (hne : a ≠ 1) :
    ∃ H : OpenNormalSubgroup G, ∃ hKH : K ≤ (H : Subgroup G),
      topologicalAbelianizationInclusion hKH a ≠ 1

theorem noFixedPoints_of_torsionFree_on_openNormalSupergroups
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    {K : Subgroup G} (hKClosed : IsClosed (K : Set G))
    (hKNormal : K.Normal) (hK : K ≤ topDerivedTop G 1)
    (hTF :
      ∀ H : OpenNormalSubgroup G, K ≤ (H : Subgroup G) →
        IsMulTorsionFree (TopologicalAbelianization ↥(H : Subgroup G))) :
    let _ : K.Normal := hKNormal
    HasNoNontrivialFixedPoints
      (quotientConjugationTopologicalAbelianizationMap (G := G) (N := K)) := by
  change HasNoNontrivialFixedPoints
    (quotientConjugationTopologicalAbelianizationMap (G := G) (N := K))
  intro a hfix
  by_contra hne
  obtain ⟨H, hKH, hHne⟩ :=
    exists_openNormalSubgroup_nontrivial_topologicalAbelianizationInclusion
      (G := G) (K := K) hKClosed hKNormal hne
  have hfixH :
      ∀ q : G ⧸ (H : Subgroup G),
        quotientConjugationTopologicalAbelianizationMap (G := G) (N := (H : Subgroup G)) q
            (topologicalAbelianizationInclusion hKH a) =
          topologicalAbelianizationInclusion hKH a := by
    intro q
    obtain ⟨g, rfl⟩ := QuotientGroup.mk'_surjective (H : Subgroup G) q
    obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective
      (Subgroup.closedCommutator K) a
    have hconj :
        topologicalAbelianizationInclusion hKH
          (quotientConjugationTopologicalAbelianizationMap (G := G) (N := K)
            (QuotientGroup.mk' K g) (TopologicalAbelianization.mk ↥K x)) =
        quotientConjugationTopologicalAbelianizationMap (G := G) (N := (H : Subgroup G))
          (QuotientGroup.mk' (H : Subgroup G) g)
          (topologicalAbelianizationInclusion hKH (TopologicalAbelianization.mk ↥K x)) := by
      simp only [QuotientGroup.mk'_apply]
      change
        topologicalAbelianizationInclusion hKH
            (TopologicalAbelianization.mk ↥K ((MulAut.conjNormal g) x)) =
          TopologicalAbelianization.mk ↥(H : Subgroup G)
            ((MulAut.conjNormal g) ((Subgroup.inclusion hKH) x))
      simp only [topologicalAbelianizationInclusion, ContinuousMonoidHom.coe_toMonoidHom,
          MonoidHom.coe_ofClass]
      rfl
    exact hconj.trans
      (congrArg (topologicalAbelianizationInclusion hKH) (hfix (QuotientGroup.mk' K g)))
  have haH :
      TopologicalAbelianization.map
        { toMonoidHom := (H : Subgroup G).subtype
          continuous_toFun := continuous_subtype_val }
        (topologicalAbelianizationInclusion hKH a) = 1 := by
    obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective
      (Subgroup.closedCommutator K) a
    have hx1 : TopologicalAbelianization.mk G x.1 = 1 := by
      exact
        (QuotientGroup.eq_one_iff
          (N := Subgroup.closedCommutator G) x.1).2
          (by simpa [topDerivedTop] using hK x.2)
    change
      TopologicalAbelianization.map
        { toMonoidHom := (H : Subgroup G).subtype
          continuous_toFun := continuous_subtype_val }
        (topologicalAbelianizationInclusion hKH (TopologicalAbelianization.mk ↥K x)) = 1
    rw [topologicalAbelianizationInclusion,
      TopologicalAbelianization.map_apply_mk,
      TopologicalAbelianization.map_apply_mk]
    change TopologicalAbelianization.mk G x.1 = 1
    exact hx1
  have hHtf : IsMulTorsionFree (TopologicalAbelianization ↥(H : Subgroup G)) := hTF H hKH
  exact hHne <|
    fixedPoint_eq_one_of_openNormal_torsionFreeAb
      (G := G) H hHtf hfixH haH

theorem noFixedPoints_of_isAbTorsionFree
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    {K : Subgroup G} (hKClosed : IsClosed (K : Set G))
    (hKNormal : K.Normal) (hK : K ≤ topDerivedTop G 1)
    (hG : IsAbTorsionFree G) :
    let _ : K.Normal := hKNormal
    HasNoNontrivialFixedPoints
      (quotientConjugationTopologicalAbelianizationMap (G := G) (N := K)) := by
  exact
    noFixedPoints_of_torsionFree_on_openNormalSupergroups
      (G := G) hKClosed hKNormal hK (fun H _ => hG H.toOpenSubgroup)

theorem isMulTorsionFree_topologicalAbelianization_of_aboveLastDerived_of_isAbTorsionFree
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G]
    (hG : IsAbTorsionFree G)
    {m : ℕ} (hm : 2 ≤ m)
    (H : OpenSubgroup (MaxSolvQuot G m))
    (hH : aboveLastDerived (G := G) m H) :
    IsMulTorsionFree
      (TopologicalAbelianization ↥(H : Subgroup (MaxSolvQuot G m)))

theorem isMulTorsionFree_topologicalAbelianization_of_openNormalSupergroup_of_isAbTorsionFree
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G]
    (hG : IsAbTorsionFree G)
    {m : ℕ} (hm : 2 ≤ m)
    (U : OpenNormalSubgroup (MaxSolvQuot G m))
    (hU : lastDerivedSubgroup (G := G) m ≤ (U : Subgroup (MaxSolvQuot G m))) :
    IsMulTorsionFree
      (TopologicalAbelianization ↥(U : Subgroup (MaxSolvQuot G m)))

theorem topDerivedTop_eq_bot_maxSolvQuot
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G]
    (m : ℕ) :
    topDerivedTop (MaxSolvQuot G m) m = ⊥

theorem center_eq_bot_maxSolvQuot_of_isAbTorsionFree_of_isAbFaithful
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (hTorsion : IsAbTorsionFree G) (hFaithful : IsAbFaithful G)
    {m : ℕ} (hm : 2 ≤ m) :
    Subgroup.center (MaxSolvQuot G m) = ⊥

theorem centralizer_subgroup_le_lastDerived_of_abTorsionFree_faithful
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (hTorsion : IsAbTorsionFree G) (hFaithful : IsAbFaithful G)
    {m : ℕ} (hm : 1 ≤ m)
    (S : Subgroup (MaxSolvQuot G m))
    (hSOpen :
      IsOpen (((S.topologicalClosure : Subgroup (MaxSolvQuot G m)) :
        Set (MaxSolvQuot G m)))) :
    Subgroup.centralizer (S : Set (MaxSolvQuot G m))
      ≤ lastDerivedSubgroup (G := G) m

theorem
    centralizer_openSubgroup_le_lastDerived_of_abTorsionFree_faithful
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (hTorsion : IsAbTorsionFree G) (hFaithful : IsAbFaithful G)
    {m : ℕ} (hm : 1 ≤ m)
    (H : OpenSubgroup (MaxSolvQuot G m)) :
    Subgroup.centralizer (H : Set (MaxSolvQuot G m))
      ≤ lastDerivedSubgroup (G := G) m

theorem isSlimModulo_lastDerivedSubgroup_maxSolvQuot_of_isAbTorsionFree_of_isAbFaithful
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (hTorsion : IsAbTorsionFree G) (hFaithful : IsAbFaithful G)
    {m : ℕ} (hm : 1 ≤ m) :
    IsSlimModulo (MaxSolvQuot G m)
      (lastDerivedSubgroup (G := G) m)

theorem center_le_lastDerivedSubgroup_of_isAbTorsionFree_of_isAbFaithful
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (hTorsion : IsAbTorsionFree G) (hFaithful : IsAbFaithful G)
    {m : ℕ} (hm : 1 ≤ m) :
    Subgroup.center (MaxSolvQuot G m) ≤
      lastDerivedSubgroup (G := G) m

theorem isSlim_maxSolvQuot_of_isAbTorsionFree_of_isAbFaithful_of_lastDerivedSubgroup_eq_bot
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (hTorsion : IsAbTorsionFree G) (hFaithful : IsAbFaithful G)
    {m : ℕ} (hm : 1 ≤ m)
    (hder : lastDerivedSubgroup (G := G) m = ⊥) :
    IsSlim (MaxSolvQuot G m)