KernelQuotient.lean

theorem presentedGroup_toGroup_ker_eq_map_freeGroupLift_ker
    {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
    (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) :
    (PresentedGroup.toGroup (rels := rels) (f := f) hrels).ker =
      Subgroup.map (PresentedGroup.mk rels) (FreeGroup.lift f).ker

def presentedFreeKernelToPresentedKernelHom
    {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
    (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) :
    (FreeGroup.lift f).ker →*
      (PresentedGroup.toGroup (rels := rels) (f := f) hrels).ker where
  toFun k :=
    ⟨PresentedGroup.mk rels k, by
      change FreeGroup.lift f (k : FreeGroup X) = 1
      exact k.property⟩
  map_one' := by
    ext
    simp only [OneMemClass.coe_one, map_one]
  map_mul' k l := by
    ext
    simp only [Subgroup.coe_mul, map_mul, MulMemClass.mk_mul_mk]

theorem presentedFreeKernelToPresentedKernelHom_surjective
    {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
    (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) :
    Function.Surjective (presentedFreeKernelToPresentedKernelHom hrels)

theorem presentedFreeKernelToPresentedKernelHom_ker_eq_comap_normalClosure
    {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
    (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) :
    (presentedFreeKernelToPresentedKernelHom hrels).ker =
      Subgroup.comap ((FreeGroup.lift f).ker.subtype) (Subgroup.normalClosure rels)

def presentedFreeKernelRelatorQuotientEquivPresentedKernel
    {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
    (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) :
    (FreeGroup.lift f).ker ⧸
        Subgroup.comap ((FreeGroup.lift f).ker.subtype) (Subgroup.normalClosure rels) ≃*
      (PresentedGroup.toGroup (rels := rels) (f := f) hrels).ker

def freeKernelConjugateRelatorSet
    {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A} :
    Set (FreeGroup.lift f).ker

def freeKernelTransversalRelatorSet
    {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
    (T : Set (FreeGroup X)) :
    Set (FreeGroup.lift f).ker

theorem freeKernelTransversalRelatorSet_subset_conjugateRelatorSet
    {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
    (T : Set (FreeGroup X)) :
    freeKernelTransversalRelatorSet (f := f) (rels := rels) T ⊆
      freeKernelConjugateRelatorSet (f := f) (rels := rels)

theorem freeKernelTransversalRelatorSet_normalClosure_eq_conjugateRelatorSet
    {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
    (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) {T : Set (FreeGroup X)}
    (hT : Subgroup.IsComplement ((FreeGroup.lift f).ker : Set (FreeGroup X)) T) :
    Subgroup.normalClosure (freeKernelTransversalRelatorSet (f := f) (rels := rels) T) =
      Subgroup.normalClosure (freeKernelConjugateRelatorSet (f := f) (rels := rels))

theorem freeKernelConjugateRelatorSet_subset_comap_normalClosure
    {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A} :
    freeKernelConjugateRelatorSet (f := f) (rels := rels) ⊆
      Subgroup.comap ((FreeGroup.lift f).ker.subtype) (Subgroup.normalClosure rels)

theorem freeKernelConjugateRelatorSet_normalClosure_le_comap_normalClosure
    {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A} :
    Subgroup.normalClosure (freeKernelConjugateRelatorSet (f := f) (rels := rels)) ≤
      Subgroup.comap ((FreeGroup.lift f).ker.subtype) (Subgroup.normalClosure rels)

theorem freeKernelConjugateRelatorSet_normalClosure_eq_comap_normalClosure
    {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
    (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) :
    Subgroup.normalClosure (freeKernelConjugateRelatorSet (f := f) (rels := rels)) =
      Subgroup.comap ((FreeGroup.lift f).ker.subtype) (Subgroup.normalClosure rels)

theorem freeKernelTransversalRelatorSet_normalClosure_eq_comap_normalClosure
    {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
    (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) {T : Set (FreeGroup X)}
    (hT : Subgroup.IsComplement ((FreeGroup.lift f).ker : Set (FreeGroup X)) T) :
    Subgroup.normalClosure (freeKernelTransversalRelatorSet (f := f) (rels := rels) T) =
      Subgroup.comap ((FreeGroup.lift f).ker.subtype) (Subgroup.normalClosure rels)

def presentedFreeKernelTransversalRelatorQuotientEquivPresentedKernel
    {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
    (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) {T : Set (FreeGroup X)}
    (hT : Subgroup.IsComplement ((FreeGroup.lift f).ker : Set (FreeGroup X)) T) :
    (FreeGroup.lift f).ker ⧸
        Subgroup.normalClosure (freeKernelTransversalRelatorSet (f := f) (rels := rels) T) ≃*
      (PresentedGroup.toGroup (rels := rels) (f := f) hrels).ker

def presentedFreeKernelSchreierRelatorQuotientEquivPresentedKernel
    {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
    (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) {T : Set (FreeGroup X)}
    (hT : Subgroup.IsComplement ((FreeGroup.lift f).ker : Set (FreeGroup X)) T)
    {Y : Type*} (e : FreeGroup Y ≃* (FreeGroup.lift f).ker) :
    FreeGroup Y ⧸
        Subgroup.normalClosure
          (freeGroupPullbackRelatorSet e
            (freeKernelTransversalRelatorSet (f := f) (rels := rels) T)) ≃*
      (PresentedGroup.toGroup (rels := rels) (f := f) hrels).ker

theorem mem_freeGroupPullbackRelatorSet_iff
    {Y G : Type*} [Group G] {e : FreeGroup Y ≃* G} {S : Set G} {y : FreeGroup Y} :
    y ∈ freeGroupPullbackRelatorSet e S ↔ e y ∈ S

theorem freeKernelTransversalRelatorSet_mem
    {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
    (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1)
    {T : Set (FreeGroup X)} {t : FreeGroup X} (ht : t ∈ T)
    {r : FreeGroup X} (hr : r ∈ rels) :
    (⟨t * r * t⁻¹, by
      change FreeGroup.lift f (t * r * t⁻¹) = 1
      simp only [map_mul, hrels r hr, mul_one, map_inv, mul_inv_cancel]⟩ : (FreeGroup.lift f).ker) ∈
        freeKernelTransversalRelatorSet (f := f) (rels := rels) T := by
  exact ⟨t, ht, r, hr, rfl⟩

theorem freeGroupPullbackRelator_mem
    {Y G : Type*} [Group G] (e : FreeGroup Y ≃* G) {S : Set G} {s : G}
    (hs : s ∈ S) :
    e.symm s ∈ freeGroupPullbackRelatorSet e S

theorem freeGroupPullbackRelator_mem_normalClosure
    {Y G : Type*} [Group G] (e : FreeGroup Y ≃* G) {S : Set G} {s : G}
    (hs : s ∈ S) :
    e.symm s ∈ Subgroup.normalClosure (freeGroupPullbackRelatorSet e S)

theorem freeGroupPullback_transversalRelator_mem_normalClosure
    {X A Y : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
    (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1)
    {T : Set (FreeGroup X)} (e : FreeGroup Y ≃* (FreeGroup.lift f).ker)
    {t : FreeGroup X} (ht : t ∈ T) {r : FreeGroup X} (hr : r ∈ rels) :
    e.symm
        (⟨t * r * t⁻¹, by
          change FreeGroup.lift f (t * r * t⁻¹) = 1
          simp only [map_mul, hrels r hr, mul_one, map_inv, mul_inv_cancel]⟩ : (FreeGroup.lift
              f).ker) ∈
      Subgroup.normalClosure
        (freeGroupPullbackRelatorSet e
          (freeKernelTransversalRelatorSet (f := f) (rels := rels) T)) :=
  freeGroupPullbackRelator_mem_normalClosure e
    (freeKernelTransversalRelatorSet_mem hrels ht hr)

theorem freeKernelElement_mem_transversalRelator_normalClosure_of_mem_normalClosure
    {X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
    (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) {T : Set (FreeGroup X)}
    (hT : Subgroup.IsComplement ((FreeGroup.lift f).ker : Set (FreeGroup X)) T)
    {k : (FreeGroup.lift f).ker}
    (hk : (k : FreeGroup X) ∈ Subgroup.normalClosure rels) :
      k ∈ Subgroup.normalClosure
        (freeKernelTransversalRelatorSet (f := f) (rels := rels) T)

theorem freeGroupPullback_mem_normalClosure_of_image_mem
    {Y G : Type*} [Group G] (e : FreeGroup Y ≃* G) (S : Set G)
    {y : FreeGroup Y} (hy : e y ∈ Subgroup.normalClosure S) :
    y ∈ Subgroup.normalClosure (freeGroupPullbackRelatorSet e S)

theorem freeGroupPullback_transversalRelator_mem_normalClosure_of_mem_normalClosure
    {X A Y : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
    (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) {T : Set (FreeGroup X)}
    (hT : Subgroup.IsComplement ((FreeGroup.lift f).ker : Set (FreeGroup X)) T)
    (e : FreeGroup Y ≃* (FreeGroup.lift f).ker) {k : (FreeGroup.lift f).ker}
    (hk : (k : FreeGroup X) ∈ Subgroup.normalClosure rels) :
    e.symm k ∈
        Subgroup.normalClosure
          (freeGroupPullbackRelatorSet e
            (freeKernelTransversalRelatorSet (f := f) (rels := rels) T))