RelatorReplacement.lean

def refl (R : Set (FreeGroup X)) :
    PresentedGroup R ≃* PresentedGroup R

def symm
    {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
    (e : PresentedGroup R ≃* PresentedGroup S) :
    PresentedGroup S ≃* PresentedGroup R

def trans
    {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)} {Z : Type*}
    {T : Set (FreeGroup Z)}
    (e₁ : PresentedGroup R ≃* PresentedGroup S)
    (e₂ : PresentedGroup S ≃* PresentedGroup T) :
    PresentedGroup R ≃* PresentedGroup T

def ofMutualMapData
    (R : Set (FreeGroup X)) (S : Set (FreeGroup Y))
    (D : RelatorQuotientMutualMapData R S) :
    PresentedGroup R ≃* PresentedGroup S

def ofTietzeEquiv
    {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
    (D : TietzeEquiv R S) :
    PresentedGroup R ≃* PresentedGroup S

def ofNormalClosureEq
    {R S : Set (FreeGroup X)}
    (h : Subgroup.normalClosure R = Subgroup.normalClosure S) :
    PresentedGroup R ≃* PresentedGroup S

def ofGeneratorMaps
    {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
    (toGenerator : X → FreeGroup Y)
    (invGenerator : Y → FreeGroup X)
    (hR :
      ∀ r ∈ R,
        FreeGroup.lift toGenerator r ∈ Subgroup.normalClosure S)
    (hS :
      ∀ s ∈ S,
        FreeGroup.lift invGenerator s ∈ Subgroup.normalClosure R)
    (hinv_to :
      ∀ x : X,
        RelatorEquivalent R
          (FreeGroup.lift invGenerator (toGenerator x))
          (FreeGroup.of x))
    (hto_inv :
      ∀ y : Y,
        RelatorEquivalent S
          (FreeGroup.lift toGenerator (invGenerator y))
          (FreeGroup.of y)) :
    PresentedGroup R ≃* PresentedGroup S

def ofGeneratorMapsRelatorEquivalent
    {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
    (toGenerator : X → FreeGroup Y)
    (invGenerator : Y → FreeGroup X)
    (hR :
      ∀ r ∈ R,
        RelatorEquivalent S (FreeGroup.lift toGenerator r) 1)
    (hS :
      ∀ s ∈ S,
        RelatorEquivalent R (FreeGroup.lift invGenerator s) 1)
    (hinv_to :
      ∀ x : X,
        RelatorEquivalent R
          (FreeGroup.lift invGenerator (toGenerator x))
          (FreeGroup.of x))
    (hto_inv :
      ∀ y : Y,
        RelatorEquivalent S
          (FreeGroup.lift toGenerator (invGenerator y))
          (FreeGroup.of y)) :
    PresentedGroup R ≃* PresentedGroup S

def replaceRelators
    {R S : Set (FreeGroup X)}
    (hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)
    (hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :
    PresentedGroup R ≃* PresentedGroup S

def replaceRelatorsTietzeEquiv
    {R S : Set (FreeGroup X)}
    (hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)
    (hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :
    TietzeEquiv R S

def replaceRelator
    {R : Set (FreeGroup X)} {oldRelator newRelator : FreeGroup X}
    (holdRelator :
      RelatorEquivalent (insert newRelator (R \ {oldRelator})) oldRelator 1)
    (hnewRelator : RelatorEquivalent R newRelator 1) :
    PresentedGroup R ≃*
      PresentedGroup (insert newRelator (R \ {oldRelator}))

def replaceRelatorTietzeEquiv
    {R : Set (FreeGroup X)} {oldRelator newRelator : FreeGroup X}
    (holdRelator :
      RelatorEquivalent (insert newRelator (R \ {oldRelator})) oldRelator 1)
    (hnewRelator : RelatorEquivalent R newRelator 1) :
    TietzeEquiv R (insert newRelator (R \ {oldRelator}))

theorem normalClosure_union_eq_left_of_subset
    {R S : Set (FreeGroup X)}
    (hS : S ⊆ Subgroup.normalClosure R) :
    Subgroup.normalClosure (R ∪ S) = Subgroup.normalClosure R

theorem normalClosure_sdiff_eq_of_subset
    {R D : Set (FreeGroup X)}
    (hD : ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure (R \ D)) :
    Subgroup.normalClosure R = Subgroup.normalClosure (R \ D)

def addRedundantRelators
    {R S : Set (FreeGroup X)}
    (hS : S ⊆ Subgroup.normalClosure R) :
    PresentedGroup (R ∪ S) ≃* PresentedGroup R

def addRedundantRelatorsRelatorEquivalent
    {R S : Set (FreeGroup X)}
    (hS : ∀ s ∈ S, RelatorEquivalent R s 1) :
    PresentedGroup (R ∪ S) ≃* PresentedGroup R

def addRedundantRelatorsTietzeEquiv
    {R S : Set (FreeGroup X)}
    (hS : S ⊆ Subgroup.normalClosure R) :
    TietzeEquiv (R ∪ S) R

def addRedundantRelatorsRelatorEquivalentTietzeEquiv
    {R S : Set (FreeGroup X)}
    (hS : ∀ s ∈ S, RelatorEquivalent R s 1) :
    TietzeEquiv (R ∪ S) R

def addRedundantRelatorsInverse
    {R S : Set (FreeGroup X)}
    (hS : S ⊆ Subgroup.normalClosure R) :
    PresentedGroup R ≃* PresentedGroup (R ∪ S)

def addRedundantRelatorsRelatorEquivalentInverse
    {R S : Set (FreeGroup X)}
    (hS : ∀ s ∈ S, RelatorEquivalent R s 1) :
    PresentedGroup R ≃* PresentedGroup (R ∪ S)

def removeRelatorSubset
    {R D : Set (FreeGroup X)}
    (hD : ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure (R \ D)) :
    PresentedGroup R ≃* PresentedGroup (R \ D)

def removeRelatorSubsetRelatorEquivalent
    {R D : Set (FreeGroup X)}
    (hD : ∀ d ∈ D, d ∈ R → RelatorEquivalent (R \ D) d 1) :
    PresentedGroup R ≃* PresentedGroup (R \ D)

def removeRelatorSubsetTietzeEquiv
    {R D : Set (FreeGroup X)}
    (hD : ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure (R \ D)) :
    TietzeEquiv R (R \ D)

def removeRelatorSubsetRelatorEquivalentTietzeEquiv
    {R D : Set (FreeGroup X)}
    (hD : ∀ d ∈ D, d ∈ R → RelatorEquivalent (R \ D) d 1) :
    TietzeEquiv R (R \ D)

def removeRelatorSubsetInverse
    {R D : Set (FreeGroup X)}
    (hD : ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure (R \ D)) :
    PresentedGroup (R \ D) ≃* PresentedGroup R

def removeRelatorSubsetRelatorEquivalentInverse
    {R D : Set (FreeGroup X)}
    (hD : ∀ d ∈ D, d ∈ R → RelatorEquivalent (R \ D) d 1) :
    PresentedGroup (R \ D) ≃* PresentedGroup R

def replaceRelatorSubset
    {R D E : Set (FreeGroup X)}
    (hD :
      ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure ((R \ D) ∪ E))
    (hE : E ⊆ Subgroup.normalClosure R) :
    PresentedGroup R ≃* PresentedGroup ((R \ D) ∪ E)

def replaceRelatorSubsetRelatorEquivalent
    {R D E : Set (FreeGroup X)}
    (hD :
      ∀ d ∈ D, d ∈ R → RelatorEquivalent ((R \ D) ∪ E) d 1)
    (hE : ∀ e ∈ E, RelatorEquivalent R e 1) :
    PresentedGroup R ≃* PresentedGroup ((R \ D) ∪ E)

def replaceRelatorSubsetTietzeEquiv
    {R D E : Set (FreeGroup X)}
    (hD :
      ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure ((R \ D) ∪ E))
    (hE : E ⊆ Subgroup.normalClosure R) :
    TietzeEquiv R ((R \ D) ∪ E)

def replaceRelatorSubsetRelatorEquivalentTietzeEquiv
    {R D E : Set (FreeGroup X)}
    (hD :
      ∀ d ∈ D, d ∈ R → RelatorEquivalent ((R \ D) ∪ E) d 1)
    (hE : ∀ e ∈ E, RelatorEquivalent R e 1) :
    TietzeEquiv R ((R \ D) ∪ E)

def addRedundantRelator
    {R : Set (FreeGroup X)} {r : FreeGroup X}
    (hr : r ∈ Subgroup.normalClosure R) :
    PresentedGroup (insert r R) ≃* PresentedGroup R

def addRedundantRelatorTietzeEquiv
    {R : Set (FreeGroup X)} {r : FreeGroup X}
    (hr : r ∈ Subgroup.normalClosure R) :
    TietzeEquiv (insert r R) R

def removeRedundantRelator
    {R : Set (FreeGroup X)} {r : FreeGroup X}
    (hr : r ∈ Subgroup.normalClosure (R \ {r})) :
    PresentedGroup R ≃* PresentedGroup (R \ {r})

def removeRedundantRelatorTietzeEquiv
    {R : Set (FreeGroup X)} {r : FreeGroup X}
    (hr : r ∈ Subgroup.normalClosure (R \ {r})) :
    TietzeEquiv R (R \ {r})

def renameGenerators
    (R : Set (FreeGroup X)) (e : X ≃ Y) :
    PresentedGroup R ≃*
      PresentedGroup (FreeGroup.freeGroupCongr e '' R)

def renameGeneratorsTietzeEquiv
    (R : Set (FreeGroup X)) (e : X ≃ Y) :
    TietzeEquiv R (FreeGroup.freeGroupCongr e '' R)