RelatorQuotientMutualMapData.lean

def quotientEquivOfRelatorsByMutualMaps
    (R : Set G) (S : Set H)
    (f : G →* H) (g : H →* G)
    (hR : ∀ r ∈ R, f r ∈ Subgroup.normalClosure S)
    (hS : ∀ s ∈ S, g s ∈ Subgroup.normalClosure R)
    (hgf : ∀ x : G, g (f x) * x⁻¹ ∈ Subgroup.normalClosure R)
    (hfg : ∀ y : H, f (g y) * y⁻¹ ∈ Subgroup.normalClosure S) :
    G ⧸ Subgroup.normalClosure R ≃* H ⧸ Subgroup.normalClosure S

structure RelatorQuotientMutualMapData
    (R : Set G) (S : Set H) where
  /-- The forward homomorphism from the source presentation group to the target one. -/
  toHom : G →* H
  /-- The homomorphism in the reverse direction. -/
  invHom : H →* G
  /-- The forward homomorphism sends each source relator into the target normal closure. -/
  mapsRelators : ∀ r ∈ R, toHom r ∈ Subgroup.normalClosure S
  /-- The reverse homomorphism sends each target relator into the source normal closure. -/
  mapsTargetRelators : ∀ s ∈ S, invHom s ∈ Subgroup.normalClosure R
  /-- The reverse-after-forward composite is the identity modulo the source relators. -/
  inv_toHom : ∀ x : G, invHom (toHom x) * x⁻¹ ∈ Subgroup.normalClosure R
  /-- The forward-after-reverse composite is the identity modulo the target relators. -/
  to_invHom : ∀ y : H, toHom (invHom y) * y⁻¹ ∈ Subgroup.normalClosure S

def refl (R : Set G) :
    RelatorQuotientMutualMapData R R where
  toHom := MonoidHom.id G
  invHom := MonoidHom.id G
  mapsRelators := by
    intro r hr
    exact Subgroup.subset_normalClosure hr
  mapsTargetRelators := by
    intro r hr
    exact Subgroup.subset_normalClosure hr
  inv_toHom := by
    intro x
    simp only [MonoidHom.id_apply, mul_inv_cancel, one_mem]
  to_invHom := by
    intro x
    simp only [MonoidHom.id_apply, mul_inv_cancel, one_mem]

def symm
    (D : RelatorQuotientMutualMapData R S) :
    RelatorQuotientMutualMapData S R where
  toHom := D.invHom
  invHom := D.toHom
  mapsRelators := D.mapsTargetRelators
  mapsTargetRelators := D.mapsRelators
  inv_toHom := D.to_invHom
  to_invHom := D.inv_toHom

def trans
    (D₁ : RelatorQuotientMutualMapData R S)
    (D₂ : RelatorQuotientMutualMapData S T) :
    RelatorQuotientMutualMapData R T where
  toHom := D₂.toHom.comp D₁.toHom
  invHom := D₁.invHom.comp D₂.invHom
  mapsRelators := by
    intro r hr
    exact map_mem_normalClosure_of_relators D₂.toHom D₂.mapsRelators
      (D₁.mapsRelators r hr)
  mapsTargetRelators := by
    intro t ht
    exact map_mem_normalClosure_of_relators D₁.invHom D₁.mapsTargetRelators
      (D₂.mapsTargetRelators t ht)
  inv_toHom := by
    intro x
    let y : H := D₁.toHom x
    have h₂ :
        D₂.invHom (D₂.toHom y) * y⁻¹ ∈ Subgroup.normalClosure S :=
      D₂.inv_toHom y
    have h₂map :
        D₁.invHom (D₂.invHom (D₂.toHom y) * y⁻¹) ∈
          Subgroup.normalClosure R :=
      map_mem_normalClosure_of_relators D₁.invHom D₁.mapsTargetRelators h₂
    have h₂map' :
        D₁.invHom (D₂.invHom (D₂.toHom y)) *
            (D₁.invHom y)⁻¹ ∈
          Subgroup.normalClosure R := by
      simpa using h₂map
    have h₁ :
        D₁.invHom y * x⁻¹ ∈ Subgroup.normalClosure R :=
      D₁.inv_toHom x
    have hprod := Subgroup.mul_mem (Subgroup.normalClosure R) h₂map' h₁
    have hmul :
        (D₁.invHom (D₂.invHom (D₂.toHom y)) *
              (D₁.invHom y)⁻¹) *
            (D₁.invHom y * x⁻¹) =
          D₁.invHom (D₂.invHom (D₂.toHom y)) * x⁻¹ := by
      group
    simpa [MonoidHom.comp_apply, y, hmul] using hprod
  to_invHom := by
    intro z
    let y : H := D₂.invHom z
    have h₁ :
        D₁.toHom (D₁.invHom y) * y⁻¹ ∈ Subgroup.normalClosure S :=
      D₁.to_invHom y
    have h₁map :
        D₂.toHom (D₁.toHom (D₁.invHom y) * y⁻¹) ∈
          Subgroup.normalClosure T :=
      map_mem_normalClosure_of_relators D₂.toHom D₂.mapsRelators h₁
    have h₁map' :
        D₂.toHom (D₁.toHom (D₁.invHom y)) *
            (D₂.toHom y)⁻¹ ∈
          Subgroup.normalClosure T := by
      simpa using h₁map
    have h₂ :
        D₂.toHom y * z⁻¹ ∈ Subgroup.normalClosure T :=
      D₂.to_invHom z
    have hprod := Subgroup.mul_mem (Subgroup.normalClosure T) h₁map' h₂
    have hmul :
        (D₂.toHom (D₁.toHom (D₁.invHom y)) *
              (D₂.toHom y)⁻¹) *
            (D₂.toHom y * z⁻¹) =
          D₂.toHom (D₁.toHom (D₁.invHom y)) * z⁻¹ := by
      group
    simpa [MonoidHom.comp_apply, y, hmul] using hprod

