ClosedNormalDataAndTransfiniteSeries.lean

structure ClosedNormalSubgroupData extends ClosedSubgroup G where
  /-- The underlying closed subgroup is normal. -/
  normal' : toSubgroup.Normal

instance instCoeClosedNormalSubgroupData : Coe (ClosedNormalSubgroupData G) (Subgroup G) where
  coe H := H.toSubgroup

theorem ClosedNormalSubgroupData.coe_mk
    (H : Subgroup G) (hHclosed : IsClosed (H : Set G)) (hHnormal : H.Normal) :
    ((⟨⟨H, hHclosed⟩, hHnormal⟩ : ClosedNormalSubgroupData G) : Subgroup G) = H

instance ClosedNormalSubgroupData.instNormal
    (H : ClosedNormalSubgroupData G) : H.toSubgroup.Normal

theorem ClosedNormalSubgroupData.isClosed
    (H : ClosedNormalSubgroupData G) : IsClosed ((H : Subgroup G) : Set G)

abbrev ClosedNormalSubgroupData.stepQuotient
    (H K : ClosedNormalSubgroupData G) : Type u

structure TransfiniteClosedNormalSeries
    (C : FiniteGroupClass.{u}) (G : Type u) [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] (μ : Ordinal) where
  /-- The closed normal subgroup at each ordinal stage. -/
  series : Ordinal → ClosedNormalSubgroupData G
  /-- The series starts at the whole group. -/
  top_eq : (series 0).toSubgroup = ⊤
  /-- The series reaches the trivial subgroup at stage \(\mu\). -/
  bot_eq : (series μ).toSubgroup = ⊥
  /-- The series is antitone up to its terminal stage \(\mu\). -/
  antitone' : ∀ ⦃lam ν : Ordinal⦄, lam ≤ ν → ν ≤ μ →
    (series ν).toSubgroup ≤ (series lam).toSubgroup
  /-- Every successor-step quotient before \(\mu\) belongs to the finite-group class \(C\). -/
  step_mem' : ∀ ⦃lam : Ordinal⦄, lam < μ →
    C (ClosedNormalSubgroupData.stepQuotient (G := G) (series lam) (series (succ lam)))
  /-- At a nonzero limit stage, the series is the intersection of all preceding stages. -/
  limit_eq_iInf' : ∀ ⦃lam : Ordinal⦄, lam ≤ μ → IsSuccLimit lam →
    (series lam).toSubgroup =
      iInf (fun ν : {ν : Ordinal // ν < lam} => (series ν.1).toSubgroup)

theorem closed_normal_subgroup_eq_inter_openNormal_of_finite_index
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (H K : Subgroup G)
    (hKclosed : IsClosed (K : Set G)) [K.Normal] (hKH : K ≤ H)
    [Finite (H ⧸ K.subgroupOf H)] :
    ∃ V : OpenNormalSubgroup G, K = H ⊓ (V : Subgroup G)

theorem localWeight_le_of_openNormal_family
    (G : Type u) [Group G] [TopologicalSpace G]
    {ι : Type u} {κ : Cardinal.{u}} (W : ι → OpenNormalSubgroup G)
    (hWbasis : IsNeighborhoodBasisAt (X := G) (1 : G)
      (Set.range fun i : ι => (((W i : Subgroup G) : Set G))))
    (hWcard : Cardinal.mk ι ≤ κ) : localWeight G ≤ κ := by
  classical
  let f : ι → Set G := fun i => (((W i : Subgroup G) : Set G))
  let chooseIdx : { V : Set G // V ∈ Set.range f } → ι :=
    fun V => Classical.choose V.2
  have hchoose : ∀ V : { V : Set G // V ∈ Set.range f }, f (chooseIdx V) = V.1 := by
    intro V
    exact Classical.choose_spec V.2
  have hchoose_inj : Function.Injective chooseIdx := by
    intro V₁ V₂ hEq
    apply Subtype.ext
    calc
      V₁.1 = f (chooseIdx V₁) := (hchoose V₁).symm
      _ = f (chooseIdx V₂) := by simp only [hEq]
      _ = V₂.1 := hchoose V₂
  simpa [localWeight] using
  calc
    localWeightAt (X := G) (1 : G) ≤ familyCardinal (X := G) (Set.range f) :=
      localWeightAt_le_familyCardinal_of_basis (X := G) (x := (1 : G)) hWbasis
    _ ≤ Cardinal.mk ι := by
      unfold familyCardinal
      exact Cardinal.mk_le_of_injective (f := chooseIdx) hchoose_inj
    _ ≤ κ := hWcard

theorem localWeight_split_over_closedNormalSubgroup
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (H : ClosedNormalSubgroupData G)
    (hInf : Infinite ↥H.toSubgroup ∨ Infinite (G ⧸ H.toSubgroup)) :
    localWeight G =
      localWeight ↥H.toSubgroup + quotientLocalWeight (G := G) H.toSubgroup

theorem quotientLocalWeight_subadd_of_subgroup_chain
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (H M K : ClosedNormalSubgroupData G)
    (hHK : H.toSubgroup ≤ K.toSubgroup) :
    quotientLocalWeight (G := ↥M.toSubgroup) (K.toSubgroup.subgroupOf M.toSubgroup) ≤
      quotientLocalWeight (G := ↥M.toSubgroup) (H.toSubgroup.subgroupOf M.toSubgroup) +
      quotientLocalWeight (G := ↥K.toSubgroup) (H.toSubgroup.subgroupOf K.toSubgroup)

theorem build_transfiniteClosedNormalSeries_of_localWeight_le
    (C : FiniteGroupClass.{u}) (G : Type u)
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (μ : Ordinal) (hForm : FiniteGroupClass.Formation C)
    (hNorm : FiniteGroupClass.NormalSubgroupClosed C) (hG : HasOpenNormalBasisInClass C G)
    (hμ : localWeight G ≤ μ.card) :
    Nonempty (TransfiniteClosedNormalSeries C G μ)