GeneratorConvergingPairs.lean

structure GeneratorConvergingPair where
  /-- The subgroup that is retained alongside the chosen generators. -/
  N : Subgroup G
  /-- The retained subgroup is normal, so convergence may be interpreted in the quotient. -/
  normal_N : N.Normal
  /-- The retained subgroup is closed in `G`. -/
  closed_N : IsClosed (N : Set G)
  /-- The selected representatives outside the retained subgroup. -/
  X : Set G
  /-- No selected representative lies in `N`. -/
  subset_compl : X ⊆ (N : Set G)ᶜ
  /--
  For every open subgroup containing `N`, only finitely many selected representatives lie
  outside that open subgroup; equivalently, their images converge to one modulo `N`.
  -/
  convergesToOneAlongOpenSubgroups_mod :
    ∀ U : OpenSubgroup G, N ≤ (U : Subgroup G) → (X \ (U : Set G)).Finite
  /-- The union of the selected representatives and `N` topologically generates `G`. -/
  generates : TopologicallyGenerates (G := G) (X ∪ (N : Set G))

instance instLEGeneratorConvergingPair : LE (GeneratorConvergingPair (G := G)) where
  le A B := B.N ≤ A.N ∧ A.X ⊆ B.X ∧ B.X \ A.X ⊆ (A.N : Set G)

instance instPreorderGeneratorConvergingPair : Preorder (GeneratorConvergingPair (G := G)) where
  le_refl A := ⟨le_rfl, subset_rfl, by simp only [sdiff_self, empty_subset]⟩
  le_trans A B C hAB hBC := by
    rcases hAB with ⟨hABN, hABX, hABdiff⟩
    rcases hBC with ⟨hBCN, hBCX, hBCdiff⟩
    refine ⟨hBCN.trans hABN, hABX.trans hBCX, ?_⟩
    intro x hx
    rcases hx with ⟨hxC, hxA⟩
    by_cases hxB : x ∈ B.X
    · exact hABdiff ⟨hxB, hxA⟩
    · exact hABN (hBCdiff ⟨hxC, hxB⟩)

def initialGeneratorConvergingPair : GeneratorConvergingPair (G := G) where
  N := ⊤
  normal_N := by infer_instance
  closed_N := isClosed_univ
  X := ∅
  subset_compl := by intro x hx; simp only [mem_empty_iff_false] at hx
  convergesToOneAlongOpenSubgroups_mod := by
    intro U hU
    simp only [empty_sdiff, finite_empty]
  generates := by
    simpa [TopologicallyGenerates, Set.empty_union, Subgroup.closure_eq] using
      (top_unique (Subgroup.le_topologicalClosure (⊤ : Subgroup G)) :
        (⊤ : Subgroup G).topologicalClosure = ⊤)

theorem finite_subset_chain_has_upper {α : Type*} [Preorder α] {c : Set α}
    (hc : IsChain (· ≤ ·) c) :
    ∀ s : Finset α, ↑s ⊆ c → s.Nonempty → ∃ m ∈ s, ∀ z ∈ s, z ≤ m

theorem exists_pair_le_openSubgroup_of_chain_iInf_le
    {c : Set (GeneratorConvergingPair (G := G))}
    (hc : IsChain (· ≤ ·) c) (hcne : c.Nonempty)
    (U : OpenSubgroup G)
    (hInf : iInf (fun p : c => p.1.N) ≤ (U : Subgroup G)) :
    ∃ p : c, p.1.N ≤ (U : Subgroup G) := by
  classical
  have hInter :
      (⋂ p : c, (((p.1.N : Subgroup G) : Set G))) ⊆ ((U : Subgroup G) : Set G) := by
    intro x hx
    exact hInf (by simpa [Subgroup.mem_iInf] using hx)
  rcases finite_iInter_subgroup_subset_openSubgroup (G := G)
      (H := fun p : c => p.1.N)
      (hclosed := fun p => p.1.closed_N)
      U hInter with ⟨s, hs⟩
  by_cases hsne : s.Nonempty
  · have hc' : IsChain (· ≤ ·) (Set.univ : Set c) := by
      intro a ha b hb hne
      have hne' : (a : GeneratorConvergingPair (G := G)) ≠ b := by
        intro h
        exact hne (Subtype.ext h)
      simpa using hc a.2 b.2 hne'
    rcases finite_subset_chain_has_upper hc' s (by intro z hz; simp only [mem_univ]) hsne with
        ⟨m, hm, hmax⟩
    refine ⟨m, ?_⟩
    intro x hx
    have hx' :
        x ∈ ⋂ p ∈ s, (((p.1.N : Subgroup G) : Set G)) := by
      refine mem_iInter₂.2 ?_
      intro p hp
      exact (hmax p hp).1 hx
    exact hs hx'
  · rcases hcne with ⟨p, hp⟩
    refine ⟨⟨p, hp⟩, ?_⟩
    have htop : ((⊤ : Subgroup G) : Set G) ⊆ ((U : Subgroup G) : Set G) := by
      have : (⋂ p ∈ s, (((p.1.N : Subgroup G) : Set G))) ⊆ ((U : Subgroup G) : Set G) := hs
      simpa [Finset.not_nonempty_iff_eq_empty.mp hsne] using this
    intro x hx
    exact htop (by simp only [Subgroup.coe_top, mem_univ])

