GeneratorAddition.lean

def includeAdjoinedGenerators : FreeGroup X →* FreeGroup (Sum X Y)

def eliminateAdjoinedGeneratorsHom (word : Y → FreeGroup X) :
    FreeGroup (Sum X Y) →* FreeGroup X

theorem eliminateAdjoinedGeneratorsHom_inl
    (word : Y → FreeGroup X) (x : X) :
    eliminateAdjoinedGeneratorsHom word (FreeGroup.of (Sum.inl x)) =
      FreeGroup.of x

theorem eliminateAdjoinedGeneratorsHom_inr
    (word : Y → FreeGroup X) (y : Y) :
    eliminateAdjoinedGeneratorsHom word (FreeGroup.of (Sum.inr y)) =
      word y

theorem eliminateAdjoinedGeneratorsHom_comp_include
    (word : Y → FreeGroup X) :
    (eliminateAdjoinedGeneratorsHom word).comp (includeAdjoinedGenerators X Y) =
      MonoidHom.id (FreeGroup X)

def adjoinGeneratorsRelators
    (R : Set (FreeGroup X)) (word : Y → FreeGroup X) :
    Set (FreeGroup (Sum X Y))

theorem adjoinGenerators_relation_mem
    (R : Set (FreeGroup X)) (word : Y → FreeGroup X) (y : Y) :
    FreeGroup.of (Sum.inr y) *
        (includeAdjoinedGenerators X Y (word y))⁻¹ ∈
      adjoinGeneratorsRelators R word

theorem include_eliminateAdjoinedGeneratorsHom_mod_relators
    (R : Set (FreeGroup X)) (word : Y → FreeGroup X)
    (z : FreeGroup (Sum X Y)) :
    includeAdjoinedGenerators X Y (eliminateAdjoinedGeneratorsHom word z) *
        z⁻¹ ∈
      Subgroup.normalClosure (adjoinGeneratorsRelators R word)

def adjoinGeneratorsMutualMapData
    (R : Set (FreeGroup X)) (word : Y → FreeGroup X) :
    RelatorQuotientMutualMapData R (adjoinGeneratorsRelators R word) where
  toHom := includeAdjoinedGenerators X Y
  invHom := eliminateAdjoinedGeneratorsHom word
  mapsRelators := by
    intro r hr
    exact Subgroup.subset_normalClosure (Or.inl ⟨r, hr, rfl⟩)
  mapsTargetRelators := by
    intro s hs
    rcases hs with hs | hs
    · rcases hs with ⟨r, hr, rfl⟩
      have hcomp := congrArg (fun f : FreeGroup X →* FreeGroup X => f r)
        (eliminateAdjoinedGeneratorsHom_comp_include word)
      have hrw :
          eliminateAdjoinedGeneratorsHom word (includeAdjoinedGenerators X Y r) = r := by
        simpa using hcomp
      simpa [hrw] using (Subgroup.subset_normalClosure hr :
        r ∈ Subgroup.normalClosure R)
    · rcases hs with ⟨y, rfl⟩
      have hw :
          eliminateAdjoinedGeneratorsHom word
              (includeAdjoinedGenerators X Y (word y)) = word y := by
        have hcomp := congrArg (fun f : FreeGroup X →* FreeGroup X => f (word y))
          (eliminateAdjoinedGeneratorsHom_comp_include word)
        simpa using hcomp
      simp only [map_mul, map_inv, eliminateAdjoinedGeneratorsHom_inr]
      change word y *
          (eliminateAdjoinedGeneratorsHom word
            (includeAdjoinedGenerators X Y (word y)))⁻¹ ∈
        Subgroup.normalClosure R
      simp only [hw, mul_inv_cancel, one_mem]
  inv_toHom := by
    intro x
    have hcomp := congrArg (fun f : FreeGroup X →* FreeGroup X => f x)
      (eliminateAdjoinedGeneratorsHom_comp_include word)
    have hx :
        eliminateAdjoinedGeneratorsHom word (includeAdjoinedGenerators X Y x) = x := by
      simpa using hcomp
    simp only [hx, mul_inv_cancel, one_mem]
  to_invHom := by
    intro z
    exact include_eliminateAdjoinedGeneratorsHom_mod_relators R word z

def adjoinGeneratorsTietzeEquiv
    (R : Set (FreeGroup X)) (word : Y → FreeGroup X) :
    TietzeEquiv R (adjoinGeneratorsRelators R word)

def adjoinGenerators
    (R : Set (FreeGroup X)) (word : Y → FreeGroup X) :
    PresentedGroup R ≃*
      PresentedGroup (adjoinGeneratorsRelators R word)

def definedGeneratorRelators
    (word : Y → FreeGroup X) :
    Set (FreeGroup (Sum X Y))

def relatorsWithDefinedGenerators
    (R : Set (FreeGroup (Sum X Y))) (word : Y → FreeGroup X) :
    Set (FreeGroup (Sum X Y))

def relatorsAfterSubstitutingDefinedGenerators
    (R : Set (FreeGroup (Sum X Y))) (word : Y → FreeGroup X) :
    Set (FreeGroup X)

