ReidemeisterSchreier.Discrete.Presentations.Relators
This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.
import
- Mathlib.GroupTheory.FreeGroup.Reduce
- Mathlib.Tactic.NormNum.LegendreSymbol
Imported by
- FenchelNielsenZomorrodian.Discrete.Singerman.FreeGroupWords
- ReidemeisterSchreier
- ReidemeisterSchreier.Discrete
- ReidemeisterSchreier.Discrete.Presentations
- ReidemeisterSchreier.Discrete.Presentations.Tietze.RelatorQuotientMutualMapData
- ReidemeisterSchreier.Discrete.ReidemeisterSchreier
- ReidemeisterSchreier.Discrete.ReidemeisterSchreier.Rewriting
def RelatorEquivalent (R : Set G) (u v : G) : Prop :=
u * v⁻¹ ∈ Subgroup.normalClosure REquality modulo the normal closure generated by R.
theorem relatorEquivalent_iff_eq_in_presentedQuotient {R : Set G} {u v : G} :
RelatorEquivalent R u v ↔
((u : G ⧸ Subgroup.normalClosure R) =
(v : G ⧸ Subgroup.normalClosure R))Relator equivalence is equivalent to equality in the presented quotient.
Show proof
by
simpa [RelatorEquivalent, div_eq_mul_inv] using
(QuotientGroup.eq_iff_div_mem
(N := Subgroup.normalClosure R) (x := u) (y := v)).symmProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□@[simp] theorem relatorEquivalent_one_right {R : Set G} {u : G} :
RelatorEquivalent R u 1 ↔ u ∈ Subgroup.normalClosure RRelator equivalence to one on the right is membership in the relator normal closure.
Show proof
by
simp only [RelatorEquivalent, inv_one, mul_one]Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□@[simp] theorem relatorEquivalent_one_left {R : Set G} {u : G} :
RelatorEquivalent R 1 u ↔ u ∈ Subgroup.normalClosure RRelator equivalence from one on the left is membership in the relator normal closure.
Show proof
by
constructor
· intro h
have huInv : u⁻¹ ∈ Subgroup.normalClosure R := by
simpa [RelatorEquivalent] using h
simpa using Subgroup.inv_mem (Subgroup.normalClosure R) huInv
· intro h
have huInv : u⁻¹ ∈ Subgroup.normalClosure R :=
Subgroup.inv_mem (Subgroup.normalClosure R) h
simpa [RelatorEquivalent] using huInvProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□def relatorEquivalentSetoid (R : Set G) : Setoid G where
r := RelatorEquivalent R
iseqv := by
refine ⟨?_, ?_, ?_⟩
· intro u
rw [relatorEquivalent_iff_eq_in_presentedQuotient]
· intro u v h
rw [relatorEquivalent_iff_eq_in_presentedQuotient] at h ⊢
exact h.symm
· intro u v w huv hvw
rw [relatorEquivalent_iff_eq_in_presentedQuotient] at huv hvw ⊢
exact huv.trans hvwRelator equivalence defines a setoid on the free group.
theorem refl (R : Set G) (u : G) : RelatorEquivalent R u uRelator equivalence is reflexive.
Show proof
by
rw [relatorEquivalent_iff_eq_in_presentedQuotient]Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem of_eq (h : u = v) : RelatorEquivalent R u vEqual relators are relator-equivalent.
Show proof
by
rw [h]Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem symm (h : RelatorEquivalent R u v) : RelatorEquivalent R v uRelator equivalence is symmetric.
Show proof
by
rw [relatorEquivalent_iff_eq_in_presentedQuotient] at h ⊢
exact h.symmProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The named operation preserves that normal closure by the appropriate closure property, monotonicity, quotient equality, or Tietze-map construction.
□theorem trans (h₁ : RelatorEquivalent R u v) (h₂ : RelatorEquivalent R v w) : RelatorEquivalent R u wRelator equivalence is transitive.
Show proof
by
rw [relatorEquivalent_iff_eq_in_presentedQuotient] at h₁ h₂ ⊢
exact h₁.trans h₂Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The named operation preserves that normal closure by the appropriate closure property, monotonicity, quotient equality, or Tietze-map construction.
□theorem inv (h : RelatorEquivalent R u v) : RelatorEquivalent R u⁻¹ v⁻¹Relator equivalence is symmetric.
Show proof
by
rw [relatorEquivalent_iff_eq_in_presentedQuotient] at h ⊢
simpa using congrArg Inv.inv hProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem mul (h₁ : RelatorEquivalent R u v) (h₂ : RelatorEquivalent R a b) :
RelatorEquivalent R (u * a) (v * b)Multiplication of relator-equivalent words preserves relator equivalence.
Show proof
by
rw [relatorEquivalent_iff_eq_in_presentedQuotient] at h₁ h₂ ⊢
calc
((u * a : G) : G ⧸ Subgroup.normalClosure R) =
(u : G ⧸ Subgroup.normalClosure R) * (a : G ⧸ Subgroup.normalClosure R) := rfl
_ = (v : G ⧸ Subgroup.normalClosure R) * (b : G ⧸ Subgroup.normalClosure R) := by
rw [h₁, h₂]
_ = ((v * b : G) : G ⧸ Subgroup.normalClosure R) := rflProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The named operation preserves that normal closure by the appropriate closure property, monotonicity, quotient equality, or Tietze-map construction.
□theorem pow (h : RelatorEquivalent R u v) (n : ℕ) : RelatorEquivalent R (u ^ n) (v ^ n)Taking natural powers preserves relator equivalence.
Show proof
by
rw [relatorEquivalent_iff_eq_in_presentedQuotient] at h ⊢
simpa using congrArg (fun z : G ⧸ Subgroup.normalClosure R => z ^ n) hProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The named operation preserves that normal closure by the appropriate closure property, monotonicity, quotient equality, or Tietze-map construction.
□theorem zpow (h : RelatorEquivalent R u v) (n : ℤ) : RelatorEquivalent R (u ^ n) (v ^ n)Taking integer powers preserves relator equivalence.
Show proof
by
rw [relatorEquivalent_iff_eq_in_presentedQuotient] at h ⊢
simpa using congrArg (fun z : G ⧸ Subgroup.normalClosure R => z ^ n) hProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The named operation preserves that normal closure by the appropriate closure property, monotonicity, quotient equality, or Tietze-map construction.
□theorem mul_eq_one (h₁ : RelatorEquivalent R u 1) (h₂ : RelatorEquivalent R v 1) :
RelatorEquivalent R (u * v) 1A product of words relator-equivalent to one is relator-equivalent to one.
Show proof
by
simpa using mul h₁ h₂Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The named operation preserves that normal closure by the appropriate closure property, monotonicity, quotient equality, or Tietze-map construction.
□theorem pow_eq_one (h : RelatorEquivalent R u 1) (n : ℕ) :
RelatorEquivalent R (u ^ n) 1A natural-number power is relator-equivalent to the identity when the base word is relator-equivalent to the identity.
Show proof
by
simpa using pow h nProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The named operation preserves that normal closure by the appropriate closure property, monotonicity, quotient equality, or Tietze-map construction.
□theorem zpow_eq_one (h : RelatorEquivalent R u 1) (n : ℤ) :
RelatorEquivalent R (u ^ n) 1An integer power is relator-equivalent to the identity when the base word is relator-equivalent to the identity.
theorem inv_eq_one (h : RelatorEquivalent R u 1) :
RelatorEquivalent R u⁻¹ 1The inverse of a word is relator-equivalent to one exactly when the word is.
Show proof
by
simpa using inv hProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The named operation preserves that normal closure by the appropriate closure property, monotonicity, quotient equality, or Tietze-map construction.
□theorem conjugate_pow_eq (a u : G) (n : ℕ) :
(a * u * a⁻¹) ^ n = a * u ^ n * a⁻¹Conjugating a power relator gives an equivalent relator.
Show proof
by
induction n with
| zero =>
simp only [pow_zero, mul_one, mul_inv_cancel]
| succ n ih =>
calc
(a * u * a⁻¹) ^ (n + 1) =
a * u ^ n * a⁻¹ * (a * u * a⁻¹) := by
rw [pow_succ, ih]
_ = a * (u ^ n * u) * a⁻¹ := by
simp only [mul_assoc, inv_mul_cancel_left]
_ = a * u ^ (n + 1) * a⁻¹ := by
rw [pow_succ]Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem mul_eq_one_iff_eq_inv :
RelatorEquivalent R (u * v) 1 ↔ RelatorEquivalent R u v⁻¹The relator membership follows from the corresponding relator-equivalence criterion.
Show proof
by
constructor
· intro h
simpa only [RelatorEquivalent, inv_inv, inv_one, mul_one] using h
· intro h
simpa only [RelatorEquivalent, inv_inv, inv_one, mul_one] using hProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem eq_inv_of_mul_eq_one (h : RelatorEquivalent R (u * v) 1) :
RelatorEquivalent R u v⁻¹If a product is relator-equivalent to one, the left factor is relator-equivalent to the inverse of the right factor.
Show proof
mul_eq_one_iff_eq_inv.1 hProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The named operation preserves that normal closure by the appropriate closure property, monotonicity, quotient equality, or Tietze-map construction.
□theorem mul_eq_one_of_eq_inv (h : RelatorEquivalent R u v⁻¹) :
RelatorEquivalent R (u * v) 1A product is relator-equivalent to the identity when one factor is relator-equivalent to the inverse of the other.
Show proof
mul_eq_one_iff_eq_inv.2 hProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The named operation preserves that normal closure by the appropriate closure property, monotonicity, quotient equality, or Tietze-map construction.
□theorem eq_one_of_mul_eq_one_left
(hu : RelatorEquivalent R u 1)
(huv : RelatorEquivalent R (u * v) 1) :
RelatorEquivalent R v 1If a left product is relator-equivalent to one and the left factor is trivial, the right factor is relator-equivalent to one.
Show proof
by
rw [relatorEquivalent_iff_eq_in_presentedQuotient] at hu huv ⊢
calc
(v : G ⧸ Subgroup.normalClosure R) =
(1 : G ⧸ Subgroup.normalClosure R) * v := by simp only [one_mul]
_ = (u : G ⧸ Subgroup.normalClosure R) * v := by
simpa using congrArg
(fun z : G ⧸ Subgroup.normalClosure R =>
z * (v : G ⧸ Subgroup.normalClosure R)) hu.symm
_ = ((u * v : G) : G ⧸ Subgroup.normalClosure R) := rfl
_ = 1 := huvProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The named operation preserves that normal closure by the appropriate closure property, monotonicity, quotient equality, or Tietze-map construction.
□theorem eq_one_of_mul_eq_one_right
(huv : RelatorEquivalent R (u * v) 1)
(hv : RelatorEquivalent R v 1) :
RelatorEquivalent R u 1If a right product is relator-equivalent to one and the right factor is trivial, the left factor is relator-equivalent to one.
Show proof
by
rw [relatorEquivalent_iff_eq_in_presentedQuotient] at huv hv ⊢
calc
(u : G ⧸ Subgroup.normalClosure R) =
(u : G ⧸ Subgroup.normalClosure R) * 1 := by simp only [mul_one]
_ = (u : G ⧸ Subgroup.normalClosure R) * v := by
simpa using congrArg
(fun z : G ⧸ Subgroup.normalClosure R =>
(u : G ⧸ Subgroup.normalClosure R) * z) hv.symm
_ = ((u * v : G) : G ⧸ Subgroup.normalClosure R) := rfl
_ = 1 := huvProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The named operation preserves that normal closure by the appropriate closure property, monotonicity, quotient equality, or Tietze-map construction.
□theorem mul_left (h : RelatorEquivalent R u v) (a : G) : RelatorEquivalent R (a * u) (a * v)Left multiplication by the same word preserves relator equivalence.
Show proof
mul (refl R a) hProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The named operation preserves that normal closure by the appropriate closure property, monotonicity, quotient equality, or Tietze-map construction.
□theorem mul_right (h : RelatorEquivalent R u v) (a : G) : RelatorEquivalent R (u * a) (v * a)Right multiplication by the same word preserves relator equivalence.
Show proof
mul h (refl R a)Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The named operation preserves that normal closure by the appropriate closure property, monotonicity, quotient equality, or Tietze-map construction.
□theorem context (h : RelatorEquivalent R u v) (a b : G) :
RelatorEquivalent R (a * u * b) (a * v * b)Replace a subword inside a two-sided context.
Show proof
mul_right (mul_left h a) bProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem conj (h : RelatorEquivalent R u v) (a : G) :
RelatorEquivalent R (a * u * a⁻¹) (a * v * a⁻¹)Conjugating both sides preserves relator equivalence.
theorem conj_eq_one (h : RelatorEquivalent R u 1) (a : G) :
RelatorEquivalent R (a * u * a⁻¹) 1If a word is relator-equivalent to the identity, then every conjugate of it is also relator-equivalent to the identity.
Show proof
by
simpa using conj h aProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The named operation preserves that normal closure by the appropriate closure property, monotonicity, quotient equality, or Tietze-map construction.
□theorem conj_pow_eq_one
{n : ℕ} (h : RelatorEquivalent R (u ^ n) 1) (a : G) :
RelatorEquivalent R ((a * u * a⁻¹) ^ n) 1If a power is relator-equivalent to the identity, then every conjugate of that power is also relator-equivalent to the identity.
Show proof
by
simpa [conjugate_pow_eq] using conj_eq_one h aProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The named operation preserves that normal closure by the appropriate closure property, monotonicity, quotient equality, or Tietze-map construction.
□theorem of_mem (hr : r ∈ R) : RelatorEquivalent R r 1The relator membership follows from the corresponding relator-equivalence criterion.
Show proof
by
simpa [RelatorEquivalent] using (Subgroup.subset_normalClosure hr :
r ∈ Subgroup.normalClosure R)Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem of_mem_normalClosure (hr : r ∈ Subgroup.normalClosure R) :
RelatorEquivalent R r 1Membership in the normal closure gives relator equivalence to the identity.
Show proof
by
simpa [RelatorEquivalent] using hrProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem mono (hR_to_S : R ⊆ S) (h : RelatorEquivalent R u v) :
RelatorEquivalent S u vRelator equivalence is monotone with respect to enlarging the relator family.
Show proof
by
have hx : u * v⁻¹ ∈ Subgroup.normalClosure S :=
Subgroup.normalClosure_mono hR_to_S
(by simpa [RelatorEquivalent] using h)
simpa [RelatorEquivalent] using hxProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem mono_iUnion {ι : Sort*} (R : ι → Set G)
(i : ι) (h : RelatorEquivalent (R i) u v) :
RelatorEquivalent (Set.iUnion R) u vRelator equivalence is monotone under an indexed union of relator families.
Show proof
mono (R := R i) (S := Set.iUnion R)
(fun _ hx => Set.mem_iUnion.2 ⟨i, hx⟩) hProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The named operation preserves that normal closure by the appropriate closure property, monotonicity, quotient equality, or Tietze-map construction.
□theorem mono_iUnion₂ {ι : Sort*} {κ : ι → Sort*}
(R : ∀ i : ι, κ i → Set G)
(i : ι) (j : κ i) (h : RelatorEquivalent (R i j) u v) :
RelatorEquivalent (Set.iUnion fun i : ι => Set.iUnion (R i)) u vRelator equivalence is monotone under a doubly indexed union of relator families.
Show proof
mono (R := R i j) (S := Set.iUnion fun i : ι => Set.iUnion (R i))
(fun _ hx => Set.mem_iUnion.2 ⟨i, Set.mem_iUnion.2 ⟨j, hx⟩⟩) hProof. Unfold the doubly indexed union and use monotonicity of normal closure under inclusion of relator sets.
□theorem mem_normalClosure_of_eq_one (h : RelatorEquivalent R r 1) :
r ∈ Subgroup.normalClosure RA relator-equivalence proof to the identity gives membership in the normal closure.
Show proof
by
simpa [RelatorEquivalent] using hProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem mul_inv_mem_normalClosure (h : RelatorEquivalent R u v) :
u * v⁻¹ ∈ Subgroup.normalClosure RIf two words are relator-equivalent, then multiplying one by the inverse of the other gives an element of the relator normal closure.
Show proof
by
simpa [RelatorEquivalent] using hProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem div_mem_normalClosure (h : RelatorEquivalent R u v) :
u / v ∈ Subgroup.normalClosure RIf two words are relator-equivalent, then their quotient lies in the normal closure of the relators.
Show proof
by
simpa [div_eq_mul_inv] using h.mul_inv_mem_normalClosureProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem mul_inv_eq_one (h : RelatorEquivalent R u v) :
RelatorEquivalent R (u * v⁻¹) 1Multiplying a word by the inverse of a relator-equivalent word gives a word relator-equivalent to one.
Show proof
of_mem_normalClosure h.mul_inv_mem_normalClosureProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The named operation preserves that normal closure by the appropriate closure property, monotonicity, quotient equality, or Tietze-map construction.
□theorem div_eq_one (h : RelatorEquivalent R u v) :
RelatorEquivalent R (u / v) 1A quotient word is relator-equivalent to the identity when its numerator and denominator are relator-equivalent to each other.
Show proof
by
simpa [div_eq_mul_inv] using h.mul_inv_eq_oneProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The named operation preserves that normal closure by the appropriate closure property, monotonicity, quotient equality, or Tietze-map construction.
□theorem one_eq_of_mem_inv (hr : r ∈ R) : RelatorEquivalent R 1 rThe relator membership follows from the corresponding relator-equivalence criterion.
Show proof
(of_mem hr).symmProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem mem_normalClosure_of_subset
(hR_to_S : R ⊆ S) {x : G}
(hx : x ∈ Subgroup.normalClosure R) :
x ∈ Subgroup.normalClosure SMembership in a normal closure is preserved when the relator set is enlarged.
Show proof
Subgroup.normalClosure_mono hR_to_S hxProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem mem_normalClosure_union_left
{x : G} (hx : x ∈ Subgroup.normalClosure R) :
x ∈ Subgroup.normalClosure (R ∪ S)Membership in the left normal closure implies membership in the normal closure of the union.
Show proof
mem_normalClosure_of_subset (R := R) (S := R ∪ S)
(Set.subset_union_left) hxProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem mem_normalClosure_union_right
{x : G} (hx : x ∈ Subgroup.normalClosure S) :
x ∈ Subgroup.normalClosure (R ∪ S)Membership in the right normal closure implies membership in the normal closure of the union.
Show proof
mem_normalClosure_of_subset (R := S) (S := R ∪ S)
(Set.subset_union_right) hxProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem mem_normalClosure_iUnion
{ι : Sort*} (R : ι → Set G) (i : ι)
{x : G} (hx : x ∈ Subgroup.normalClosure (R i)) :
x ∈ Subgroup.normalClosure (Set.iUnion R)Membership in the normal closure of an indexed union follows from membership in one indexed normal closure.
Show proof
mem_normalClosure_of_subset (R := R i) (S := Set.iUnion R)
(fun _ hy => Set.mem_iUnion.2 ⟨i, hy⟩) hxProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem mem_normalClosure_iUnion₂
{ι : Sort*} {κ : ι → Sort*}
(R : ∀ i : ι, κ i → Set G) (i : ι) (j : κ i)
{x : G} (hx : x ∈ Subgroup.normalClosure (R i j)) :
x ∈ Subgroup.normalClosure
(Set.iUnion fun i : ι => Set.iUnion (R i))Membership in the normal closure of a doubly indexed union follows from membership in one doubly indexed normal closure.
Show proof
mem_normalClosure_of_subset
(R := R i j)
(S := Set.iUnion fun i : ι => Set.iUnion (R i))
(fun _ hy => Set.mem_iUnion.2 ⟨i, Set.mem_iUnion.2 ⟨j, hy⟩⟩) hxProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem mem_normalClosure_iUnion₂_of_exists
{ι : Sort*} {κ : ι → Sort*}
(R : ∀ i : ι, κ i → Set G)
{x : G} (hx : ∃ i : ι, ∃ j : κ i,
x ∈ Subgroup.normalClosure (R i j)) :
x ∈ Subgroup.normalClosure
(Set.iUnion fun i : ι => Set.iUnion (R i))An explicit pair of indices gives membership in the normal closure of the doubly indexed union.
Show proof
by
rcases hx with ⟨i, j, hij⟩
exact mem_normalClosure_iUnion₂ (R := R) i j hijProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem maps_iUnion_relators_mem_normalClosure
{ι : Sort*} (f : G →* H) {R : ι → Set G} {S : Set H}
(hR : ∀ i : ι, ∀ r ∈ R i, f r ∈ Subgroup.normalClosure S) :
∀ r ∈ Set.iUnion R, f r ∈ Subgroup.normalClosure SMaps that preserve each indexed relator family send the union of the source relators into the target normal closure.
Show proof
by
intro r hr
rcases Set.mem_iUnion.1 hr with ⟨i, hi⟩
exact hR i r hiProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem maps_iUnion₂_relators_mem_normalClosure
{ι : Sort*} {κ : ι → Sort*}
(f : G →* H) {R : ∀ i : ι, κ i → Set G} {S : Set H}
(hR : ∀ i : ι, ∀ j : κ i, ∀ r ∈ R i j,
f r ∈ Subgroup.normalClosure S) :
∀ r ∈ Set.iUnion (fun i : ι => Set.iUnion (R i)),
f r ∈ Subgroup.normalClosure SMaps that preserve each doubly indexed relator family send the union of the source relators into the target normal closure.
Show proof
by
intro r hr
rcases Set.mem_iUnion.1 hr with ⟨i, hi⟩
rcases Set.mem_iUnion.1 hi with ⟨j, hj⟩
exact hR i j r hjProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem map_mem_normalClosure_of_relators
(f : G →* H) {R : Set G} {S : Set H}
(hR : ∀ r ∈ R, f r ∈ Subgroup.normalClosure S)
{x : G} (hx : x ∈ Subgroup.normalClosure R) :
f x ∈ Subgroup.normalClosure SA relator-preserving map sends relators into the normal closure of the target relator set.
Show proof
by
let N : Subgroup G := Subgroup.comap f (Subgroup.normalClosure S)
have hle : Subgroup.normalClosure R ≤ N := by
refine Subgroup.normalClosure_le_normal ?_
intro r hr
exact hR r hr
exact hle hxProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem hom_relatorEquivalent_of_maps_relators
(f : G →* H) {R : Set G} {S : Set H}
(hR : ∀ r ∈ R, f r ∈ Subgroup.normalClosure S)
{u v : G} (h : RelatorEquivalent R u v) :
RelatorEquivalent S (f u) (f v)A homomorphism preserves relator equivalence when each source relator maps into the target normal closure.
Show proof
by
have hx :
f (u * v⁻¹) ∈ Subgroup.normalClosure S :=
map_mem_normalClosure_of_relators f hR (by simpa [RelatorEquivalent] using h)
simpa [RelatorEquivalent, map_mul] using hxProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□theorem hom_relatorEquivalent_of_maps_relators_relatorEquivalent
(f : G →* H) {R : Set G} {S : Set H}
(hR : ∀ r ∈ R, RelatorEquivalent S (f r) 1)
{u v : G} (h : RelatorEquivalent R u v) :
RelatorEquivalent S (f u) (f v)A homomorphism preserves relator equivalence when each source relator maps to a target-relator-equivalent trivial word.
Show proof
hom_relatorEquivalent_of_maps_relators f
(fun r hr => RelatorEquivalent.mem_normalClosure_of_eq_one (hR r hr)) hProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□theorem map_mem_normalClosure_iUnion_of_relators
{ι : Sort*} (f : G →* H) {R : ι → Set G} {S : Set H}
(hR : ∀ i : ι, ∀ r ∈ R i, f r ∈ Subgroup.normalClosure S)
{x : G} (hx : x ∈ Subgroup.normalClosure (Set.iUnion R)) :
f x ∈ Subgroup.normalClosure SA mapped relator from an indexed family lies in the normal closure of the union of the mapped relator families.
Show proof
map_mem_normalClosure_of_relators f
(maps_iUnion_relators_mem_normalClosure f hR) hxProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem map_mem_normalClosure_iUnion₂_of_relators
{ι : Sort*} {κ : ι → Sort*}
(f : G →* H) {R : ∀ i : ι, κ i → Set G} {S : Set H}
(hR : ∀ i : ι, ∀ j : κ i, ∀ r ∈ R i j,
f r ∈ Subgroup.normalClosure S)
{x : G}
(hx : x ∈ Subgroup.normalClosure
(Set.iUnion fun i : ι => Set.iUnion (R i))) :
f x ∈ Subgroup.normalClosure SA mapped relator from a doubly indexed family lies in the normal closure of the union of the mapped relator families.
Show proof
map_mem_normalClosure_of_relators f
(maps_iUnion₂_relators_mem_normalClosure f hR) hxProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem hom_relatorEquivalent_of_maps_iUnion_relators
{ι : Sort*} (f : G →* H) {R : ι → Set G} {S : Set H}
(hR : ∀ i : ι, ∀ r ∈ R i, f r ∈ Subgroup.normalClosure S)
{u v : G} (h : RelatorEquivalent (Set.iUnion R) u v) :
RelatorEquivalent S (f u) (f v)A homomorphism preserves relator equivalence for an indexed union of relators when every source relator maps into the target normal closure.
Show proof
hom_relatorEquivalent_of_maps_relators f
(maps_iUnion_relators_mem_normalClosure f hR) hProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□theorem hom_relatorEquivalent_of_maps_iUnion_relators_relatorEquivalent
{ι : Sort*} (f : G →* H) {R : ι → Set G} {S : Set H}
(hR : ∀ i : ι, ∀ r ∈ R i, RelatorEquivalent S (f r) 1)
{u v : G} (h : RelatorEquivalent (Set.iUnion R) u v) :
RelatorEquivalent S (f u) (f v)A homomorphism preserves relator equivalence for an indexed union of relators when every source relator maps to a target-relator-equivalent trivial word.
Show proof
hom_relatorEquivalent_of_maps_iUnion_relators f
(fun i r hr => RelatorEquivalent.mem_normalClosure_of_eq_one (hR i r hr)) hProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□theorem hom_relatorEquivalent_of_maps_iUnion₂_relators
{ι : Sort*} {κ : ι → Sort*}
(f : G →* H) {R : ∀ i : ι, κ i → Set G} {S : Set H}
(hR : ∀ i : ι, ∀ j : κ i, ∀ r ∈ R i j,
f r ∈ Subgroup.normalClosure S)
{u v : G}
(h : RelatorEquivalent
(Set.iUnion fun i : ι => Set.iUnion (R i)) u v) :
RelatorEquivalent S (f u) (f v)A homomorphism preserves relator equivalence for a doubly indexed union of relators when every source relator maps into the target normal closure.
Show proof
hom_relatorEquivalent_of_maps_relators f
(maps_iUnion₂_relators_mem_normalClosure f hR) hProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated homomorphism or quotient operation preserves the doubly indexed relator normal closure, so it descends to the corresponding presented quotient.
□theorem hom_relatorEquivalent_of_maps_iUnion₂_relators_relatorEquivalent
{ι : Sort*} {κ : ι → Sort*}
(f : G →* H) {R : ∀ i : ι, κ i → Set G} {S : Set H}
(hR : ∀ i : ι, ∀ j : κ i, ∀ r ∈ R i j,
RelatorEquivalent S (f r) 1)
{u v : G}
(h : RelatorEquivalent
(Set.iUnion fun i : ι => Set.iUnion (R i)) u v) :
RelatorEquivalent S (f u) (f v)A homomorphism preserves relator equivalence for a doubly indexed union of relators when every source relator maps to a target-relator-equivalent trivial word.
Show proof
hom_relatorEquivalent_of_maps_iUnion₂_relators f
(fun i j r hr => RelatorEquivalent.mem_normalClosure_of_eq_one (hR i j r hr)) hProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated homomorphism or quotient operation preserves the doubly indexed relator normal closure, so it descends to the corresponding presented quotient.
□theorem freeGroup_relatorEquivalent_of_toWord_eq_reduce
[DecidableEq X]
{R : Set (FreeGroup X)} {u : FreeGroup X} {w : List (X × Bool)}
(h : u.toWord = FreeGroup.reduce w) :
RelatorEquivalent R u (FreeGroup.mk w)A free-group element is relator-equivalent to the word built from a list when its word representation reduces to that list.
Show proof
by
apply RelatorEquivalent.of_eq
rw [← FreeGroup.toWord_inj]
simp only [h, FreeGroup.toWord_mk]Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□theorem freeGroup_relatorEquivalent_mk_of_reduce_eq
[DecidableEq X]
{R : Set (FreeGroup X)} {u : FreeGroup X} {w : List (X × Bool)}
(h : FreeGroup.reduce w = u.toWord) :
RelatorEquivalent R (FreeGroup.mk w) uA free-group word is relator-equivalent to the word built from a list when their reduced words agree.
Show proof
(freeGroup_relatorEquivalent_of_toWord_eq_reduce
(R := R) (u := u) (w := w) h.symm).symmProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□def freeGroupSubstitutionWord {Y : Type*} [DecidableEq Y]
(f : X → FreeGroup Y) :
List (X × Bool) → List (Y × Bool)
| [] => []
| (x, true) :: xs => (f x).toWord ++ freeGroupSubstitutionWord f xs
| (x, false) :: xs => FreeGroup.invRev (f x).toWord ++ freeGroupSubstitutionWord f xs
@[simp]The substitution word is the free-group word used in the presentation comparison.
theorem freeGroupSubstitutionWord_nil {Y : Type*} [DecidableEq Y]
(f : X → FreeGroup Y) :
freeGroupSubstitutionWord f [] = []The relator-equivalence calculation follows from the product, inverse, conjugation, and substitution closure rules for normal closures.
Show proof
rfl
@[simp]Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem freeGroupSubstitutionWord_cons_true {Y : Type*} [DecidableEq Y]
(f : X → FreeGroup Y) (x : X) (xs : List (X × Bool)) :
freeGroupSubstitutionWord f ((x, true) :: xs) =
(f x).toWord ++ freeGroupSubstitutionWord f xsThe relator-equivalence calculation follows from the product, inverse, conjugation, and substitution closure rules for normal closures.
Show proof
rfl
@[simp]Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem freeGroupSubstitutionWord_cons_false {Y : Type*} [DecidableEq Y]
(f : X → FreeGroup Y) (x : X) (xs : List (X × Bool)) :
freeGroupSubstitutionWord f ((x, false) :: xs) =
FreeGroup.invRev (f x).toWord ++ freeGroupSubstitutionWord f xsThe relator-equivalence calculation follows from the product, inverse, conjugation, and substitution closure rules for normal closures.
Show proof
rflProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem freeGroupSubstitutionWord_append {Y : Type*} [DecidableEq Y]
(f : X → FreeGroup Y) (xs ys : List (X × Bool)) :
freeGroupSubstitutionWord f (xs ++ ys) =
freeGroupSubstitutionWord f xs ++ freeGroupSubstitutionWord f ysThe relator-equivalence calculation follows from the product, inverse, conjugation, and substitution closure rules for normal closures.
Show proof
by
induction xs with
| nil => simp
| cons xb xs ih =>
rcases xb with ⟨x, b⟩
cases b
· simp only [List.cons_append, freeGroupSubstitutionWord_cons_false, ih, List.append_assoc]
· simp only [List.cons_append, freeGroupSubstitutionWord_cons_true, ih, List.append_assoc]Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem freeGroup_mk_substitutionWord {Y : Type*} [DecidableEq Y]
(f : X → FreeGroup Y) (xs : List (X × Bool)) :
FreeGroup.mk (freeGroupSubstitutionWord f xs) =
FreeGroup.lift f (FreeGroup.mk xs)The substitution word is the free-group word used in the presentation comparison.
Show proof
by
induction xs with
| nil => exact FreeGroup.one_eq_mk.symm
| cons xb xs ih =>
rcases xb with ⟨x, b⟩
cases b
· rw [freeGroupSubstitutionWord_cons_false, ← FreeGroup.mul_mk,
← FreeGroup.inv_mk, FreeGroup.mk_toWord, ih]
simp only [FreeGroup.lift_mk, List.map_cons, cond_false, List.prod_cons]
· rw [freeGroupSubstitutionWord_cons_true, ← FreeGroup.mul_mk,
FreeGroup.mk_toWord, ih]
simp only [FreeGroup.lift_mk, List.map_cons, cond_true, List.prod_cons]Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem freeGroup_toWord_lift_mk {Y : Type*} [DecidableEq Y]
(f : X → FreeGroup Y) (xs : List (X × Bool)) :
(FreeGroup.lift f (FreeGroup.mk xs)).toWord =
FreeGroup.reduce (freeGroupSubstitutionWord f xs)The lifted generator maps to the corresponding word in the free-group presentation.
Show proof
by
rw [← freeGroup_mk_substitutionWord (f := f) (xs := xs)]
simp only [FreeGroup.toWord_mk]Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem freeGroup_lift_mk_eq_mk_of_substitutionWord_reduce_eq
{Y : Type*} [DecidableEq Y]
{f : X → FreeGroup Y} {xs : List (X × Bool)}
{ys : List (Y × Bool)}
(h :
FreeGroup.reduce (freeGroupSubstitutionWord f xs) =
FreeGroup.reduce ys) :
FreeGroup.lift f (FreeGroup.mk xs) = FreeGroup.mk ysThe free-group lift of a reduced substitution word agrees with the corresponding generator.
Show proof
by
rw [← FreeGroup.toWord_inj]
rw [freeGroup_toWord_lift_mk, FreeGroup.toWord_mk, h]Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem freeGroup_relatorEquivalent_lift_mk_of_substitutionWord_reduce_eq
{Y : Type*} [DecidableEq Y]
{R : Set (FreeGroup Y)}
{f : X → FreeGroup Y} {xs : List (X × Bool)}
{ys : List (Y × Bool)}
(h :
FreeGroup.reduce (freeGroupSubstitutionWord f xs) =
FreeGroup.reduce ys) :
RelatorEquivalent R (FreeGroup.lift f (FreeGroup.mk xs))
(FreeGroup.mk ys)A lifted generator word is relator-equivalent to the corresponding word when the substitution word has the stated reduction.
Show proof
RelatorEquivalent.of_eq
(freeGroup_lift_mk_eq_mk_of_substitutionWord_reduce_eq h)Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□theorem freeGroup_relatorEquivalent_lift_mk_one_of_substitutionWord_reduce_eq
{Y : Type*} [DecidableEq Y]
{R : Set (FreeGroup Y)}
{f : X → FreeGroup Y} {xs : List (X × Bool)}
{ys : List (Y × Bool)}
(h :
FreeGroup.reduce (freeGroupSubstitutionWord f xs) =
FreeGroup.reduce ys)
(hy : RelatorEquivalent R (FreeGroup.mk ys) 1) :
RelatorEquivalent R (FreeGroup.lift f (FreeGroup.mk xs)) 1A lifted generator word is relator-equivalent to the identity when its substitution word reduces to the empty word.
Show proof
(freeGroup_relatorEquivalent_lift_mk_of_substitutionWord_reduce_eq
(R := R) h).trans hyProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□theorem freeGroup_lift_relatorEquivalent_of_generator_relatorEquivalent
{R : Set G} {f g : X → G}
(h : ∀ x : X, RelatorEquivalent R (f x) (g x))
(w : FreeGroup X) :
RelatorEquivalent R (FreeGroup.lift f w) (FreeGroup.lift g w)A free-group lift preserves relator equivalence when the generator images are relator-equivalent.
Show proof
by
let N : Subgroup G := Subgroup.normalClosure R
let F : FreeGroup X →* G ⧸ N :=
(QuotientGroup.mk' N).comp (FreeGroup.lift f)
let K : FreeGroup X →* G ⧸ N :=
(QuotientGroup.mk' N).comp (FreeGroup.lift g)
have hhom : F = K := by
ext x
dsimp [F, K]
simp only [FreeGroup.lift_apply_of]
rw [← relatorEquivalent_iff_eq_in_presentedQuotient]
exact h x
have hw := congrArg (fun φ : FreeGroup X →* G ⧸ N => φ w) hhom
change ((FreeGroup.lift f w : G) : G ⧸ N) =
((FreeGroup.lift g w : G) : G ⧸ N) at hw
exact relatorEquivalent_iff_eq_in_presentedQuotient.2 hwProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□theorem freeGroup_lift_relatorEquivalent_one_of_generator_relatorEquivalent
{R : Set G} {f : X → G}
(h : ∀ x : X, RelatorEquivalent R (f x) 1)
(w : FreeGroup X) :
RelatorEquivalent R (FreeGroup.lift f w) 1A free-group lift sends the word to a relator-equivalent trivial word when the generator images are relator-equivalent to one.
Show proof
by
let trivialLift : FreeGroup X →* G :=
FreeGroup.lift (fun _ : X => (1 : G))
have htrivial : trivialLift w = 1 := by
have hhom : trivialLift = 1 := by
ext x
simp only [FreeGroup.lift_apply_of, MonoidHom.one_apply, trivialLift]
exact congrArg (fun φ : FreeGroup X →* G => φ w) hhom
simpa [trivialLift, htrivial] using
freeGroup_lift_relatorEquivalent_of_generator_relatorEquivalent
(R := R) (f := f) (g := fun _ : X => (1 : G)) h wProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□theorem freeGroup_lift_relatorEquivalent_of_generator_eq
{R : Set G} {f g : X → G}
(h : ∀ x : X, f x = g x)
(w : FreeGroup X) :
RelatorEquivalent R (FreeGroup.lift f w) (FreeGroup.lift g w)A free-group lift preserves relator equivalence when the generator images are equal.
Show proof
freeGroup_lift_relatorEquivalent_of_generator_relatorEquivalent
(R := R) (f := f) (g := g)
(fun x => RelatorEquivalent.of_eq (h x)) wProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□theorem normalClosure_eq_of_relatorEquivalent
(hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)
(hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :
Subgroup.normalClosure R = Subgroup.normalClosure SIf every relator on each side is trivial modulo the other side, the normal closures are equal.
Show proof
by
apply le_antisymm
· refine Subgroup.normalClosure_le_normal ?_
intro r hr
exact RelatorEquivalent.mem_normalClosure_of_eq_one (hR_to_S r hr)
· refine Subgroup.normalClosure_le_normal ?_
intro s hs
exact RelatorEquivalent.mem_normalClosure_of_eq_one (hS_to_R s hs)Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem normalClosure_insert_eq_of_mem
(hr : r ∈ Subgroup.normalClosure R) :
Subgroup.normalClosure (insert r R) = Subgroup.normalClosure RInserting an element already in the normal closure does not change the normal closure.
Show proof
by
apply le_antisymm
· refine Subgroup.normalClosure_le_normal ?_
intro x hx
rcases hx with rfl | hx
· exact hr
· exact Subgroup.subset_normalClosure hx
· exact Subgroup.normalClosure_mono (by
intro x hx
exact Set.mem_insert_of_mem r hx)Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem normalClosure_diff_singleton_eq_of_mem
(hr : r ∈ Subgroup.normalClosure (R \ {r})) :
Subgroup.normalClosure R = Subgroup.normalClosure (R \ {r})Removing a relator that already lies in the normal closure of the remaining relators does not change the normal closure.
Show proof
by
apply le_antisymm
· refine Subgroup.normalClosure_le_normal ?_
intro x hx
by_cases hxr : x = r
· simpa [hxr] using hr
· exact Subgroup.subset_normalClosure ⟨hx, by simpa [Set.mem_singleton_iff] using hxr⟩
· exact Subgroup.normalClosure_mono (by
intro x hx
exact hx.1)Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem normalClosure_eq_of_subset_normalClosure
(hR_to_S : R ⊆ Subgroup.normalClosure S)
(hS_to_R : S ⊆ Subgroup.normalClosure R) :
Subgroup.normalClosure R = Subgroup.normalClosure STwo relator normal closures are equal when each relator family is contained in the normal closure generated by the other.
Show proof
by
apply le_antisymm
· exact Subgroup.normalClosure_le_normal hR_to_S
· exact Subgroup.normalClosure_le_normal hS_to_RProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem conjugate_mem_normalClosure_of_mem
(hr : r ∈ R) (a : G) :
a * r * a⁻¹ ∈ Subgroup.normalClosure RA conjugate of a relator lies in the normal closure generated by the relator set.
Show proof
by
simpa [mul_assoc] using
(Subgroup.normalClosure_normal.conj_mem r
(Subgroup.subset_normalClosure hr) a)Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem conjugate_mem_normalClosure
(hr : r ∈ Subgroup.normalClosure R) (a : G) :
a * r * a⁻¹ ∈ Subgroup.normalClosure RA conjugate of a relator belongs to the normal closure of the relator set.
Show proof
by
simpa [mul_assoc] using
(Subgroup.normalClosure_normal.conj_mem r hr a)Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem cyclic_rotation_mem_normalClosure
(h : a * b ∈ Subgroup.normalClosure R) :
b * a ∈ Subgroup.normalClosure RCyclically rotating a relator keeps it in the same normal closure.
Show proof
by
have hc := conjugate_mem_normalClosure (R := R) h b
simpa [mul_assoc] using hcProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem mem_of_left_mul_mem_normalClosure
{a b : G}
(ha : a ∈ Subgroup.normalClosure R)
(hab : a * b ∈ Subgroup.normalClosure R) :
b ∈ Subgroup.normalClosure RIf left multiplication by a relator-normal-closure element gives membership, then the original element has the same membership property.
Show proof
by
let N : Subgroup G := Subgroup.normalClosure R
have h : a⁻¹ * (a * b) ∈ N := N.mul_mem (N.inv_mem ha) hab
simpa [N, mul_assoc] using hProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem cyclic_rotation_pow_mem_normalClosure
{a b : G} {n : ℕ}
(h : (a * b) ^ n ∈ Subgroup.normalClosure R) :
(b * a) ^ n ∈ Subgroup.normalClosure RA cyclic rotation of a power relator belongs to the normal closure of the original relator set.
Show proof
by
let N : Subgroup G := Subgroup.normalClosure R
have hconj : b * ((a * b) ^ n) * b⁻¹ ∈ N := by
simpa [N, MulAut.conj_apply] using
(Subgroup.normalClosure_normal.conj_mem ((a * b) ^ n) h b)
have hpow : b * ((a * b) ^ n) * b⁻¹ = (b * a) ^ n := by
clear h hconj
induction n with
| zero =>
simp only [pow_zero, mul_one, mul_inv_cancel]
| succ n ih =>
rw [pow_succ, pow_succ, ← ih]
group
simpa [hpow] using hconjProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem pow_mem_normalClosure_of_mul_inv_mem
{u v : G} {n : ℕ}
(huv : u * v⁻¹ ∈ Subgroup.normalClosure R)
(hv : v ^ n ∈ Subgroup.normalClosure R) :
u ^ n ∈ Subgroup.normalClosure RIf u and v are congruent modulo the normal closure and a power of v lies in it, then the same power of u lies in it.
Show proof
by
let N : Subgroup G := Subgroup.normalClosure R
let q : G →* G ⧸ N := QuotientGroup.mk' N
have hq : q u = q v := by
exact
(QuotientGroup.eq_iff_div_mem (N := N) (x := u) (y := v)).2
(by simpa [N, div_eq_mul_inv] using huv)
have hqv : q (v ^ n) = 1 :=
(QuotientGroup.eq_one_iff (N := N) (v ^ n)).2 hv
have hqu : q (u ^ n) = 1 := by
rw [map_pow, hq, ← map_pow]
exact hqv
exact (QuotientGroup.eq_one_iff (N := N) (u ^ n)).1 hquProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem list_prod_mem_normalClosure
{l : List G}
(h : ∀ x ∈ l, x ∈ Subgroup.normalClosure R) :
l.prod ∈ Subgroup.normalClosure RThe product of a list of relators belongs to the normal closure of the relator set.
Show proof
by
induction l with
| nil =>
simp only [List.prod_nil, one_mem]
| cons x xs ih =>
simp only [List.mem_cons] at h
exact Subgroup.mul_mem (Subgroup.normalClosure R)
(h x (Or.inl rfl))
(ih (by
intro y hy
exact h y (Or.inr hy)))Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem list_prod_map_relatorEquivalent
{ι : Type*} (l : List ι) {f g : ι → G}
(h : ∀ i ∈ l, RelatorEquivalent R (f i) (g i)) :
RelatorEquivalent R (l.map f).prod (l.map g).prodMapping a list through relator-equivalent entries preserves relator equivalence of the product.
Show proof
by
induction l with
| nil =>
exact RelatorEquivalent.refl R 1
| cons i is ih =>
simp only [List.mem_cons] at h
simpa using RelatorEquivalent.mul
(h i (Or.inl rfl))
(ih (by
intro j hj
exact h j (Or.inr hj)))Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□theorem list_prod_map_relatorEquivalent_one
{ι : Type*} (l : List ι) {f : ι → G}
(h : ∀ i ∈ l, RelatorEquivalent R (f i) 1) :
RelatorEquivalent R (l.map f).prod 1A list product is relator-equivalent to the identity when every mapped entry is relator-equivalent to the identity.
Show proof
by
simpa using
list_prod_map_relatorEquivalent (R := R) l
(f := f) (g := fun _ => (1 : G)) hProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□theorem list_prod_map_inv_reverse (l : List G) :
(l.map Inv.inv).reverse.prod = l.prod⁻¹The product of the reversed inverse list agrees with the inverse of the list product.
Show proof
by
induction l with
| nil =>
simp only [List.map_nil, List.reverse_nil, List.prod_nil, inv_one]
| cons x xs ih =>
simp only [List.map_cons, List.reverse_cons, List.prod_append, ih, List.prod_cons, List.prod_nil, mul_one,
mul_inv_rev]Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem list_prod_reverse_map_inv (l : List G) :
(l.reverse.map Inv.inv).prod = l.prod⁻¹The product of the reversed inverse list agrees with the inverse of the list product.
Show proof
by
simpa [List.map_reverse] using list_prod_map_inv_reverse (G := G) lProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem list_prod_reverse_inv_relatorEquivalent
{l m : List G}
(h : RelatorEquivalent R l.prod m.prod) :
RelatorEquivalent R (l.reverse.map Inv.inv).prod
(m.reverse.map Inv.inv).prodA list product is relator-equivalent to the inverse of the reversed inverse list product.
Show proof
by
simpa [List.map_reverse, list_prod_map_inv_reverse] using
RelatorEquivalent.inv hProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□theorem list_prod_append_relatorEquivalent
{l₁ l₂ m₁ m₂ : List G}
(h₁ : RelatorEquivalent R l₁.prod m₁.prod)
(h₂ : RelatorEquivalent R l₂.prod m₂.prod) :
RelatorEquivalent R (l₁ ++ l₂).prod (m₁ ++ m₂).prodAppending relator-equivalent list products preserves relator equivalence.
Show proof
by
simpa using RelatorEquivalent.mul h₁ h₂Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□theorem list_prod_append_left_relatorEquivalent
(l : List G) {m n : List G}
(h : RelatorEquivalent R m.prod n.prod) :
RelatorEquivalent R (l ++ m).prod (l ++ n).prodLeft-appending the same list product preserves relator equivalence.
Show proof
by
exact list_prod_append_relatorEquivalent
(R := R) (l₁ := l) (l₂ := m) (m₁ := l) (m₂ := n)
(RelatorEquivalent.refl R l.prod) hProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□theorem list_prod_middle_eq_one_relatorEquivalent
(l m : List G) {u : G}
(h : RelatorEquivalent R u 1) :
RelatorEquivalent R (l ++ u :: m).prod (l ++ m).prodRemoving a middle subproduct equal to one preserves relator equivalence of the list product.
Show proof
by
have htail :
RelatorEquivalent R (u :: m).prod m.prod := by
simpa using RelatorEquivalent.mul h (RelatorEquivalent.refl R m.prod)
simpa [List.singleton_append] using
list_prod_append_left_relatorEquivalent (R := R) l htailProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□theorem list_prod_middle_mul_inv_relatorEquivalent
(l m : List G) {u v : G}
(h : RelatorEquivalent R u v) :
RelatorEquivalent R (l ++ (u * v⁻¹) :: m).prod
(l ++ m).prodInserting or removing a middle product multiplied by its inverse preserves relator equivalence.
Show proof
list_prod_middle_eq_one_relatorEquivalent (R := R) l m
(RelatorEquivalent.mul_inv_eq_one h)Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□theorem list_prod_append_rotate_mem_normalClosure
{l m : List G}
(h : (l ++ m).prod ∈ Subgroup.normalClosure R) :
(m ++ l).prod ∈ Subgroup.normalClosure RRotating an appended list product gives an element of the relator normal closure.
Show proof
by
have hprod : l.prod * m.prod ∈ Subgroup.normalClosure R := by
simpa using h
have hrot :
m.prod * l.prod ∈ Subgroup.normalClosure R :=
cyclic_rotation_mem_normalClosure (R := R)
(a := l.prod) (b := m.prod) hprod
simpa using hrotProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem list_prod_append_rotate_relatorEquivalent
{l m : List G}
(h : RelatorEquivalent R (l ++ m).prod 1) :
RelatorEquivalent R (m ++ l).prod 1A rotated append decomposition of a list product is relator-equivalent to the original product.
Show proof
by
exact RelatorEquivalent.of_mem_normalClosure
(list_prod_append_rotate_mem_normalClosure (R := R)
(by simpa [RelatorEquivalent] using h))Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□theorem list_prod_rotate_to_front_relatorEquivalent
{l m : List G}
(h : RelatorEquivalent R (l ++ m).prod 1) :
RelatorEquivalent R (m ++ l).prod 1Rotating a list segment to the front preserves relator equivalence of the product.
Show proof
list_prod_append_rotate_relatorEquivalent (R := R) hProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□theorem list_prod_take_drop_rotate_relatorEquivalent
(l : List G) (n : ℕ)
(h : RelatorEquivalent R l.prod 1) :
RelatorEquivalent R ((l.drop n) ++ (l.take n)).prod 1The take/drop rotation of a list product is relator-equivalent to the original product.
Show proof
by
have hsplit :
RelatorEquivalent R ((l.take n) ++ (l.drop n)).prod 1 := by
simpa [List.take_append_drop] using h
exact list_prod_append_rotate_relatorEquivalent (R := R) hsplitProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□theorem list_prod_take_drop_rotate_mem_normalClosure
(l : List G) (n : ℕ)
(h : l.prod ∈ Subgroup.normalClosure R) :
((l.drop n) ++ (l.take n)).prod ∈ Subgroup.normalClosure RA take-drop rotation of a list product belongs to the relator normal closure.
Show proof
RelatorEquivalent.mem_normalClosure_of_eq_one
(list_prod_take_drop_rotate_relatorEquivalent (R := R) l n
(RelatorEquivalent.of_mem_normalClosure (by simpa [RelatorEquivalent] using h)))Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem orderedFinsetProduct_mem_normalClosure
(s : Finset ι) {f : ι → G}
(h : ∀ i ∈ s, f i ∈ Subgroup.normalClosure R) :
orderedFinsetProduct s f ∈ Subgroup.normalClosure RShow proof
by
unfold orderedFinsetProduct
exact list_prod_mem_normalClosure (R := R) (by
intro x hx
rcases List.mem_map.1 hx with ⟨i, hi, rfl⟩
exact h i (by
exact (Finset.mem_sort (s := s) (r := fun a b : ι => a ≤ b)).1 hi))Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem orderedFinsetProduct_relatorEquivalent
(s : Finset ι) {f g : ι → G}
(h : ∀ i ∈ s, RelatorEquivalent R (f i) (g i)) :
RelatorEquivalent R (orderedFinsetProduct s f)
(orderedFinsetProduct s g)Replacing each term of an ordered finite product by a relator-equivalent term preserves relator equivalence.
Show proof
by
unfold orderedFinsetProduct
exact list_prod_map_relatorEquivalent (R := R) (s.sort (· ≤ ·))
(f := f) (g := g) (by
intro i hi
exact h i (by
exact (Finset.mem_sort (s := s) (r := fun a b : ι => a ≤ b)).1 hi))Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□theorem orderedFinsetProduct_relatorEquivalent_one
(s : Finset ι) {f : ι → G}
(h : ∀ i ∈ s, RelatorEquivalent R (f i) 1) :
RelatorEquivalent R (orderedFinsetProduct s f) 1An ordered finite product is relator-equivalent to the identity when every term is relator-equivalent to the identity.
Show proof
by
unfold orderedFinsetProduct
simpa using
list_prod_map_relatorEquivalent_one (R := R) (s.sort (· ≤ ·))
(f := f) (by
intro i hi
exact h i (by
exact (Finset.mem_sort (s := s) (r := fun a b : ι => a ≤ b)).1 hi))Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The stated word, list-product, homomorphism, or quotient operation preserves that normal closure by closure under multiplication, inversion, conjugation, substitution, and passage to the presented quotient.
□theorem orderedFinsetProduct_congr
(s : Finset ι) {f g : ι → G}
(h : ∀ i ∈ s, f i = g i) :
orderedFinsetProduct s f = orderedFinsetProduct s gThe relator-equivalence calculation follows from the product, inverse, conjugation, and substitution closure rules for normal closures.
Show proof
by
unfold orderedFinsetProduct
congr 1
apply List.map_congr_left
intro i hi
exact h i ((Finset.mem_sort (s := s) (r := fun a b : ι => a ≤ b)).1 hi)Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem conjugate_list_prod {G : Type*} [Group G] (x : G) :
∀ l : List G, x * l.prod * x⁻¹ = (l.map fun t => x * t * x⁻¹).prod
| [] => by
simp only [List.prod_nil, mul_one, mul_inv_cancel, List.map_nil]
| t :: ts => by
rw [List.prod_cons, List.map_cons, List.prod_cons]
calc
x * (t * ts.prod) * x⁻¹ = (x * t * x⁻¹) * (x * ts.prod * x⁻¹)The relator-equivalence calculation follows from the product, inverse, conjugation, and substitution closure rules for normal closures.
Show proof
by
group
_ = x * t * x⁻¹ * (List.map (fun t => x * t * x⁻¹) ts).prod := by
rw [conjugate_list_prod x ts]Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem nested_conjugate_list_prod {G : Type*} [Group G]
(x : G) {p n : ℕ} (f : Fin p → Fin n → G) :
(List.ofFn (fun b : Fin p =>
(List.ofFn (fun j : Fin n => x * f b j * x⁻¹)).prod)).prod =
x * (List.ofFn (fun b : Fin p =>
(List.ofFn (fun j : Fin n => f b j)).prod)).prod * x⁻¹The relator-equivalence calculation follows from the product, inverse, conjugation, and substitution closure rules for normal closures.
Show proof
by
have hinner :
(List.ofFn (fun b : Fin p =>
(List.ofFn (fun j : Fin n => x * f b j * x⁻¹)).prod)) =
List.ofFn (fun b : Fin p =>
x * (List.ofFn (fun j : Fin n => f b j)).prod * x⁻¹) := by
apply List.ofFn_inj.2
funext b
simpa using
(conjugate_list_prod x (List.ofFn (fun j : Fin n => f b j))).symm
rw [hinner]
simpa using
(conjugate_list_prod x
(List.ofFn (fun b : Fin p =>
(List.ofFn (fun j : Fin n => f b j)).prod))).symmProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem subgroup_list_prod_val {G : Type*} [Group G]
{H : Subgroup G} {n : ℕ} (f : Fin n → H) :
(((List.ofFn f).prod : H) : G) =
(List.ofFn (fun i : Fin n => ((f i : H) : G))).prodThe value of a subgroup list product is the product of the underlying subgroup elements.
Show proof
by
change H.subtype ((List.ofFn f).prod) =
(List.ofFn (fun i : Fin n => ((f i : H) : G))).prod
rw [map_list_prod, List.map_ofFn]
apply congrArg List.prod
apply List.ofFn_inj.2
funext i
rflProof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem subgroup_nested_list_prod_val {G : Type*} [Group G]
{H : Subgroup G} {p n : ℕ} (f : Fin p → Fin n → H) :
(((List.ofFn (fun b : Fin p =>
(List.ofFn (fun j : Fin n => f b j)).prod)).prod : H) : G) =
(List.ofFn (fun b : Fin p =>
(List.ofFn (fun j : Fin n => ((f b j : H) : G))).prod)).prodThe subgroup nested list product underlying value is evaluated by the displayed coordinate or generator-level formula in the Reidemeister--Schreier rewriting system.
Show proof
by
change H.subtype
((List.ofFn (fun b : Fin p =>
(List.ofFn (fun j : Fin n => f b j)).prod)).prod) =
(List.ofFn (fun b : Fin p =>
(List.ofFn (fun j : Fin n => ((f b j : H) : G))).prod)).prod
rw [map_list_prod, List.map_ofFn]
apply congrArg List.prod
apply List.ofFn_inj.2
funext b
exact subgroup_list_prod_val (fun j : Fin n => f b j)Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□theorem freeGroup_endomorph_mul_inv_mem_normalClosure_of_generator_mul_inv
{Y : Type*} (R : Set (FreeGroup Y)) (F : FreeGroup Y →* FreeGroup Y)
(hgen :
∀ y : Y,
F (FreeGroup.of y) * (FreeGroup.of y)⁻¹ ∈ Subgroup.normalClosure R) :
∀ w : FreeGroup Y, F w * w⁻¹ ∈ Subgroup.normalClosure RIf an endomorphism is congruent to the identity on generators modulo a normal closure, then it is congruent to the identity on every free-group word.
Show proof
by
classical
let N : Subgroup (FreeGroup Y) := Subgroup.normalClosure R
let q : FreeGroup Y →* FreeGroup Y ⧸ N := QuotientGroup.mk' N
have hq : q.comp F = q := by
apply FreeGroup.ext_hom
intro y
change q (F (FreeGroup.of y)) = q (FreeGroup.of y)
exact
(QuotientGroup.eq_iff_div_mem
(N := N) (x := F (FreeGroup.of y)) (y := FreeGroup.of y)).2
(by simpa [N, div_eq_mul_inv] using hgen y)
intro w
have hw :
q (F w) = q w := by
simpa using congrArg (fun ψ : FreeGroup Y →* FreeGroup Y ⧸ N => ψ w) hq
exact
(QuotientGroup.eq_iff_div_mem (N := N) (x := F w) (y := w)).1
(by simpa [N, div_eq_mul_inv] using hw)Proof. Unfold relator equivalence as equality modulo the normal closure generated by the relator family. The word operations preserve the normal closure by closure under multiplication, inversion, conjugation, and substitution. The quotient maps therefore agree precisely when the corresponding lifted words differ by an element of that normal closure, giving the presentation comparison.
□