LeftQuotientProjectionSections.lean

theorem exists_mem_of_not_le {G : Type u} [Group G] [TopologicalSpace G] {K L : ClosedSubgroup G}
    (hnotle : ¬ (L : Subgroup G) ≤ (K : Subgroup G)) :
    ∃ x : G, x ∈ (L : Subgroup G) ∧ x ∉ (K : Subgroup G)

theorem exists_openNormalSubgroup_not_mem
    {x : G} (hx : x ≠ 1) :
    ∃ U : OpenNormalSubgroup G, x ∉ (U : Subgroup G)

theorem exists_openSubgroup_ge_closedSubgroup_not_mem
    (K : ClosedSubgroup G) {x : G} (hx : x ∉ (K : Set G)) :
    ∃ U : OpenSubgroup G, (K : Subgroup G) ≤ (U : Subgroup G) ∧ x ∉ (U : Set G)

def closedSubgroupOfOpenSubgroup
    (T : ClosedSubgroup G) (N : OpenSubgroup T) :
    ClosedSubgroup G where
  toSubgroup := (N : Subgroup T).map ((T : Subgroup G).subtype)
  isClosed' := by
    have : IsTopologicalGroup ↥(T : Subgroup G) :=
      Topology.IsInducing.subtypeVal.isTopologicalGroup (T : Subgroup G).subtype
    have hNclosed : IsClosed ((N : Subgroup T) : Set T) :=
      Subgroup.isClosed_of_isOpen (N : Subgroup T) N.isOpen'
    have hNcompact : IsCompact ((N : Subgroup T) : Set T) := hNclosed.isCompact
    have hEq :
        ((T : Subgroup G).subtype '' ((N : Subgroup T) : Set T)) =
          (((N : Subgroup T).map ((T : Subgroup G).subtype) : Subgroup G) : Set G) := by
      ext x
      constructor <;> rintro ⟨y, hy, rfl⟩ <;> exact ⟨y, hy, rfl⟩
    change IsClosed ((((N : Subgroup T).map ((T : Subgroup G).subtype) : Subgroup G) : Set G))
    rw [← hEq]
    exact hNcompact.image continuous_subtype_val |>.isClosed

theorem mem_closedSubgroupOfOpenSubgroup
    {T : ClosedSubgroup G} {N : OpenSubgroup T} {x : T} :
    (x : G) ∈ (closedSubgroupOfOpenSubgroup (G := G) T N : Subgroup G) ↔
      x ∈ (N : Subgroup T)

theorem closedSubgroupOfOpenSubgroup_le
    (T : ClosedSubgroup G) (N : OpenSubgroup T) :
    (closedSubgroupOfOpenSubgroup (G := G) T N : Subgroup G) ≤ (T : Subgroup G)

theorem closedSubgroupOfOpenSubgroup_subgroupOf_eq
    (T : ClosedSubgroup G) (N : OpenSubgroup T) :
    (((closedSubgroupOfOpenSubgroup (G := G) T N : ClosedSubgroup G) : Subgroup G).subgroupOf
      (T : Subgroup G)) = (N : Subgroup T)

def quotientBotHomeomorph :
    G ≃ₜ G ⧸ (⊥ : Subgroup G)

theorem quotientBotHomeomorph_apply (g : G) :
    quotientBotHomeomorph (G := G) g = QuotientGroup.mk (s := (⊥ : Subgroup G)) g

