DoubleCosetOrbitGeometry.lean

def orbitQuotientEquivDoubleCoset
    {Q : Type u} [Group Q] (S H : Subgroup Q) :
    Quotient (orbitRel S (Q ⧸ H)) ≃
      DoubleCoset.Quotient (S : Set Q) (H : Set Q) where
  toFun z := Quotient.liftOn' z
    (fun q => DoubleCoset.mk S H q.out) (by
      intro q₁ q₂ hq
      rw [orbitRel_apply, mem_orbit_iff] at hq
      obtain ⟨s, hs⟩ := hq
      symm
      apply DoubleCoset.eq.mpr
      have hcoset :
          (QuotientGroup.mk q₁.out : Q ⧸ H) =
            QuotientGroup.mk (s.1 * q₂.out) := by
        calc
          QuotientGroup.mk q₁.out = q₁ := Quotient.out_eq' q₁
          _ = s • q₂ := hs.symm
          _ = s • (QuotientGroup.mk q₂.out : Q ⧸ H) :=
            congrArg (s • ·) (Quotient.out_eq' q₂).symm
          _ = QuotientGroup.mk (s.1 * q₂.out) := rfl
      have hh : q₁.out⁻¹ * (s.1 * q₂.out) ∈ H :=
        QuotientGroup.eq.mp hcoset
      refine ⟨s.1, s.2, (q₁.out⁻¹ * (s.1 * q₂.out))⁻¹,
        H.inv_mem hh, ?_⟩
      simp [mul_assoc])
  invFun z := Quotient.liftOn' z
    (fun x => Quotient.mk'' (QuotientGroup.mk x : Q ⧸ H)) (by
      intro x y hxy
      rw [DoubleCoset.rel_iff] at hxy
      obtain ⟨s, hs, h, hh, rfl⟩ := hxy
      apply Quotient.eq''.mpr
      rw [orbitRel_apply, mem_orbit_iff]
      refine ⟨⟨s⁻¹, S.inv_mem hs⟩, ?_⟩
      apply QuotientGroup.eq.mpr
      simpa [mul_assoc] using hh)
  left_inv z := by
    refine Quotient.inductionOn' z ?_
    intro q
    change Quotient.mk'' (QuotientGroup.mk q.out : Q ⧸ H) = Quotient.mk'' q
    exact congrArg Quotient.mk'' (Quotient.out_eq' q)
  right_inv z := by
    refine Quotient.inductionOn' z ?_
    intro x
    change DoubleCoset.mk S H (Quotient.out
      (QuotientGroup.mk x : Q ⧸ H)) = DoubleCoset.mk S H x
    apply DoubleCoset.eq.mpr
    have hh : (Quotient.out (QuotientGroup.mk x : Q ⧸ H))⁻¹ * x ∈ H :=
      QuotientGroup.leftRel_apply.mp
        (Quotient.exact' (Quotient.out_eq' (QuotientGroup.mk x : Q ⧸ H)))
    exact ⟨1, S.one_mem,
      (Quotient.out (QuotientGroup.mk x : Q ⧸ H))⁻¹ * x,
      hh, by simp⟩

theorem orbitQuotientEquivDoubleCoset_mk
    {Q : Type u} [Group Q] (S H : Subgroup Q) (x : Q) :
    orbitQuotientEquivDoubleCoset S H
        (Quotient.mk'' (QuotientGroup.mk x : Q ⧸ H)) =
      DoubleCoset.mk S H x

theorem orbitQuotientEquivDoubleCoset_symm_mk
    {Q : Type u} [Group Q] (S H : Subgroup Q) (x : Q) :
    (orbitQuotientEquivDoubleCoset S H).symm (DoubleCoset.mk S H x) =
      Quotient.mk'' (QuotientGroup.mk x : Q ⧸ H)

def doubleCosetInversionEquiv
    {Q : Type u} [Group Q] (S H : Subgroup Q) :
    DoubleCoset.Quotient (S : Set Q) (H : Set Q) ≃
      DoubleCoset.Quotient (H : Set Q) (S : Set Q) where
  toFun z := Quotient.liftOn' z
    (fun x => DoubleCoset.mk H S x⁻¹) (by
      intro x y hxy
      rw [DoubleCoset.rel_iff] at hxy
      obtain ⟨s, hs, h, hh, rfl⟩ := hxy
      apply DoubleCoset.eq.mpr
      exact ⟨h⁻¹, H.inv_mem hh, s⁻¹, S.inv_mem hs,
        by simp [mul_assoc]⟩)
  invFun z := Quotient.liftOn' z
    (fun x => DoubleCoset.mk S H x⁻¹) (by
      intro x y hxy
      rw [DoubleCoset.rel_iff] at hxy
      obtain ⟨h, hh, s, hs, rfl⟩ := hxy
      apply DoubleCoset.eq.mpr
      exact ⟨s⁻¹, S.inv_mem hs, h⁻¹, H.inv_mem hh,
        by simp [mul_assoc]⟩)
  left_inv z := by
    refine Quotient.inductionOn' z ?_
    intro x
    change DoubleCoset.mk S H (x⁻¹)⁻¹ = DoubleCoset.mk S H x
    rw [inv_inv]
  right_inv z := by
    refine Quotient.inductionOn' z ?_
    intro x
    change DoubleCoset.mk H S (x⁻¹)⁻¹ = DoubleCoset.mk H S x
    rw [inv_inv]

def orbitQuotientSwapEquiv
    {Q : Type u} [Group Q] (S H : Subgroup Q) :
    Quotient (orbitRel S (Q ⧸ H)) ≃
      Quotient (orbitRel H (Q ⧸ S))

theorem orbitQuotientSwapEquiv_mk
    {Q : Type u} [Group Q] (S H : Subgroup Q) (x : Q) :
    orbitQuotientSwapEquiv S H
        (Quotient.mk'' (QuotientGroup.mk x : Q ⧸ H)) =
      Quotient.mk'' (QuotientGroup.mk x⁻¹ : Q ⧸ S)

def orbitQuotientEquivOfSurjectiveEquivariant
    {M : Type*} {N : Type*} {X : Type*} {Y : Type*} [Group M] [Group N]
    [MulAction M X] [MulAction N Y]
    (f : M →* N) (hf : Function.Surjective f) (e : X ≃ Y)
    (he : ∀ (m : M) (x : X), e (m • x) = f m • e x) :
    Quotient (orbitRel M X) ≃ Quotient (orbitRel N Y)

theorem orbitQuotientEquivOfSurjectiveEquivariant_mk
    {M : Type*} {N : Type*} {X : Type*} {Y : Type*} [Group M] [Group N]
    [MulAction M X] [MulAction N Y]
    (f : M →* N) (hf : Function.Surjective f) (e : X ≃ Y)
    (he : ∀ (m : M) (x : X), e (m • x) = f m • e x) (x : X) :
    orbitQuotientEquivOfSurjectiveEquivariant f hf e he
        (Quotient.mk'' x) = Quotient.mk'' (e x)

theorem orbitQuotientEquivOfSurjectiveEquivariant_symm_mk
    {M : Type*} {N : Type*} {X : Type*} {Y : Type*} [Group M] [Group N]
    [MulAction M X] [MulAction N Y]
    (f : M →* N) (hf : Function.Surjective f) (e : X ≃ Y)
    (he : ∀ (m : M) (x : X), e (m • x) = f m • e x) (y : Y) :
    (orbitQuotientEquivOfSurjectiveEquivariant f hf e he).symm
        (Quotient.mk'' y) = Quotient.mk'' (e.symm y)

def leftCosetEquivOfMulEquiv
    {Q : Type*} {R : Type*} [Group Q] [Group R]
    (e : Q ≃* R) (S : Subgroup Q) :
    Q ⧸ S ≃ R ⧸ S.map e.toMonoidHom where
  toFun := Quotient.map' e (by
    intro x y hxy
    rw [QuotientGroup.leftRel_apply] at hxy ⊢
    exact ⟨x⁻¹ * y, hxy, by simp⟩)
  invFun := Quotient.map' e.symm (by
    intro x y hxy
    rw [QuotientGroup.leftRel_apply] at hxy ⊢
    obtain ⟨z, hz, heq⟩ := hxy
    have hzEq : e.symm (x⁻¹ * y) = z := by
      rw [← heq]
      simp
    have hxyEq : (e.symm x)⁻¹ * e.symm y = z := by
      calc
        (e.symm x)⁻¹ * e.symm y = e.symm (x⁻¹ * y) := by simp
        _ = z := hzEq
    rw [hxyEq]
    exact hz)
  left_inv q := by
    refine Quotient.inductionOn' q ?_
    intro x
    change QuotientGroup.mk (e.symm (e x)) = QuotientGroup.mk x
    rw [e.symm_apply_apply]
  right_inv q := by
    refine Quotient.inductionOn' q ?_
    intro x
    change QuotientGroup.mk (e (e.symm x)) = QuotientGroup.mk x
    rw [e.apply_symm_apply]

