Mathlib.Algebra.Group.Semiconj.Defs

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 definition

[Mul M] (a x y : M) : Prop

Full source

/-- `x` is semiconjugate to `y` by `a`, if `a * x = y * a`. -/
@[to_additive "`x` is additive semiconjugate to `y` by `a` if `a + x = y + a`"]
def SemiconjBy [Mul M] (a x y : M) : Prop :=
  a * x = y * a

Semiconjugate elements in a semigroup

Informal description

Given a semigroup $M$ with multiplication operation $*$, we say that an element $x$ is semiconjugate to an element $y$ by an element $a$ (written as $\text{SemiconjBy}\ a\ x\ y$) if the equation $a * x = y * a$ holds in $M$.

SemiconjBy.eq theorem

[Mul S] {a x y : S} (h : SemiconjBy a x y) : a * x = y * a

Full source

/-- Equality behind `SemiconjBy a x y`; useful for rewriting. -/
@[to_additive "Equality behind `AddSemiconjBy a x y`; useful for rewriting."]
protected theorem eq [Mul S] {a x y : S} (h : SemiconjBy a x y) : a * x = y * a :=
  h

Semiconjugate Elements Satisfy $a * x = y * a$

Informal description

Let $S$ be a semigroup with multiplication operation $*$. If $x$ is semiconjugate to $y$ by $a$ (i.e., $\text{SemiconjBy}\ a\ x\ y$ holds), then $a * x = y * a$.

SemiconjBy.mul_right theorem

