ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Basic

Definition ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent

def RelatorEquivalent (R : Set G) (u v : G) : Prop :=
  u * v⁻¹ ∈ Subgroup.normalClosure R

Equality modulo the normal closure generated by R.

Theorem ReidemeisterSchreier.Discrete.Presentations.relatorEquivalent_iff_eq_in_presentedQuotient

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 Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.relatorEquivalent_one_right

@[simp] theorem relatorEquivalent_one_right {R : Set G} {u : G} :
    RelatorEquivalent R u 1 ↔ u ∈ Subgroup.normalClosure R

Relator equivalence to one on the right is membership in the relator normal closure.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.relatorEquivalent_one_left

@[simp] theorem relatorEquivalent_one_left {R : Set G} {u : G} :
    RelatorEquivalent R 1 u ↔ u ∈ Subgroup.normalClosure R

Relator equivalence from one on the left is membership in the relator normal closure.

Show Lean proof

Definition ReidemeisterSchreier.Discrete.Presentations.relatorEquivalentSetoid

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 hvw

Relator equivalence defines a setoid on the free group.

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.refl

@[refl]
theorem refl (R : Set G) (u : G) : RelatorEquivalent R u u

Relator equivalence is reflexive.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.of_eq

theorem of_eq (h : u = v) : RelatorEquivalent R u v

Equal relators are relator-equivalent.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.symm

theorem symm (h : RelatorEquivalent R u v) : RelatorEquivalent R v u

Relator equivalence is symmetric.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.trans

theorem trans (h₁ : RelatorEquivalent R u v) (h₂ : RelatorEquivalent R v w) : RelatorEquivalent
    R u w

Relator equivalence is transitive.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.inv

theorem inv (h : RelatorEquivalent R u v) : RelatorEquivalent R u⁻¹ v⁻¹

Taking inverses preserves relator equivalence.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.mul

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 Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.pow

theorem pow (h : RelatorEquivalent R u v) (n : ℕ) : RelatorEquivalent R (u ^ n) (v ^ n)

Taking natural powers preserves relator equivalence.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.zpow

theorem zpow (h : RelatorEquivalent R u v) (n : ℤ) : RelatorEquivalent R (u ^ n) (v ^ n)

Taking integer powers preserves relator equivalence.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.mul_eq_one

theorem mul_eq_one (h₁ : RelatorEquivalent R u 1) (h₂ : RelatorEquivalent R v 1) :
    RelatorEquivalent R (u * v) 1

A product of words relator-equivalent to one is relator-equivalent to one.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.pow_eq_one

theorem pow_eq_one (h : RelatorEquivalent R u 1) (n : ℕ) :
    RelatorEquivalent R (u ^ n) 1

A natural-number power is relator-equivalent to the identity when the base word is relator-equivalent to the identity.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.zpow_eq_one

theorem zpow_eq_one (h : RelatorEquivalent R u 1) (n : ℤ) :
    RelatorEquivalent R (u ^ n) 1

An integer power is relator-equivalent to the identity when the base word is relator-equivalent to the identity.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.inv_eq_one

theorem inv_eq_one (h : RelatorEquivalent R u 1) :
    RelatorEquivalent R u⁻¹ 1

The inverse of a word is relator-equivalent to one exactly when the word is.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.conjugate_pow_eq

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 Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.mul_eq_one_iff_eq_inv

theorem mul_eq_one_iff_eq_inv :
    RelatorEquivalent R (u * v) 1 ↔ RelatorEquivalent R u v⁻¹

A product is trivial modulo the relators exactly when its first factor equals the inverse of the second.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.eq_inv_of_mul_eq_one

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 Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.mul_eq_one_of_eq_inv

theorem mul_eq_one_of_eq_inv (h : RelatorEquivalent R u v⁻¹) :
    RelatorEquivalent R (u * v) 1

A product is relator-equivalent to the identity when one factor is relator-equivalent to the inverse of the other.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.eq_one_of_mul_eq_one_left

