Mathlib.Algebra.Group.Semiconj.Units

Module docstring

{"# Semiconjugate elements of a semigroup

Main definitions

We say that x is semiconjugate to y by a (SemiconjBy a x y), if a * x = y * a. In this file we provide operations on SemiconjBy _ _ _.

In the names of these operations, we treat a as the “left” argument, and both x and y as “right” arguments. This way most names in this file agree with the names of the corresponding lemmas for Commute a b = SemiconjBy a b b. As a side effect, some lemmas have only _right version.

Lean does not immediately recognise these terms as equations, so for rewriting we need syntax like rw [(h.pow_right 5).eq] rather than just rw [h.pow_right 5].

This file provides only basic operations (mul_left, mul_right, inv_right etc). Other operations (pow_right, field inverse etc) are in the files that define corresponding notions. "}

SemiconjBy.units_inv_right theorem

{a : M} {x y : Mˣ} (h : SemiconjBy a x y) : SemiconjBy a ↑x⁻¹ ↑y⁻¹

Full source

/-- If `a` semiconjugates a unit `x` to a unit `y`, then it semiconjugates `x⁻¹` to `y⁻¹`. -/
@[to_additive "If `a` semiconjugates an additive unit `x` to an additive unit `y`, then it
semiconjugates `-x` to `-y`."]
theorem units_inv_right {a : M} {x y : Mˣ} (h : SemiconjBy a x y) : SemiconjBy a ↑x⁻¹ ↑y⁻¹ :=
  calc
    a * ↑x⁻¹ = ↑y⁻¹ * (y * a) * ↑x⁻¹ := by rw [Units.inv_mul_cancel_left]
    _        = ↑y⁻¹ * a              := by rw [← h.eq, mul_assoc, Units.mul_inv_cancel_right]

Inversion Preserves Semiconjugacy for Units

Informal description

Let $M$ be a monoid and let $x, y$ be invertible elements in $M$ (i.e., $x, y \in M^\times$). If $a \in M$ semiconjugates $x$ to $y$ (i.e., $a * x = y * a$), then $a$ also semiconjugates $x^{-1}$ to $y^{-1}$ (i.e., $a * x^{-1} = y^{-1} * a$).

SemiconjBy.units_inv_right_iff theorem

{a : M} {x y : Mˣ} : SemiconjBy a ↑x⁻¹ ↑y⁻¹ ↔ SemiconjBy a x y

Full source

@[to_additive (attr := simp)]
theorem units_inv_right_iff {a : M} {x y : Mˣ} : SemiconjBySemiconjBy a ↑x⁻¹ ↑y⁻¹ ↔ SemiconjBy a x y :=
  ⟨units_inv_right, units_inv_right⟩

Equivalence of Semiconjugacy for Units and Their Inverses

Informal description

Let $M$ be a monoid and let $x, y$ be invertible elements in $M$ (i.e., $x, y \in M^\times$). For any element $a \in M$, the following equivalence holds: $a$ semiconjugates $x^{-1}$ to $y^{-1}$ (i.e., $a * x^{-1} = y^{-1} * a$) if and only if $a$ semiconjugates $x$ to $y$ (i.e., $a * x = y * a$).

SemiconjBy.units_inv_symm_left theorem

{a : Mˣ} {x y : M} (h : SemiconjBy (↑a) x y) : SemiconjBy (↑a⁻¹) y x

Full source

/-- If a unit `a` semiconjugates `x` to `y`, then `a⁻¹` semiconjugates `y` to `x`. -/
@[to_additive "If an additive unit `a` semiconjugates `x` to `y`, then `-a` semiconjugates `y` to
`x`."]
theorem units_inv_symm_left {a : Mˣ} {x y : M} (h : SemiconjBy (↑a) x y) : SemiconjBy (↑a⁻¹) y x :=
  calc
    ↑a⁻¹ * y = ↑a⁻¹ * (y * a * ↑a⁻¹) := by rw [Units.mul_inv_cancel_right]
    _ = x * ↑a⁻¹ := by rw [← h.eq, ← mul_assoc, Units.inv_mul_cancel_left]

Inverse of a Unit Semiconjugates Elements in Reverse Order: $a^{-1} \cdot y = x \cdot a^{-1}$

Informal description

Let $M$ be a monoid and let $a$ be an invertible element in $M$ (i.e., $a \in M^\times$). If $x$ is semiconjugate to $y$ by $a$ (i.e., $a \cdot x = y \cdot a$), then $y$ is semiconjugate to $x$ by $a^{-1}$ (i.e., $a^{-1} \cdot y = x \cdot a^{-1}$).

SemiconjBy.units_inv_symm_left_iff theorem

{a : Mˣ} {x y : M} : SemiconjBy (↑a⁻¹) y x ↔ SemiconjBy (↑a) x y

Full source

@[to_additive (attr := simp)]
theorem units_inv_symm_left_iff {a : Mˣ} {x y : M} : SemiconjBySemiconjBy (↑a⁻¹) y x ↔ SemiconjBy (↑a) x y :=
  ⟨units_inv_symm_left, units_inv_symm_left⟩

Equivalence of Semiconjugacy Relations via Unit Inversion: $a^{-1} \cdot y = x \cdot a^{-1} \leftrightarrow a \cdot x = y \cdot a$

Informal description

Let $M$ be a monoid and let $a$ be an invertible element in $M$ (i.e., $a \in M^\times$). For any elements $x, y \in M$, the following are equivalent: 1. $y$ is semiconjugate to $x$ by $a^{-1}$ (i.e., $a^{-1} \cdot y = x \cdot a^{-1}$) 2. $x$ is semiconjugate to $y$ by $a$ (i.e., $a \cdot x = y \cdot a$)

SemiconjBy.units_val theorem

{a x y : Mˣ} (h : SemiconjBy a x y) : SemiconjBy (a : M) x y

Full source

@[to_additive]
theorem units_val {a x y : Mˣ} (h : SemiconjBy a x y) : SemiconjBy (a : M) x y :=
  congr_arg Units.val h

Semiconjugacy in Units Implies Semiconjugacy in Monoid

Informal description

Let $M$ be a monoid and let $a, x, y$ be units (invertible elements) of $M$. If $x$ is semiconjugate to $y$ by $a$ in the group of units (i.e., $a \cdot x = y \cdot a$ holds in the group of units), then $x$ is also semiconjugate to $y$ by $a$ in the underlying monoid $M$.

SemiconjBy.units_of_val theorem

{a x y : Mˣ} (h : SemiconjBy (a : M) x y) : SemiconjBy a x y

Full source

@[to_additive]
theorem units_of_val {a x y : Mˣ} (h : SemiconjBy (a : M) x y) : SemiconjBy a x y :=
  Units.ext h

Semiconjugacy in Monoid Implies Semiconjugacy in Units

Informal description

Let $M$ be a monoid and let $a, x, y$ be units (invertible elements) of $M$. If $x$ is semiconjugate to $y$ by $a$ in the underlying monoid $M$ (i.e., $a \cdot x = y \cdot a$ holds in $M$), then $x$ is also semiconjugate to $y$ by $a$ in the group of units $M^\times$.

SemiconjBy.units_val_iff theorem

{a x y : Mˣ} : SemiconjBy (a : M) x y ↔ SemiconjBy a x y

Full source

@[to_additive (attr := simp)]
theorem units_val_iff {a x y : Mˣ} : SemiconjBySemiconjBy (a : M) x y ↔ SemiconjBy a x y :=
  ⟨units_of_val, units_val⟩

Equivalence of Semiconjugacy in Monoid and Units: $a \cdot x = y \cdot a$ in $M$ iff $a \cdot x = y \cdot a$ in $M^\times$

Informal description

For any units $a, x, y$ in a monoid $M$, the element $x$ is semiconjugate to $y$ by $a$ in the underlying monoid $M$ (i.e., $a \cdot x = y \cdot a$ holds in $M$) if and only if $x$ is semiconjugate to $y$ by $a$ in the group of units $M^\times$.

SemiconjBy.units_zpow_right theorem

{a : M} {x y : Mˣ} (h : SemiconjBy a x y) : ∀ m : ℤ, SemiconjBy a ↑(x ^ m) ↑(y ^ m)

Full source

@[to_additive (attr := simp)]
lemma units_zpow_right {a : M} {x y : Mˣ} (h : SemiconjBy a x y) :
    ∀ m : ℤ, SemiconjBy a ↑(x ^ m) ↑(y ^ m)
  | (n : ℕ) => by simp only [zpow_natCast, Units.val_pow_eq_pow_val, h, pow_right]
  | -[n+1] => by simp only [zpow_negSucc, Units.val_pow_eq_pow_val, units_inv_right, h, pow_right]

Semiconjugacy of Integer Powers of Units: $a \cdot x^m = y^m \cdot a$ for all $m \in \mathbb{Z}$

Informal description

Let $M$ be a monoid and let $a \in M$. If $x, y$ are units in $M$ such that $x$ is semiconjugate to $y$ by $a$ (i.e., $a \cdot x = y \cdot a$), then for any integer $m$, the $m$-th power of $x$ is semiconjugate to the $m$-th power of $y$ by $a$, i.e., $a \cdot x^m = y^m \cdot a$.

Units.mk_semiconjBy theorem

(u : Mˣ) (x : M) : SemiconjBy (↑u) x (u * x * ↑u⁻¹)

Full source

/-- `a` semiconjugates `x` to `a * x * a⁻¹`. -/
@[to_additive "`a` semiconjugates `x` to `a + x + -a`."]
lemma mk_semiconjBy (u : Mˣ) (x : M) : SemiconjBy (↑u) x (u * x * ↑u⁻¹) := by
  unfold SemiconjBy; rw [Units.inv_mul_cancel_right]

Semiconjugation by a unit: $u \cdot x = (u \cdot x \cdot u^{-1}) \cdot u$

Informal description

For any unit $u$ in a monoid $M$ and any element $x \in M$, the element $u$ semiconjugates $x$ to $u * x * u^{-1}$, i.e., $u \cdot x = (u \cdot x \cdot u^{-1}) \cdot u$.

Units.conj_pow theorem

(u : Mˣ) (x : M) (n : ℕ) : ((↑u : M) * x * (↑u⁻¹ : M)) ^ n = (u : M) * x ^ n * (↑u⁻¹ : M)

Full source

lemma conj_pow (u : Mˣ) (x : M) (n : ℕ) :
    ((↑u : M) * x * (↑u⁻¹ : M)) ^ n = (u : M) * x ^ n * (↑u⁻¹ : M) :=
  eq_divp_iff_mul_eq.2 ((u.mk_semiconjBy x).pow_right n).eq.symm

Conjugation of Powers by a Unit: $(u x u^{-1})^n = u x^n u^{-1}$

Informal description

Let $M$ be a monoid, $u$ be a unit in $M$, and $x \in M$. Then for any natural number $n$, the $n$-th power of the conjugate of $x$ by $u$ equals the conjugate of $x^n$ by $u$, i.e., $$(u \cdot x \cdot u^{-1})^n = u \cdot x^n \cdot u^{-1}.$$

Units.conj_pow' theorem

(u : Mˣ) (x : M) (n : ℕ) : ((↑u⁻¹ : M) * x * (u : M)) ^ n = (↑u⁻¹ : M) * x ^ n * (u : M)

Full source

lemma conj_pow' (u : Mˣ) (x : M) (n : ℕ) :
    ((↑u⁻¹ : M) * x * (u : M)) ^ n = (↑u⁻¹ : M) * x ^ n * (u : M) := u⁻¹.conj_pow x n

Conjugation of Powers by Inverse Unit: $(u^{-1} x u)^n = u^{-1} x^n u$

Informal description

Let $M$ be a monoid, $u$ be a unit in $M$, and $x \in M$. Then for any natural number $n$, the $n$-th power of the conjugate of $x$ by $u^{-1}$ equals the conjugate of $x^n$ by $u^{-1}$, i.e., $$(u^{-1} \cdot x \cdot u)^n = u^{-1} \cdot x^n \cdot u.$$