(h : SemiconjBy a x y) (h' : SemiconjBy a x' y') : SemiconjBy a (x * x') (y * y')

Full source

/-- If `a` semiconjugates `x` to `y` and `x'` to `y'`,
then it semiconjugates `x * x'` to `y * y'`. -/
@[to_additive (attr := simp) "If `a` semiconjugates `x` to `y` and `x'` to `y'`,
then it semiconjugates `x + x'` to `y + y'`."]
theorem mul_right (h : SemiconjBy a x y) (h' : SemiconjBy a x' y') :
    SemiconjBy a (x * x') (y * y') := by
  unfold SemiconjBy
  -- TODO this could be done using `assoc_rw` if/when this is ported to mathlib4
  rw [← mul_assoc, h.eq, mul_assoc, h'.eq, ← mul_assoc]

Multiplication of Semiconjugate Pairs in a Semigroup

Informal description

Let $M$ be a semigroup with multiplication operation $*$. If an element $a \in M$ semiconjugates $x$ to $y$ (i.e., $a * x = y * a$) and $x'$ to $y'$ (i.e., $a * x' = y' * a$), then $a$ semiconjugates $x * x'$ to $y * y'$ (i.e., $a * (x * x') = (y * y') * a$).

SemiconjBy.mul_left theorem

(ha : SemiconjBy a y z) (hb : SemiconjBy b x y) : SemiconjBy (a * b) x z

Full source

/-- If `b` semiconjugates `x` to `y` and `a` semiconjugates `y` to `z`, then `a * b`
semiconjugates `x` to `z`. -/
@[to_additive "If `b` semiconjugates `x` to `y` and `a` semiconjugates `y` to `z`, then `a + b`
semiconjugates `x` to `z`."]
theorem mul_left (ha : SemiconjBy a y z) (hb : SemiconjBy b x y) : SemiconjBy (a * b) x z := by
  unfold SemiconjBy
  rw [mul_assoc, hb.eq, ← mul_assoc, ha.eq, mul_assoc]

Composition of Semiconjugate Relations: $(a * b) * x = z * (a * b)$

Informal description

Let $M$ be a semigroup with multiplication operation $*$. If an element $a \in M$ semiconjugates $y$ to $z$ (i.e., $a * y = z * a$) and an element $b \in M$ semiconjugates $x$ to $y$ (i.e., $b * x = y * b$), then the product $a * b$ semiconjugates $x$ to $z$ (i.e., $(a * b) * x = z * (a * b)$).

SemiconjBy.transitive theorem

: Transitive fun a b : S ↦ ∃ c, SemiconjBy c a b

Full source

/-- The relation “there exists an element that semiconjugates `a` to `b`” on a semigroup
is transitive. -/
@[to_additive "The relation “there exists an element that semiconjugates `a` to `b`” on an additive
semigroup is transitive."]
protected theorem transitive : Transitive fun a b : S ↦ ∃ c, SemiconjBy c a b
  | _, _, _, ⟨x, hx⟩, ⟨y, hy⟩ => ⟨y * x, hy.mul_left hx⟩

Transitivity of the Semiconjugacy Relation in a Semigroup

Informal description

The relation "there exists an element that semiconjugates $a$ to $b$" on a semigroup $S$ is transitive. That is, for any elements $a, b, c \in S$, if there exists an element $x$ such that $x$ semiconjugates $a$ to $b$ (i.e., $x * a = b * x$) and there exists an element $y$ such that $y$ semiconjugates $b$ to $c$ (i.e., $y * b = c * y$), then there exists an element $z$ such that $z$ semiconjugates $a$ to $c$ (i.e., $z * a = c * z$).

SemiconjBy.one_right theorem

(a : M) : SemiconjBy a 1 1

Full source

/-- Any element semiconjugates `1` to `1`. -/
@[to_additive (attr := simp) "Any element semiconjugates `0` to `0`."]
theorem one_right (a : M) : SemiconjBy a 1 1 := by rw [SemiconjBy, mul_one, one_mul]

Identity elements are semiconjugate under any element

Informal description

For any element $a$ in a multiplicative monoid $M$ with identity element $1$, the element $a$ semiconjugates $1$ to $1$, i.e., the equation $a \cdot 1 = 1 \cdot a$ holds.

SemiconjBy.one_left theorem

(x : M) : SemiconjBy 1 x x

Full source

/-- One semiconjugates any element to itself. -/
@[to_additive (attr := simp) "Zero semiconjugates any element to itself."]
theorem one_left (x : M) : SemiconjBy 1 x x :=
  Eq.symm <| one_right x

Identity Semiconjugates Any Element to Itself

Informal description

For any element $x$ in a multiplicative monoid $M$ with identity element $1$, the identity element $1$ semiconjugates $x$ to itself, i.e., the equation $1 \cdot x = x \cdot 1$ holds.

SemiconjBy.reflexive theorem

: Reflexive fun a b : M ↦ ∃ c, SemiconjBy c a b

Full source

/-- The relation “there exists an element that semiconjugates `a` to `b`” on a monoid (or, more
generally, on `MulOneClass` type) is reflexive. -/
@[to_additive "The relation “there exists an element that semiconjugates `a` to `b`” on an additive
monoid (or, more generally, on an `AddZeroClass` type) is reflexive."]
protected theorem reflexive : Reflexive fun a b : M ↦ ∃ c, SemiconjBy c a b
  | a => ⟨1, one_left a⟩

Reflexivity of the Semiconjugacy Relation in a Monoid

Informal description

The relation "there exists an element that semiconjugates $a$ to $b$" is reflexive on any monoid $M$. That is, for every element $a \in M$, there exists some element $c \in M$ such that $c$ semiconjugates $a$ to itself (i.e., $c * a = a * c$).

SemiconjBy.pow_right theorem

{a x y : M} (h : SemiconjBy a x y) (n : ℕ) : SemiconjBy a (x ^ n) (y ^ n)

Full source

@[to_additive (attr := simp)]
theorem pow_right {a x y : M} (h : SemiconjBy a x y) (n : ℕ) : SemiconjBy a (x ^ n) (y ^ n) := by
  induction n with
  | zero =>
    rw [pow_zero, pow_zero]
    exact SemiconjBy.one_right _
  | succ n ih =>
    rw [pow_succ, pow_succ]
    exact ih.mul_right h

Powers of Semiconjugate Elements in a Monoid: $a \cdot x^n = y^n \cdot a$

Informal description

Let $M$ be a monoid, and let $a, x, y \in M$ such that $x$ is semiconjugate to $y$ by $a$ (i.e., $a \cdot x = y \cdot a$). Then for any natural number $n$, the $n$-th power of $x$ is semiconjugate to the $n$-th power of $y$ by $a$, i.e., $a \cdot x^n = y^n \cdot a$.

SemiconjBy.conj_mk theorem

(a x : G) : SemiconjBy a x (a * x * a⁻¹)

Full source

/-- `a` semiconjugates `x` to `a * x * a⁻¹`. -/
@[to_additive "`a` semiconjugates `x` to `a + x + -a`."]
theorem conj_mk (a x : G) : SemiconjBy a x (a * x * a⁻¹) := by
  unfold SemiconjBy; rw [mul_assoc, inv_mul_cancel, mul_one]

Conjugation Semiconjugacy: $x$ is semiconjugate to $a x a^{-1}$ by $a$

Informal description

For any elements $a$ and $x$ in a group $G$, the element $x$ is semiconjugate to $a * x * a^{-1}$ by $a$, i.e., the relation $a * x = (a * x * a^{-1}) * a$ holds.

SemiconjBy.conj_iff theorem

{a x y b : G} : SemiconjBy (b * a * b⁻¹) (b * x * b⁻¹) (b * y * b⁻¹) ↔ SemiconjBy a x y

Full source

@[to_additive (attr := simp)]
theorem conj_iff {a x y b : G} :
    SemiconjBySemiconjBy (b * a * b⁻¹) (b * x * b⁻¹) (b * y * b⁻¹) ↔ SemiconjBy a x y := by
  unfold SemiconjBy
  simp only [← mul_assoc, inv_mul_cancel_right]
  repeat rw [mul_assoc]
  rw [mul_left_cancel_iff, ← mul_assoc, ← mul_assoc, mul_right_cancel_iff]

Conjugation Invariance of Semiconjugacy: $(bab^{-1})(bxb^{-1}) = (byb^{-1})(bab^{-1}) \leftrightarrow a x = y a$

Informal description

Let $G$ be a group and let $a, x, y, b \in G$. Then the element $b * a * b^{-1}$ semiconjugates $b * x * b^{-1}$ to $b * y * b^{-1}$ (i.e., $(b * a * b^{-1}) * (b * x * b^{-1}) = (b * y * b^{-1}) * (b * a * b^{-1})$) if and only if $a$ semiconjugates $x$ to $y$ (i.e., $a * x = y * a$).

semiconjBy_iff_eq theorem

[CancelCommMonoid M] {a x y : M} : SemiconjBy a x y ↔ x = y

Full source

@[to_additive (attr := simp)]
theorem semiconjBy_iff_eq [CancelCommMonoid M] {a x y : M} : SemiconjBySemiconjBy a x y ↔ x = y :=
  ⟨fun h => mul_left_cancel (h.trans (mul_comm _ _)), fun h => by rw [h, SemiconjBy, mul_comm]⟩

Semiconjugacy in Cancellative Commutative Monoids Implies Equality

Informal description

In a cancellative commutative monoid $M$, for any elements $a, x, y \in M$, the condition that $x$ is semiconjugate to $y$ by $a$ (i.e., $a \cdot x = y \cdot a$) holds if and only if $x = y$.