theorem eq_one_of_mul_eq_one_left
    (hu : RelatorEquivalent R u 1)
    (huv : RelatorEquivalent R (u * v) 1) :
    RelatorEquivalent R v 1

If a left product is relator-equivalent to one and the left factor is trivial, the right factor is relator-equivalent to one.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.eq_one_of_mul_eq_one_right

theorem eq_one_of_mul_eq_one_right
    (huv : RelatorEquivalent R (u * v) 1)
    (hv : RelatorEquivalent R v 1) :
    RelatorEquivalent R u 1

If a right product is relator-equivalent to one and the right factor is trivial, the left factor is relator-equivalent to one.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.mul_left

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 Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.mul_right

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 Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.context

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 Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.conj

theorem conj (h : RelatorEquivalent R u v) (a : G) :
    RelatorEquivalent R (a * u * a⁻¹) (a * v * a⁻¹)

Conjugating both sides preserves relator equivalence.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.conj_eq_one

theorem conj_eq_one (h : RelatorEquivalent R u 1) (a : G) :
    RelatorEquivalent R (a * u * a⁻¹) 1

If a word is relator-equivalent to the identity, then every conjugate of it is also relator-equivalent to the identity.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.conj_pow_eq_one

theorem conj_pow_eq_one
    {n : ℕ} (h : RelatorEquivalent R (u ^ n) 1) (a : G) :
    RelatorEquivalent R ((a * u * a⁻¹) ^ n) 1

If a power is relator-equivalent to the identity, then every conjugate of that power is also relator-equivalent to the identity.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.of_mem

theorem of_mem (hr : r ∈ R) : RelatorEquivalent R r 1

Every defining relator is equivalent to the identity.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.of_mem_normalClosure

theorem of_mem_normalClosure (hr : r ∈ Subgroup.normalClosure R) :
    RelatorEquivalent R r 1

Membership in the normal closure gives relator equivalence to the identity.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.mono

theorem mono (hR_to_S : R ⊆ S) (h : RelatorEquivalent R u v) :
    RelatorEquivalent S u v

Relator equivalence is monotone with respect to enlarging the relator family.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.mono_iUnion

theorem mono_iUnion {ι : Sort*} (R : ι → Set G)
    (i : ι) (h : RelatorEquivalent (R i) u v) :
    RelatorEquivalent (Set.iUnion R) u v

Relator equivalence is monotone under an indexed union of relator families.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.mono_iUnion₂

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

Relator equivalence is monotone under a doubly indexed union of relator families.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.mem_normalClosure_of_eq_one

theorem mem_normalClosure_of_eq_one (h : RelatorEquivalent R r 1) :
    r ∈ Subgroup.normalClosure R

A relator-equivalence certificate to the identity gives membership in the normal closure.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.mul_inv_mem_normalClosure

theorem mul_inv_mem_normalClosure (h : RelatorEquivalent R u v) :
    u * v⁻¹ ∈ Subgroup.normalClosure R

If two words are relator-equivalent, then multiplying one by the inverse of the other gives an element of the relator normal closure.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.div_mem_normalClosure

theorem div_mem_normalClosure (h : RelatorEquivalent R u v) :
    u / v ∈ Subgroup.normalClosure R

If two words are relator-equivalent, then their quotient lies in the normal closure of the relators.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.mul_inv_eq_one

theorem mul_inv_eq_one (h : RelatorEquivalent R u v) :
    RelatorEquivalent R (u * v⁻¹) 1

Multiplying a word by the inverse of a relator-equivalent word gives a word relator-equivalent to one.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.div_eq_one

theorem div_eq_one (h : RelatorEquivalent R u v) :
    RelatorEquivalent R (u / v) 1

A quotient word is relator-equivalent to the identity when its numerator and denominator are relator-equivalent to each other.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.RelatorEquivalent.one_eq_of_mem_inv

theorem one_eq_of_mem_inv (hr : r ∈ R) : RelatorEquivalent R 1 r

The identity is equivalent to every defining relator.

Show Lean proof

ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Basic

Declarations