This module defines equality modulo a relator normal closure and proves its elementary equivalence, congruence, inversion, multiplication, and quotient characterizations.
Equality modulo the normal closure generated by R.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]def RelatorEquivalent (R : Set G) (u v : G) : PropRelator equivalence is equivalent to equality in the presented quotient.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]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 to one on the right is membership in the relator normal closure.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]theorem relatorEquivalent_one_right {R : Set G} {u : G} :
RelatorEquivalent R u 1 ↔ u ∈ Subgroup.normalClosure RRelator equivalence from one on the left is membership in the relator normal closure.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]theorem relatorEquivalent_one_left {R : Set G} {u : G} :
RelatorEquivalent R 1 u ↔ u ∈ Subgroup.normalClosure RRelator equivalence defines a setoid on the free group.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]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 is reflexive.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem refl (R : Set G) (u : G) : RelatorEquivalent R u uEqual relators are relator-equivalent.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem of_eq (h : u = v) : RelatorEquivalent R u vRelator equivalence is symmetric.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem symm (h : RelatorEquivalent R u v) : RelatorEquivalent R v uRelator equivalence is transitive.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem trans (h₁ : RelatorEquivalent R u v) (h₂ : RelatorEquivalent R v w) : RelatorEquivalent
R u wTaking inverses preserves relator equivalence.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem inv (h : RelatorEquivalent R u v) : RelatorEquivalent R u⁻¹ v⁻¹Multiplication of relator-equivalent words preserves relator equivalence.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem mul (h₁ : RelatorEquivalent R u v) (h₂ : RelatorEquivalent R a b) :
RelatorEquivalent R (u * a) (v * b)Taking natural powers preserves relator equivalence.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem pow (h : RelatorEquivalent R u v) (n : ℕ) : RelatorEquivalent R (u ^ n) (v ^ n)Taking integer powers preserves relator equivalence.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem zpow (h : RelatorEquivalent R u v) (n : ℤ) : RelatorEquivalent R (u ^ n) (v ^ n)A product of words relator-equivalent to one is relator-equivalent to one.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem mul_eq_one (h₁ : RelatorEquivalent R u 1) (h₂ : RelatorEquivalent R v 1) :
RelatorEquivalent R (u * v) 1A natural-number power is relator-equivalent to the identity when the base word is relator-equivalent to the identity.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem pow_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.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem zpow_eq_one (h : RelatorEquivalent R u 1) (n : ℤ) :
RelatorEquivalent R (u ^ n) 1The inverse of a word is relator-equivalent to one exactly when the word is.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem inv_eq_one (h : RelatorEquivalent R u 1) :
RelatorEquivalent R u⁻¹ 1Conjugating a power relator gives an equivalent relator.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem conjugate_pow_eq (a u : G) (n : ℕ) :
(a * u * a⁻¹) ^ n = a * u ^ n * a⁻¹A product is trivial modulo the relators exactly when its first factor equals the inverse of the second.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem mul_eq_one_iff_eq_inv :
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.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem eq_inv_of_mul_eq_one (h : RelatorEquivalent R (u * v) 1) :
RelatorEquivalent R u v⁻¹A product is relator-equivalent to the identity when one factor is relator-equivalent to the inverse of the other.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem mul_eq_one_of_eq_inv (h : RelatorEquivalent R u v⁻¹) :
RelatorEquivalent R (u * v) 1If a left product is relator-equivalent to one and the left factor is trivial, the right factor is relator-equivalent to one.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem eq_one_of_mul_eq_one_left
(hu : RelatorEquivalent R u 1)
(huv : RelatorEquivalent R (u * v) 1) :
RelatorEquivalent R v 1If a right product is relator-equivalent to one and the right factor is trivial, the left factor is relator-equivalent to one.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem eq_one_of_mul_eq_one_right
(huv : RelatorEquivalent R (u * v) 1)
(hv : RelatorEquivalent R v 1) :
RelatorEquivalent R u 1Left multiplication by the same word preserves relator equivalence.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem mul_left (h : RelatorEquivalent R u v) (a : G) : RelatorEquivalent R (a * u) (a * v)Right multiplication by the same word preserves relator equivalence.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem mul_right (h : RelatorEquivalent R u v) (a : G) : RelatorEquivalent R (u * a) (v * a)Replace a subword inside a two-sided context.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem context (h : RelatorEquivalent R u v) (a b : G) :
RelatorEquivalent R (a * u * b) (a * v * b)Conjugating both sides preserves relator equivalence.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem conj (h : RelatorEquivalent R u v) (a : G) :
RelatorEquivalent R (a * u * a⁻¹) (a * v * a⁻¹)If a word is relator-equivalent to the identity, then every conjugate of it is also relator-equivalent to the identity.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem conj_eq_one (h : RelatorEquivalent R u 1) (a : G) :
RelatorEquivalent R (a * u * a⁻¹) 1If a power is relator-equivalent to the identity, then every conjugate of that power is also relator-equivalent to the identity.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem conj_pow_eq_one
{n : ℕ} (h : RelatorEquivalent R (u ^ n) 1) (a : G) :
RelatorEquivalent R ((a * u * a⁻¹) ^ n) 1Every defining relator is equivalent to the identity.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem of_mem (hr : r ∈ R) : RelatorEquivalent R r 1Membership in the normal closure gives relator equivalence to the identity.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem of_mem_normalClosure (hr : r ∈ Subgroup.normalClosure R) :
RelatorEquivalent R r 1Relator equivalence is monotone with respect to enlarging the relator family.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem mono (hR_to_S : R ⊆ S) (h : RelatorEquivalent R u v) :
RelatorEquivalent S u vRelator equivalence is monotone under an indexed union of relator families.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem mono_iUnion {ι : Sort*} (R : ι → Set G)
(i : ι) (h : RelatorEquivalent (R i) u v) :
RelatorEquivalent (Set.iUnion R) u vRelator equivalence is monotone under a doubly indexed union of relator families.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}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 v :=
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⟩⟩) hA relator-equivalence certificate to the identity gives membership in the normal closure.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem mem_normalClosure_of_eq_one (h : RelatorEquivalent R r 1) :
r ∈ 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.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem mul_inv_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.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem div_mem_normalClosure (h : RelatorEquivalent R u v) :
u / v ∈ Subgroup.normalClosure RMultiplying a word by the inverse of a relator-equivalent word gives a word relator-equivalent to one.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem mul_inv_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.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem div_eq_one (h : RelatorEquivalent R u v) :
RelatorEquivalent R (u / v) 1The identity is equivalent to every defining relator.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
namespace RelatorEquivalent
variable {R S : Set G} {u v w a b r : G}theorem one_eq_of_mem_inv (hr : r ∈ R) : RelatorEquivalent R 1 r