theorem leftCosetEquivOfMulEquiv_mk
    {Q : Type*} {R : Type*} [Group Q] [Group R]
    (e : Q ≃* R) (S : Subgroup Q) (x : Q) :
    leftCosetEquivOfMulEquiv e S (QuotientGroup.mk x) =
      QuotientGroup.mk (e x)

theorem doubleCoset_closedCyclic_eq
    {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
    (H : Subgroup Q) [H.FiniteIndex] (hHclosed : IsClosed (H : Set Q))
    (g x y : Q) :
    DoubleCoset.mk H (Subgroup.zpowers g) x =
        DoubleCoset.mk H (Subgroup.zpowers g) y ↔
      DoubleCoset.mk H
          (closedSubgroupGenerated ({g} : Set Q)).toSubgroup x =
        DoubleCoset.mk H
          (closedSubgroupGenerated ({g} : Set Q)).toSubgroup y

def doubleCosetClosedCyclicEquiv
    {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
    (H : Subgroup Q) [H.FiniteIndex] (hHclosed : IsClosed (H : Set Q))
    (g : Q) :
    DoubleCoset.Quotient (H : Set Q) (Subgroup.zpowers g : Set Q) ≃
      DoubleCoset.Quotient (H : Set Q)
        ((closedSubgroupGenerated ({g} : Set Q)).toSubgroup : Set Q) where
  toFun z := Quotient.liftOn' z
    (fun x => DoubleCoset.mk H
      (closedSubgroupGenerated ({g} : Set Q)).toSubgroup x)
    (fun x y hxy =>
      (doubleCoset_closedCyclic_eq H hHclosed g x y).mp
        (Quotient.sound' hxy))
  invFun z := Quotient.liftOn' z
    (fun x => DoubleCoset.mk H (Subgroup.zpowers g) x)
    (fun x y hxy =>
      (doubleCoset_closedCyclic_eq H hHclosed g x y).mpr
        (Quotient.sound' hxy))
  left_inv z := by
    refine Quotient.inductionOn' z ?_
    intro x
    rfl
  right_inv z := by
    refine Quotient.inductionOn' z ?_
    intro x
    rfl

def orbitQuotientClosedCyclicEquiv
    {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
    (H : Subgroup Q) [H.FiniteIndex] (hHclosed : IsClosed (H : Set Q))
    (g : Q) :
    Quotient (orbitRel H (Q ⧸ Subgroup.zpowers g)) ≃
      Quotient (orbitRel H
        (Q ⧸ (closedSubgroupGenerated ({g} : Set Q)).toSubgroup))

theorem orbitQuotientClosedCyclicEquiv_mk
    {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
    (H : Subgroup Q) [H.FiniteIndex] (hHclosed : IsClosed (H : Set Q))
    (g x : Q) :
    orbitQuotientClosedCyclicEquiv H hHclosed g
        (Quotient.mk'' (QuotientGroup.mk x : Q ⧸ Subgroup.zpowers g)) =
      Quotient.mk'' (QuotientGroup.mk x :
        Q ⧸ (closedSubgroupGenerated ({g} : Set Q)).toSubgroup)