structure LeftQuotientSectionData (K H : ClosedSubgroup G) where
  /-- The intermediate closed subgroup through which the section is constructed. -/
  L : ClosedSubgroup G
  /-- The lower endpoint \(K\) is contained in the intermediate subgroup \(L\). -/
  hKL : (K : Subgroup G) ≤ (L : Subgroup G)
  /-- The intermediate subgroup \(L\) is contained in the upper endpoint \(H\). -/
  hLH : (L : Subgroup G) ≤ (H : Subgroup G)
  /-- A section from the left quotient by \(H\) to the left quotient by \(L\). -/
  σ : G ⧸ (H : Subgroup G) → G ⧸ (L : Subgroup G)
  /-- The section \(\sigma\) is continuous. -/
  continuous_σ : Continuous σ
  /-- The map \(\sigma\) is a right inverse of the quotient projection from \(G/L\) to \(G/H\). -/
  rightInv : Function.RightInverse σ
    (leftQuotientProjection (L : Subgroup G) (H : Subgroup G) hLH)
  /-- The section sends the identity coset modulo \(H\) to the identity coset modulo \(L\). -/
  one_eq :
    σ (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) =
      QuotientGroup.mk (s := (L : Subgroup G)) (1 : G)

instance instLELeftQuotientSectionData : LE (LeftQuotientSectionData (G := G) K H) where
  le a b :=
    ∃ hba : (b.L : Subgroup G) ≤ (a.L : Subgroup G),
      leftQuotientProjection (b.L : Subgroup G) (a.L : Subgroup G) hba ∘ b.σ = a.σ

instance instPreorderLeftQuotientSectionData : Preorder (LeftQuotientSectionData (G := G) K H) where
  le_refl a := by
    refine ⟨le_rfl, ?_⟩
    funext x
    simp only [leftQuotientProjection_id, Function.comp_apply, id_eq]
  le_trans a b c hab hbc := by
    rcases hab with ⟨hba, hbaσ⟩
    rcases hbc with ⟨hcb, hcbσ⟩
    refine ⟨hcb.trans hba, ?_⟩
    funext x
    calc
      leftQuotientProjection (c.L : Subgroup G) (a.L : Subgroup G) (hcb.trans hba) (c.σ x)
                = leftQuotientProjection (b.L : Subgroup G) (a.L : Subgroup G) hba
                    (leftQuotientProjection (c.L : Subgroup G) (b.L : Subgroup G) hcb (c.σ x)) := by
                convert
                  (leftQuotientProjection_comp_apply
                    (K := (c.L : Subgroup G)) (H := (b.L : Subgroup G))
                    (L := (a.L : Subgroup G)) hcb hba (c.σ x)).symm
      _ = leftQuotientProjection (b.L : Subgroup G) (a.L : Subgroup G) hba (b.σ x) := by
            exact congrArg (leftQuotientProjection (b.L : Subgroup G) (a.L : Subgroup G) hba)
              (congrFun hcbσ x)
      _ = a.σ x := congrFun hbaσ x

def top (hKH : (K : Subgroup G) ≤ (H : Subgroup G)) :
    LeftQuotientSectionData (G := G) K H where
  L := H
  hKL := hKH
  hLH := le_rfl
  σ := id
  continuous_σ := continuous_id
  rightInv := by
    intro x
    simp only [id_eq, leftQuotientProjection_id]
  one_eq := rfl

theorem exists_upperBound_of_chain
    (c : Set (LeftQuotientSectionData (G := G) K H))
    (hc : IsChain (· ≤ ·) c) (hcn : c.Nonempty) :
    ∃ ub : LeftQuotientSectionData (G := G) K H, ∀ a ∈ c, a ≤ ub

theorem leftQuotientProjection_hasContinuousSection
    (K H : ClosedSubgroup G)
    (hKH : (K : Subgroup G) ≤ (H : Subgroup G)) :
    ∃ σ : G ⧸ (H : Subgroup G) → G ⧸ (K : Subgroup G),
      Continuous σ ∧
        Function.RightInverse σ
          (leftQuotientProjection (K : Subgroup G) (H : Subgroup G) hKH) ∧
        σ (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) =
          QuotientGroup.mk (s := (K : Subgroup G)) (1 : G)

theorem exists_continuousSection_quotientMk_of_isClosed
    (H : Subgroup G) (hH : IsClosed (H : Set G)) :
        ∃ σ : (G ⧸ H) → G,
          Continuous σ ∧
            Function.RightInverse σ (QuotientGroup.mk (s := H)) ∧
            σ (QuotientGroup.mk (s := H) (1 : G)) = 1