ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorDeletion
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
def trivializeGeneratorsHom : FreeGroup (Sum X Y) →* FreeGroup X :=
eliminateAdjoinedGeneratorsHom (fun _ : Y => 1)The substitution map sends the generators in \(Y\) to \(1\), while keeping the old generators \(X\). It is used by the Tietze move deleting generators with relators \(y = 1\).
theorem trivializeGeneratorsHom_inl (x : X) :
trivializeGeneratorsHom X Y (FreeGroup.of (Sum.inl x)) =
FreeGroup.of xThe trivializing homomorphism fixes each retained generator \(x : X\).
Show proof
by
simp only [trivializeGeneratorsHom, eliminateAdjoinedGeneratorsHom_inl]
@[simp]Proof. Unfold the presented-group quotient and the relevant Tietze move. The forward and inverse maps are defined on generators, and the relator hypotheses say that each defining relation is sent into the normal closure generated by the target relators. Therefore the maps descend to the presented quotients, compose to the identity by relator-equivalence calculations, and preserve the presentation after adding, deleting, or replacing redundant generators and relators.
□theorem trivializeGeneratorsHom_inr (y : Y) :
trivializeGeneratorsHom X Y (FreeGroup.of (Sum.inr y)) = 1The trivializing homomorphism sends each deleted generator \(y : Y\) to \(1\).
Show proof
by
simp only [trivializeGeneratorsHom, eliminateAdjoinedGeneratorsHom_inr]Proof. Unfold the presented-group quotient and the relevant Tietze move. The forward and inverse maps are defined on generators, and the relator hypotheses say that each defining relation is sent into the normal closure generated by the target relators. Therefore the maps descend to the presented quotients, compose to the identity by relator-equivalence calculations, and preserve the presentation after adding, deleting, or replacing redundant generators and relators.
□theorem trivializeGeneratorsHom_comp_include :
(trivializeGeneratorsHom X Y).comp (includeAdjoinedGenerators X Y) =
MonoidHom.id (FreeGroup X)Trivializing the deleted generators after including the retained generators is the identity on the retained free group.
Show proof
eliminateAdjoinedGeneratorsHom_comp_include (fun _ : Y => 1)Proof. Unfold the presented-group quotient and the relevant Tietze move. The forward and inverse maps are defined on generators, and the relator hypotheses say that each defining relation is sent into the normal closure generated by the target relators. Therefore the maps descend to the presented quotients, compose to the identity by relator-equivalence calculations, and preserve the presentation after adding, deleting, or replacing redundant generators and relators.
□def trivialGeneratorRelators :
Set (FreeGroup (Sum X Y)) :=
{q | ∃ y : Y, q = FreeGroup.of (Sum.inr y)}Relators \(y = 1\) for a family of generators to be deleted.
def relatorsWithTrivialGenerators
(R : Set (FreeGroup (Sum X Y))) :
Set (FreeGroup (Sum X Y)) :=
R ∪ trivialGeneratorRelators (X := X) (Y := Y)Adds the relators \(y = 1\) to a presentation over \(X \oplus Y\), trivializing the auxiliary generators.
def relatorsAfterDeletingTrivialGenerators
(R : Set (FreeGroup (Sum X Y))) :
Set (FreeGroup X) :=
trivializeGeneratorsHom X Y '' RThe relators after deleting the \(Y\)-generators are obtained by substituting them with \(1\).
theorem trivialGeneratorRelator_mem (y : Y) :
FreeGroup.of (Sum.inr y) ∈
trivialGeneratorRelators (X := X) (Y := Y)Show proof
⟨y, rfl⟩Proof. Unfold the presented-group quotient and the relevant Tietze move. The forward and inverse maps are defined on generators, and the relator hypotheses say that each defining relation is sent into the normal closure generated by the target relators. Therefore the maps descend to the presented quotients, compose to the identity by relator-equivalence calculations, and preserve the presentation after adding, deleting, or replacing redundant generators and relators.
□theorem trivialGeneratorRelator_mem_relatorsWithTrivialGenerators
(R : Set (FreeGroup (Sum X Y))) (y : Y) :
FreeGroup.of (Sum.inr y) ∈ relatorsWithTrivialGenerators REach trivial-generator relation \(y = 1\) belongs to the relator set with trivial generators.
Show proof
Or.inr (trivialGeneratorRelator_mem (X := X) (Y := Y) y)Proof. Unfold the presented-group quotient and the relevant Tietze move. The forward and inverse maps are defined on generators, and the relator hypotheses say that each defining relation is sent into the normal closure generated by the target relators. Therefore the maps descend to the presented quotients, compose to the identity by relator-equivalence calculations, and preserve the presentation after adding, deleting, or replacing redundant generators and relators.
□theorem relator_mem_relatorsWithTrivialGenerators
{R : Set (FreeGroup (Sum X Y))} {r : FreeGroup (Sum X Y)}
(hr : r ∈ R) :
r ∈ relatorsWithTrivialGenerators REvery original relator belongs to the relator set with trivial generators.
Show proof
Or.inl hrProof. Unfold the presented-group quotient and the relevant Tietze move. The forward and inverse maps are defined on generators, and the relator hypotheses say that each defining relation is sent into the normal closure generated by the target relators. Therefore the maps descend to the presented quotients, compose to the identity by relator-equivalence calculations, and preserve the presentation after adding, deleting, or replacing redundant generators and relators.
□theorem include_trivializeGeneratorsHom_mod_trivialGeneratorRelators
(z : FreeGroup (Sum X Y)) :
includeAdjoinedGenerators X Y (trivializeGeneratorsHom X Y z) * z⁻¹ ∈
Subgroup.normalClosure (trivialGeneratorRelators (X := X) (Y := Y))Including the result of trivializing deleted generators is congruent to the original word modulo the trivial-generator relators.
Show proof
by
let S : Set (FreeGroup (Sum X Y)) :=
trivialGeneratorRelators (X := X) (Y := Y)
let N : Subgroup (FreeGroup (Sum X Y)) := Subgroup.normalClosure S
let F : FreeGroup (Sum X Y) →* FreeGroup (Sum X Y) :=
(includeAdjoinedGenerators X Y).comp (trivializeGeneratorsHom X Y)
have hhom : (QuotientGroup.mk' N).comp F = QuotientGroup.mk' N := by
ext z
cases z with
| inl x =>
simp only [includeAdjoinedGenerators, trivializeGeneratorsHom, MonoidHom.coe_comp, QuotientGroup.coe_mk',
Function.comp_apply, eliminateAdjoinedGeneratorsHom_inl, FreeGroup.map.of, QuotientGroup.mk'_apply, N, F]
| inr y =>
simp only [MonoidHom.comp_apply, F, trivializeGeneratorsHom_inr,
map_one]
change ((1 : FreeGroup (Sum X Y)) : FreeGroup (Sum X Y) ⧸ N) =
((FreeGroup.of (Sum.inr y) : FreeGroup (Sum X Y)) :
FreeGroup (Sum X Y) ⧸ N)
apply (QuotientGroup.eq_iff_div_mem
(N := N)
(x := (1 : FreeGroup (Sum X Y)))
(y := FreeGroup.of (Sum.inr y))).2
have hrel :
FreeGroup.of (Sum.inr y) ∈ N :=
Subgroup.subset_normalClosure
(trivialGeneratorRelator_mem (X := X) (Y := Y) y)
simpa [N, div_eq_mul_inv] using N.inv_mem hrel
have hz := congrArg (fun f : FreeGroup (Sum X Y) →*
FreeGroup (Sum X Y) ⧸ N => f z) hhom
change (includeAdjoinedGenerators X Y (trivializeGeneratorsHom X Y z) :
FreeGroup (Sum X Y) ⧸ N) = z at hz
exact (QuotientGroup.eq_iff_div_mem
(N := N)
(x := includeAdjoinedGenerators X Y (trivializeGeneratorsHom X Y z))
(y := z)).1 hzProof. Unfold the presented-group quotient and the relevant Tietze move. The forward and inverse maps are defined on generators, and the relator hypotheses say that each defining relation is sent into the normal closure generated by the target relators. Therefore the maps descend to the presented quotients, compose to the identity by relator-equivalence calculations, and preserve the presentation after adding, deleting, or replacing redundant generators and relators.
□theorem include_trivializeGeneratorsHom_mod_relatorsWithTrivialGenerators
(R : Set (FreeGroup (Sum X Y))) (z : FreeGroup (Sum X Y)) :
includeAdjoinedGenerators X Y (trivializeGeneratorsHom X Y z) * z⁻¹ ∈
Subgroup.normalClosure (relatorsWithTrivialGenerators R)Including the result of trivializing deleted generators is congruent to the original word modulo the relators with trivial generators.
Show proof
Subgroup.normalClosure_mono
(fun _ hq => Or.inr hq)
(include_trivializeGeneratorsHom_mod_trivialGeneratorRelators
(X := X) (Y := Y) z)Proof. Unfold the presented-group quotient and the relevant Tietze move. The forward and inverse maps are defined on generators, and the relator hypotheses say that each defining relation is sent into the normal closure generated by the target relators. Therefore the maps descend to the presented quotients, compose to the identity by relator-equivalence calculations, and preserve the presentation after adding, deleting, or replacing redundant generators and relators.
□def deleteTrivialGeneratorsMutualMapData
(R : Set (FreeGroup (Sum X Y))) :
RelatorQuotientMutualMapData
(relatorsWithTrivialGenerators R)
(relatorsAfterDeletingTrivialGenerators R) where
toHom := trivializeGeneratorsHom X Y
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⟩
simp only [trivializeGeneratorsHom_inr, one_mem]
mapsTargetRelators := by
intro s hs
rcases hs with ⟨r, hr, rfl⟩
let N : Subgroup (FreeGroup (Sum X Y)) :=
Subgroup.normalClosure (relatorsWithTrivialGenerators R)
have hmod :
includeAdjoinedGenerators X Y (trivializeGeneratorsHom X Y r) *
r⁻¹ ∈ N :=
include_trivializeGeneratorsHom_mod_relatorsWithTrivialGenerators
(X := X) (Y := Y) R r
have hrN : r ∈ N :=
Subgroup.subset_normalClosure
(relator_mem_relatorsWithTrivialGenerators (R := R) hr)
have hprod := Subgroup.mul_mem N hmod hrN
convert hprod using 1
group
inv_toHom := by
intro z
exact include_trivializeGeneratorsHom_mod_relatorsWithTrivialGenerators
(X := X) (Y := Y) R z
to_invHom := by
intro z
have hcomp := congrArg (fun f : FreeGroup X →* FreeGroup X => f z)
(trivializeGeneratorsHom_comp_include (X := X) (Y := Y))
have hz :
trivializeGeneratorsHom X Y (includeAdjoinedGenerators X Y z) = z := by
simpa using hcomp
simp only [hz, mul_inv_cancel, one_mem]Deleting generators forced to be trivial gives mutual maps between the original presentation and the reduced presentation.
def deleteTrivialGeneratorsTietzeEquiv
(R : Set (FreeGroup (Sum X Y))) :
TietzeEquiv
(relatorsWithTrivialGenerators R)
(relatorsAfterDeletingTrivialGenerators R) :=
TietzeEquiv.ofMutualMapData
(deleteTrivialGeneratorsMutualMapData R)Tietze equivalence deleting generators forced to be trivial by the relators \(y = 1\).
noncomputable def deleteTrivialGenerators
(R : Set (FreeGroup (Sum X Y))) :
PresentedGroup (relatorsWithTrivialGenerators R) ≃*
PresentedGroup (relatorsAfterDeletingTrivialGenerators R) :=
(deleteTrivialGeneratorsTietzeEquiv R).presentedEquivTietze move deleting a family of generators that have relators y = 1. Every remaining relator is pushed forward by substituting those deleted generators with 1.
def Kept (delete : Z → Prop) : Type _ :=
{z : Z // ¬ delete z}The subtype of generators kept after deleting those satisfying the predicate.
def Deleted (delete : Z → Prop) : Type _ :=
{z : Z // delete z}The subtype of generators deleted by the chosen decidable predicate.
def equiv (delete : Z → Prop) [DecidablePred delete] :
Z ≃ Sum (Kept delete) (Deleted delete) where
toFun z :=
if hz : delete z then
Sum.inr ⟨z, hz⟩
else
Sum.inl ⟨z, hz⟩
invFun z :=
match z with
| Sum.inl x => x.1
| Sum.inr y => y.1
left_inv z := by
by_cases hz : delete z <;> simp only [hz, ↓reduceDIte]
right_inv z := by
cases z with
| inl x =>
simp only [Kept, Deleted, x.property, ↓reduceDIte, Subtype.coe_eta]
| inr y =>
simp only [Kept, Deleted, y.property, ↓reduceDIte, Subtype.coe_eta]
@[simp]Split an arbitrary generator type into the generators kept and deleted by a decidable predicate.
theorem equiv_apply_of_delete
(delete : Z → Prop) [DecidablePred delete]
{z : Z} (hz : delete z) :
equiv delete z = Sum.inr (⟨z, hz⟩ : Deleted delete)Show proof
by
simp only [equiv, Equiv.coe_fn_mk, hz, ↓reduceDIte]
@[simp]Proof. Unfold the presented-group quotient and the relevant Tietze move. The forward and inverse maps are defined on generators, and the relator hypotheses say that each defining relation is sent into the normal closure generated by the target relators. Therefore the maps descend to the presented quotients, compose to the identity by relator-equivalence calculations, and preserve the presentation after adding, deleting, or replacing redundant generators and relators.
□theorem equiv_apply_of_not_delete
(delete : Z → Prop) [DecidablePred delete]
{z : Z} (hz : ¬ delete z) :
equiv delete z = Sum.inl (⟨z, hz⟩ : Kept delete)Show proof
by
simp only [equiv, Equiv.coe_fn_mk, hz, ↓reduceDIte]
@[simp]Proof. Unfold the presented-group quotient and the relevant Tietze move. The forward and inverse maps are defined on generators, and the relator hypotheses say that each defining relation is sent into the normal closure generated by the target relators. Therefore the maps descend to the presented quotients, compose to the identity by relator-equivalence calculations, and preserve the presentation after adding, deleting, or replacing redundant generators and relators.
□theorem equiv_symm_inl
(delete : Z → Prop) [DecidablePred delete]
(z : Kept delete) :
(equiv delete).symm (Sum.inl z) = z.1Show proof
rfl
@[simp]Proof. Unfold the presented-group quotient and the relevant Tietze move. The forward and inverse maps are defined on generators, and the relator hypotheses say that each defining relation is sent into the normal closure generated by the target relators. Therefore the maps descend to the presented quotients, compose to the identity by relator-equivalence calculations, and preserve the presentation after adding, deleting, or replacing redundant generators and relators.
□theorem equiv_symm_inr
(delete : Z → Prop) [DecidablePred delete]
(z : Deleted delete) :
(equiv delete).symm (Sum.inr z) = z.1Show proof
rflProof. Unfold the presented-group quotient and the relevant Tietze move. The forward and inverse maps are defined on generators, and the relator hypotheses say that each defining relation is sent into the normal closure generated by the target relators. Therefore the maps descend to the presented quotients, compose to the identity by relator-equivalence calculations, and preserve the presentation after adding, deleting, or replacing redundant generators and relators.
□def definedGeneratorRelatorsAlongEquiv
(e : Z ≃ Sum X Y) (word : Y → FreeGroup X) :
Set (FreeGroup Z) :=
(FreeGroup.freeGroupCongr e).symm ''
definedGeneratorRelators (X := X) (Y := Y) worddef relatorsWithDefinedGeneratorsAlongEquiv
(R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)
(word : Y → FreeGroup X) :
Set (FreeGroup Z) :=
R ∪ definedGeneratorRelatorsAlongEquiv e worddef relatorsAfterSubstitutingDefinedGeneratorsAlongEquiv
(R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)
(word : Y → FreeGroup X) :
Set (FreeGroup X) :=
relatorsAfterSubstitutingDefinedGenerators
(FreeGroup.freeGroupCongr e '' R) wordRelators after renaming by \(e\) and substituting every deleted generator \(y : Y\) by \(\mathrm{word}(y)\).
theorem freeGroupCongr_image_definedGeneratorRelatorsAlongEquiv
(e : Z ≃ Sum X Y) (word : Y → FreeGroup X) :
FreeGroup.freeGroupCongr e ''
definedGeneratorRelatorsAlongEquiv e word =
definedGeneratorRelators (X := X) (Y := Y) wordShow proof
by
ext q
constructor
· rintro ⟨z, hz, rfl⟩
rcases hz with ⟨p, hp, hpz⟩
have hpmap :
FreeGroup.map (fun z : Z => e z)
(FreeGroup.map (fun z : Sum X Y => e.symm z) p) = p := by
simpa [FreeGroup.freeGroupCongr] using
(FreeGroup.freeGroupCongr e).right_inv p
simpa [FreeGroup.freeGroupCongr, ← hpz, hpmap] using hp
· intro hq
exact ⟨(FreeGroup.freeGroupCongr e).symm q, ⟨q, hq, rfl⟩,
(FreeGroup.freeGroupCongr e).right_inv q⟩Proof. Unfold the presented-group quotient and the relevant Tietze move. The forward and inverse maps are defined on generators, and the relator hypotheses say that each defining relation is sent into the normal closure generated by the target relators. Therefore the maps descend to the presented quotients, compose to the identity by relator-equivalence calculations, and preserve the presentation after adding, deleting, or replacing redundant generators and relators.
□theorem freeGroupCongr_image_relatorsWithDefinedGeneratorsAlongEquiv
(R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)
(word : Y → FreeGroup X) :
FreeGroup.freeGroupCongr e ''
relatorsWithDefinedGeneratorsAlongEquiv R e word =
relatorsWithDefinedGenerators
(FreeGroup.freeGroupCongr e '' R) wordRenaming generators carries the pulled-back relators with defined generators to the corresponding split relator set.
Show proof
by
ext q
constructor
· rintro ⟨z, hz, rfl⟩
rcases hz with hz | hz
· exact Or.inl ⟨z, hz, rfl⟩
· rcases hz with ⟨p, hp, hpz⟩
exact Or.inr (by
have hpmap :
FreeGroup.map (fun z : Z => e z)
(FreeGroup.map (fun z : Sum X Y => e.symm z) p) = p := by
simpa [FreeGroup.freeGroupCongr] using
(FreeGroup.freeGroupCongr e).right_inv p
simpa [FreeGroup.freeGroupCongr, ← hpz, hpmap] using hp)
· intro hq
rcases hq with hq | hq
· rcases hq with ⟨z, hz, hzq⟩
exact ⟨z, Or.inl hz, hzq⟩
· exact ⟨(FreeGroup.freeGroupCongr e).symm q,
Or.inr ⟨q, hq, rfl⟩,
(FreeGroup.freeGroupCongr e).right_inv q⟩Proof. Unfold the presented-group quotient and the relevant Tietze move. The forward and inverse maps are defined on generators, and the relator hypotheses say that each defining relation is sent into the normal closure generated by the target relators. Therefore the maps descend to the presented quotients, compose to the identity by relator-equivalence calculations, and preserve the presentation after adding, deleting, or replacing redundant generators and relators.
□def substituteDefinedGeneratorsAlongEquivTietzeEquiv
(R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)
(word : Y → FreeGroup X) :
TietzeEquiv
(relatorsWithDefinedGeneratorsAlongEquiv R e word)
(relatorsAfterSubstitutingDefinedGeneratorsAlongEquiv R e word) :=
(renameGeneratorsTietzeEquiv
(relatorsWithDefinedGeneratorsAlongEquiv R e word) e).trans
((TietzeEquiv.ofNormalClosureEq
(R := FreeGroup.freeGroupCongr e ''
relatorsWithDefinedGeneratorsAlongEquiv R e word)
(S := relatorsWithDefinedGenerators
(FreeGroup.freeGroupCongr e '' R) word)
(by
rw [freeGroupCongr_image_relatorsWithDefinedGeneratorsAlongEquiv])).trans
(substituteDefinedGeneratorsTietzeEquiv
(FreeGroup.freeGroupCongr e '' R) word))Tietze move eliminating an arbitrary family of generators after splitting the generator type by an equivalence \(Z \simeq X \oplus Y\).
noncomputable def substituteDefinedGeneratorsAlongEquiv
(R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)
(word : Y → FreeGroup X) :
PresentedGroup (relatorsWithDefinedGeneratorsAlongEquiv R e word) ≃*
PresentedGroup
(relatorsAfterSubstitutingDefinedGeneratorsAlongEquiv R e word) :=
(substituteDefinedGeneratorsAlongEquivTietzeEquiv R e word).presentedEquivPresented-group isomorphism obtained by substituting defined generators after splitting the generator type by an equivalence \(Z \simeq X \oplus Y\).
def definedGeneratorRelatorsOfPredicate
(delete : Z → Prop) [DecidablePred delete]
(word :
GeneratorPartition.Deleted delete →
FreeGroup (GeneratorPartition.Kept delete)) :
Set (FreeGroup Z) :=
definedGeneratorRelatorsAlongEquiv
(GeneratorPartition.equiv delete) worddef relatorsWithDefinedGeneratorsOfPredicate
(R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete]
(word :
GeneratorPartition.Deleted delete →
FreeGroup (GeneratorPartition.Kept delete)) :
Set (FreeGroup Z) :=
relatorsWithDefinedGeneratorsAlongEquiv R
(GeneratorPartition.equiv delete) wordThe relator set obtained by adding defining relators for all generators satisfying the predicate.
def relatorsAfterSubstitutingDefinedGeneratorsOfPredicate
(R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete]
(word :
GeneratorPartition.Deleted delete →
FreeGroup (GeneratorPartition.Kept delete)) :
Set (FreeGroup (GeneratorPartition.Kept delete)) :=
relatorsAfterSubstitutingDefinedGeneratorsAlongEquiv R
(GeneratorPartition.equiv delete) wordRelators obtained after substituting every generator satisfying the predicate by its defining word.
def substituteDefinedGeneratorsOfPredicateTietzeEquiv
(R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete]
(word :
GeneratorPartition.Deleted delete →
FreeGroup (GeneratorPartition.Kept delete)) :
TietzeEquiv
(relatorsWithDefinedGeneratorsOfPredicate R delete word)
(relatorsAfterSubstitutingDefinedGeneratorsOfPredicate R delete word) :=
substituteDefinedGeneratorsAlongEquivTietzeEquiv R
(GeneratorPartition.equiv delete) wordTietze equivalence substituting the generators satisfying the predicate by their defining words.
noncomputable def substituteDefinedGeneratorsOfPredicate
(R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete]
(word :
GeneratorPartition.Deleted delete →
FreeGroup (GeneratorPartition.Kept delete)) :
PresentedGroup (relatorsWithDefinedGeneratorsOfPredicate R delete word) ≃*
PresentedGroup
(relatorsAfterSubstitutingDefinedGeneratorsOfPredicate R delete word) :=
(substituteDefinedGeneratorsOfPredicateTietzeEquiv R delete word).presentedEquivSubstitute generators defined by words satisfying the given predicate.
def trivialGeneratorRelatorsAlongEquiv
(e : Z ≃ Sum X Y) :
Set (FreeGroup Z) :=
(FreeGroup.freeGroupCongr e).symm ''
trivialGeneratorRelators (X := X) (Y := Y)def relatorsWithTrivialGeneratorsAlongEquiv
(R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :
Set (FreeGroup Z) :=
R ∪ trivialGeneratorRelatorsAlongEquiv edef relatorsAfterDeletingTrivialGeneratorsAlongEquiv
(R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :
Set (FreeGroup X) :=
relatorsAfterDeletingTrivialGenerators (FreeGroup.freeGroupCongr e '' R)Relators after renaming by \(e\) and deleting every generator in \(Y\).
theorem freeGroupCongr_image_trivialGeneratorRelatorsAlongEquiv
(e : Z ≃ Sum X Y) :
FreeGroup.freeGroupCongr e ''
trivialGeneratorRelatorsAlongEquiv (X := X) (Y := Y) e =
trivialGeneratorRelators (X := X) (Y := Y)Show proof
by
ext q
constructor
· rintro ⟨z, hz, rfl⟩
rcases hz with ⟨p, hp, hpz⟩
have hpmap :
FreeGroup.map (fun z : Z => e z)
(FreeGroup.map (fun z : Sum X Y => e.symm z) p) = p := by
simpa [FreeGroup.freeGroupCongr] using
(FreeGroup.freeGroupCongr e).right_inv p
simpa [FreeGroup.freeGroupCongr, ← hpz, hpmap] using hp
· intro hq
exact ⟨(FreeGroup.freeGroupCongr e).symm q, ⟨q, hq, rfl⟩,
(FreeGroup.freeGroupCongr e).right_inv q⟩Proof. Unfold the presented-group quotient and the relevant Tietze move. The forward and inverse maps are defined on generators, and the relator hypotheses say that each defining relation is sent into the normal closure generated by the target relators. Therefore the maps descend to the presented quotients, compose to the identity by relator-equivalence calculations, and preserve the presentation after adding, deleting, or replacing redundant generators and relators.
□theorem freeGroupCongr_image_relatorsWithTrivialGeneratorsAlongEquiv
(R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :
FreeGroup.freeGroupCongr e ''
relatorsWithTrivialGeneratorsAlongEquiv R e =
relatorsWithTrivialGenerators (FreeGroup.freeGroupCongr e '' R)Renaming generators carries the pulled-back relators with trivial generators to the corresponding split relator set.
Show proof
by
ext q
constructor
· rintro ⟨z, hz, rfl⟩
rcases hz with hz | hz
· exact Or.inl ⟨z, hz, rfl⟩
· rcases hz with ⟨p, hp, hpz⟩
exact Or.inr (by
have hpmap :
FreeGroup.map (fun z : Z => e z)
(FreeGroup.map (fun z : Sum X Y => e.symm z) p) = p := by
simpa [FreeGroup.freeGroupCongr] using
(FreeGroup.freeGroupCongr e).right_inv p
simpa [FreeGroup.freeGroupCongr, ← hpz, hpmap] using hp)
· intro hq
rcases hq with hq | hq
· rcases hq with ⟨z, hz, hzq⟩
exact ⟨z, Or.inl hz, hzq⟩
· exact ⟨(FreeGroup.freeGroupCongr e).symm q,
Or.inr ⟨q, hq, rfl⟩,
(FreeGroup.freeGroupCongr e).right_inv q⟩Proof. Unfold the presented-group quotient and the relevant Tietze move. The forward and inverse maps are defined on generators, and the relator hypotheses say that each defining relation is sent into the normal closure generated by the target relators. Therefore the maps descend to the presented quotients, compose to the identity by relator-equivalence calculations, and preserve the presentation after adding, deleting, or replacing redundant generators and relators.
□def deleteTrivialGeneratorsAlongEquivTietzeEquiv
(R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :
TietzeEquiv
(relatorsWithTrivialGeneratorsAlongEquiv R e)
(relatorsAfterDeletingTrivialGeneratorsAlongEquiv R e) :=
(renameGeneratorsTietzeEquiv
(relatorsWithTrivialGeneratorsAlongEquiv R e) e).trans
((TietzeEquiv.ofNormalClosureEq
(R := FreeGroup.freeGroupCongr e ''
relatorsWithTrivialGeneratorsAlongEquiv R e)
(S := relatorsWithTrivialGenerators
(FreeGroup.freeGroupCongr e '' R))
(by
rw [freeGroupCongr_image_relatorsWithTrivialGeneratorsAlongEquiv])).trans
(deleteTrivialGeneratorsTietzeEquiv
(FreeGroup.freeGroupCongr e '' R)))Tietze move deleting an arbitrary family of generators after splitting the generator type by an equivalence \(Z \simeq X \oplus Y\).
noncomputable def deleteTrivialGeneratorsAlongEquiv
(R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :
PresentedGroup (relatorsWithTrivialGeneratorsAlongEquiv R e) ≃*
PresentedGroup
(relatorsAfterDeletingTrivialGeneratorsAlongEquiv R e) :=
(deleteTrivialGeneratorsAlongEquivTietzeEquiv R e).presentedEquivPresented-group isomorphism obtained by deleting trivial generators after splitting the generator type by an equivalence \(Z \simeq X \oplus Y\).
def trivialGeneratorRelatorsOfPredicate
(delete : Z → Prop) [DecidablePred delete] :
Set (FreeGroup Z) :=
trivialGeneratorRelatorsAlongEquiv
(X := GeneratorPartition.Kept delete)
(Y := GeneratorPartition.Deleted delete)
(GeneratorPartition.equiv delete)def relatorsWithTrivialGeneratorsOfPredicate
(R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete] :
Set (FreeGroup Z) :=
relatorsWithTrivialGeneratorsAlongEquiv R
(X := GeneratorPartition.Kept delete)
(Y := GeneratorPartition.Deleted delete)
(GeneratorPartition.equiv delete)def relatorsAfterDeletingTrivialGeneratorsOfPredicate
(R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete] :
Set (FreeGroup (GeneratorPartition.Kept delete)) :=
relatorsAfterDeletingTrivialGeneratorsAlongEquiv R
(X := GeneratorPartition.Kept delete)
(Y := GeneratorPartition.Deleted delete)
(GeneratorPartition.equiv delete)Relators obtained after deleting every generator satisfying the predicate by substituting it with \(1\).
def deleteTrivialGeneratorsOfPredicateTietzeEquiv
(R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete] :
TietzeEquiv
(relatorsWithTrivialGeneratorsOfPredicate R delete)
(relatorsAfterDeletingTrivialGeneratorsOfPredicate R delete) :=
deleteTrivialGeneratorsAlongEquivTietzeEquiv R
(X := GeneratorPartition.Kept delete)
(Y := GeneratorPartition.Deleted delete)
(GeneratorPartition.equiv delete)Tietze equivalence deleting the generators satisfying the chosen predicate.
noncomputable def deleteTrivialGeneratorsOfPredicate
(R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete] :
PresentedGroup (relatorsWithTrivialGeneratorsOfPredicate R delete) ≃*
PresentedGroup
(relatorsAfterDeletingTrivialGeneratorsOfPredicate R delete) :=
(deleteTrivialGeneratorsOfPredicateTietzeEquiv R delete).presentedEquivThis declaration deletes generators proved trivial by the given predicate.