def relatorQuotientMutualMapDataOfNormalClosureEq
    {R S : Set G}
    (h : Subgroup.normalClosure R = Subgroup.normalClosure S) :
    RelatorQuotientMutualMapData R S where
  toHom := MonoidHom.id G
  invHom := MonoidHom.id G
  mapsRelators := by
    intro r hr
    rw [← h]
    exact Subgroup.subset_normalClosure hr
  mapsTargetRelators := by
    intro s hs
    rw [h]
    exact Subgroup.subset_normalClosure hs
  inv_toHom := by
    intro x
    simp only [MonoidHom.id_apply, mul_inv_cancel, one_mem]
  to_invHom := by
    intro x
    simp only [MonoidHom.id_apply, mul_inv_cancel, one_mem]

def relatorQuotientMutualMapDataOfRelatorEquivalent
    {R S : Set G}
    (hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)
    (hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :
    RelatorQuotientMutualMapData R S

def relatorQuotientMutualMapDataOfNormalClosureMapEq
    (R : Set G) (S : Set H) (e : G ≃* H)
    (hmap :
      Subgroup.map e.toMonoidHom (Subgroup.normalClosure R) =
        Subgroup.normalClosure S) :
    RelatorQuotientMutualMapData R S where
  toHom := e.toMonoidHom
  invHom := e.symm.toMonoidHom
  mapsRelators := by
    intro r hr
    have hrmap : e r ∈ Subgroup.map e.toMonoidHom (Subgroup.normalClosure R) :=
      ⟨r, Subgroup.subset_normalClosure hr, rfl⟩
    rw [← hmap]
    exact hrmap
  mapsTargetRelators := by
    intro s hs
    have hsmap : s ∈ Subgroup.map e.toMonoidHom (Subgroup.normalClosure R) := by
      rw [hmap]
      exact Subgroup.subset_normalClosure hs
    rcases hsmap with ⟨r, hr, hrs⟩
    simpa [← hrs] using hr
  inv_toHom := by
    intro x
    simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_ofClass, MulEquiv.symm_apply_apply,
        mul_inv_cancel, one_mem]
  to_invHom := by
    intro y
    simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_ofClass, MulEquiv.apply_symm_apply,
        mul_inv_cancel, one_mem]

theorem map_normalClosure_eq_of_mulEquiv_relator_images_mem_normalClosure
    (e : G ≃* H) (R : Set G) (S : Set H)
    (hR_to_S : ∀ r ∈ R, e r ∈ Subgroup.normalClosure S)
    (hS_to_R : ∀ s ∈ S, e.symm s ∈ Subgroup.normalClosure R) :
    Subgroup.map e.toMonoidHom (Subgroup.normalClosure R) =
      Subgroup.normalClosure S