theorem definedGeneratorRelator_mem
    (word : Y → FreeGroup X) (y : Y) :
    FreeGroup.of (Sum.inr y) *
        (includeAdjoinedGenerators X Y (word y))⁻¹ ∈
      definedGeneratorRelators word

theorem definedGeneratorRelator_mem_relatorsWithDefinedGenerators
    (R : Set (FreeGroup (Sum X Y))) (word : Y → FreeGroup X) (y : Y) :
    FreeGroup.of (Sum.inr y) *
        (includeAdjoinedGenerators X Y (word y))⁻¹ ∈
      relatorsWithDefinedGenerators R word

theorem relator_mem_relatorsWithDefinedGenerators
    {R : Set (FreeGroup (Sum X Y))} {word : Y → FreeGroup X}
    {r : FreeGroup (Sum X Y)} (hr : r ∈ R) :
    r ∈ relatorsWithDefinedGenerators R word

theorem include_eliminateAdjoinedGeneratorsHom_mod_definedGeneratorRelators
    (word : Y → FreeGroup X) (z : FreeGroup (Sum X Y)) :
    includeAdjoinedGenerators X Y (eliminateAdjoinedGeneratorsHom word z) *
        z⁻¹ ∈
      Subgroup.normalClosure (definedGeneratorRelators word)

theorem include_eliminateAdjoinedGeneratorsHom_mod_relatorsWithDefinedGenerators
    (R : Set (FreeGroup (Sum X Y))) (word : Y → FreeGroup X)
    (z : FreeGroup (Sum X Y)) :
    includeAdjoinedGenerators X Y (eliminateAdjoinedGeneratorsHom word z) *
        z⁻¹ ∈
      Subgroup.normalClosure (relatorsWithDefinedGenerators R word)

def substituteDefinedGeneratorsMutualMapData
    (R : Set (FreeGroup (Sum X Y))) (word : Y → FreeGroup X) :
    RelatorQuotientMutualMapData
      (relatorsWithDefinedGenerators R word)
      (relatorsAfterSubstitutingDefinedGenerators R word) where
  toHom := eliminateAdjoinedGeneratorsHom word
  invHom := includeAdjoinedGenerators X Y
  mapsRelators := by
    intro r hr
    rcases hr with hr | hr
    · exact Subgroup.subset_normalClosure ⟨r, hr, rfl⟩
    · rcases hr with ⟨y, rfl⟩
      have hw :
          eliminateAdjoinedGeneratorsHom word
              (includeAdjoinedGenerators X Y (word y)) = word y := by
        have hcomp := congrArg (fun f : FreeGroup X →* FreeGroup X => f (word y))
          (eliminateAdjoinedGeneratorsHom_comp_include word)
        simpa using hcomp
      simp only [map_mul, map_inv, eliminateAdjoinedGeneratorsHom_inr]
      change word y *
          (eliminateAdjoinedGeneratorsHom word
            (includeAdjoinedGenerators X Y (word y)))⁻¹ ∈
        Subgroup.normalClosure (relatorsAfterSubstitutingDefinedGenerators R word)
      simp only [hw, mul_inv_cancel, one_mem]
  mapsTargetRelators := by
    intro s hs
    rcases hs with ⟨r, hr, rfl⟩
    let N : Subgroup (FreeGroup (Sum X Y)) :=
      Subgroup.normalClosure (relatorsWithDefinedGenerators R word)
    have hmod :
        includeAdjoinedGenerators X Y (eliminateAdjoinedGeneratorsHom word r) *
            r⁻¹ ∈ N :=
      include_eliminateAdjoinedGeneratorsHom_mod_relatorsWithDefinedGenerators
        (X := X) (Y := Y) R word r
    have hrN : r ∈ N :=
      Subgroup.subset_normalClosure
        (relator_mem_relatorsWithDefinedGenerators (R := R) (word := word) hr)
    have hprod := Subgroup.mul_mem N hmod hrN
    convert hprod using 1
    group
  inv_toHom := by
    intro z
    exact include_eliminateAdjoinedGeneratorsHom_mod_relatorsWithDefinedGenerators
      (X := X) (Y := Y) R word z
  to_invHom := by
    intro z
    have hcomp := congrArg (fun f : FreeGroup X →* FreeGroup X => f z)
      (eliminateAdjoinedGeneratorsHom_comp_include word)
    have hz :
        eliminateAdjoinedGeneratorsHom word (includeAdjoinedGenerators X Y z) = z := by
      simpa using hcomp
    simp only [hz, mul_inv_cancel, one_mem]

def substituteDefinedGeneratorsTietzeEquiv
    (R : Set (FreeGroup (Sum X Y))) (word : Y → FreeGroup X) :
    TietzeEquiv
      (relatorsWithDefinedGenerators R word)
      (relatorsAfterSubstitutingDefinedGenerators R word)

def substituteDefinedGenerators
    (R : Set (FreeGroup (Sum X Y))) (word : Y → FreeGroup X) :
    PresentedGroup (relatorsWithDefinedGenerators R word) ≃*
      PresentedGroup (relatorsAfterSubstitutingDefinedGenerators R word)