def chainUpperBoundOfNonempty
    {c : Set (GeneratorConvergingPair (G := G))}
    (hc : IsChain (· ≤ ·) c) (hcne : c.Nonempty) :
    GeneratorConvergingPair (G := G) where
  N := iInf fun p : c => p.1.N
  normal_N := by
    classical
    exact Subgroup.normal_iInf_normal fun p : c => p.1.normal_N
  closed_N := by
    classical
    simpa using isClosed_iInter (fun p : c => p.1.closed_N)
  X := ⋃ p : c, p.1.X
  subset_compl := by
    intro x hx
    rcases mem_iUnion.mp hx with ⟨p, hpx⟩
    refine by
      intro hxK
      exact p.1.subset_compl hpx ((iInf_le (fun q : c => q.1.N) p) hxK)
  convergesToOneAlongOpenSubgroups_mod := by
    intro U hKU
    rcases exists_pair_le_openSubgroup_of_chain_iInf_le (G := G) hc hcne U
      hKU with ⟨p, hpU⟩
    have hEq : ((⋃ q : c, q.1.X) \ (U : Set G)) = (p.1.X \ (U : Set G)) := by
      ext x
      constructor
      · intro hx
        rcases hx with ⟨hxX, hxU⟩
        rcases mem_iUnion.mp hxX with ⟨q, hqx⟩
        have hcmp :
            (q.1 ≤ p.1) ∨ (p.1 ≤ q.1) := by
          by_cases hqp : q = p
          · exact Or.inl (hqp ▸ le_rfl)
          · have hqp' : (q : GeneratorConvergingPair (G := G)) ≠ p := by
              intro h
              exact hqp (Subtype.ext h)
            exact hc q.2 p.2 hqp'
        cases hcmp with
        | inl hqp =>
            exact ⟨hqp.2.1 hqx, hxU⟩
        | inr hpq =>
            by_cases hxp : x ∈ p.1.X
            · exact ⟨hxp, hxU⟩
            · have hxN : x ∈ (p.1.N : Set G) := hpq.2.2 ⟨hqx, hxp⟩
              exact False.elim (hxU (hpU hxN))
      · intro hx
        exact ⟨mem_iUnion.mpr ⟨p, hx.1⟩, hx.2⟩
    rw [hEq]
    exact p.1.convergesToOneAlongOpenSubgroups_mod U hpU
  generates := by
    let K : Subgroup G := iInf fun p : c => p.1.N
    have : K.Normal := Subgroup.normal_iInf_normal fun p : c => p.1.normal_N
    apply (topologicallyGenerates_union_subgroup_iff_forall_openNormalQuotient
      (G := G)
      (N := K) (X := ⋃ p : c, p.1.X)).2
    intro U hKU
    rcases exists_pair_le_openSubgroup_of_chain_iInf_le (G := G) hc hcne U.toOpenSubgroup
      (by simpa [K] using hKU) with ⟨p, hpU⟩
    have hpgen :
        TopologicallyGenerates (G := G ⧸ (U : Subgroup G))
          ((QuotientGroup.mk' (U : Subgroup G)) '' p.1.X) := by
      have : p.1.N.Normal := p.1.normal_N
      exact
        (topologicallyGenerates_union_subgroup_iff_forall_openNormalQuotient
          (G := G)
          (N := p.1.N) (X := p.1.X)).1
          p.1.generates U hpU
    exact topologicallyGenerates_mono hpgen (by
      intro y hy
      rcases hy with ⟨x, hx, rfl⟩
      exact ⟨x, mem_iUnion.mpr ⟨p, hx⟩, rfl⟩)

theorem chain_bounded_generatorConvergingPair
    (c : Set (GeneratorConvergingPair (G := G)))
    (hc : IsChain (· ≤ ·) c) :
    BddAbove c

theorem exists_finite_subset_generating_subgroup_mod_openNormal
    {M : Subgroup G}
    (hMclosed : IsClosed (M : Set G)) (U : OpenNormalSubgroup G) :
    ∃ T : Set G,
      T.Finite ∧
      T ⊆ (M : Set G) \ (((U : Subgroup G) ⊓ M : Subgroup G) : Set G) ∧
      M ≤ Subgroup.closure (T ∪ ((((U : Subgroup G) ⊓ M : Subgroup G) : Subgroup G) : Set G))