Mathlib.Algebra.Group.Commute.Defs

Module docstring

{"# Commuting pairs of elements in monoids

We define the predicate Commute a b := a * b = b * a and provide some operations on terms (h : Commute a b). E.g., if a, b, and c are elements of a semiring, and that hb : Commute a b and hc : Commute a c. Then hb.pow_left 5 proves Commute (a ^ 5) b and (hb.pow_right 2).add_right (hb.mul_right hc) proves Commute a (b ^ 2 + b * c).

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

This file defines only a few operations (mul_left, inv_right, etc). Other operations (pow_right, field inverse etc) are in the files that define corresponding notions.

Implementation details

Most of the proofs come from the properties of SemiconjBy. "}

Commute definition

[Mul S] (a b : S) : Prop

Full source

/-- Two elements commute if `a * b = b * a`. -/
@[to_additive "Two elements additively commute if `a + b = b + a`"]
def Commute [Mul S] (a b : S) : Prop :=
  SemiconjBy a b b

Commuting elements in a multiplicative structure

Informal description

Two elements $ a $ and $ b $ in a multiplicative structure $ S $ are said to *commute* if $ a * b = b * a $.

commute_iff_eq theorem

[Mul S] (a b : S) : Commute a b ↔ a * b = b * a

Full source

/--
Two elements `a` and `b` commute if `a * b = b * a`.
-/
@[to_additive]
theorem commute_iff_eq [Mul S] (a b : S) : CommuteCommute a b ↔ a * b = b * a := Iff.rfl

Characterization of Commuting Elements: $a * b = b * a$ if and only if $a$ and $b$ commute

Informal description

For any elements $a$ and $b$ in a multiplicative structure $S$, the elements commute if and only if $a * b = b * a$.

Commute.eq theorem

{a b : S} (h : Commute a b) : a * b = b * a

Full source

/-- Equality behind `Commute a b`; useful for rewriting. -/
@[to_additive "Equality behind `AddCommute a b`; useful for rewriting."]
protected theorem eq {a b : S} (h : Commute a b) : a * b = b * a :=
  h

Equality of Commuting Elements: $ a * b = b * a $

Informal description

For any elements $ a $ and $ b $ in a multiplicative structure $ S $, if $ a $ and $ b $ commute (i.e., $ \text{Commute}\,a\,b $ holds), then $ a * b = b * a $.

Commute.refl theorem

(a : S) : Commute a a

Full source

/-- Any element commutes with itself. -/
@[to_additive (attr := refl, simp) "Any element commutes with itself."]
protected theorem refl (a : S) : Commute a a :=
  Eq.refl (a * a)

Reflexivity of Commutation in Multiplicative Structures

Informal description

For any element $a$ in a multiplicative structure $S$, the element commutes with itself, i.e., $a * a = a * a$.

Commute.symm theorem

{a b : S} (h : Commute a b) : Commute b a

Full source

/-- If `a` commutes with `b`, then `b` commutes with `a`. -/
@[to_additive (attr := symm) "If `a` commutes with `b`, then `b` commutes with `a`."]
protected theorem symm {a b : S} (h : Commute a b) : Commute b a :=
  Eq.symm h

Symmetry of Commuting Elements

Informal description

For any elements $a$ and $b$ in a multiplicative structure $S$, if $a$ commutes with $b$ (i.e., $a * b = b * a$), then $b$ commutes with $a$ (i.e., $b * a = a * b$).

Commute.semiconjBy theorem

{a b : S} (h : Commute a b) : SemiconjBy a b b

Full source

@[to_additive]
protected theorem semiconjBy {a b : S} (h : Commute a b) : SemiconjBy a b b :=
  h

Semiconjugation Property of Commuting Elements

Informal description

For any elements $ a $ and $ b $ in a multiplicative structure $ S $, if $ a $ and $ b $ commute (i.e., $ a * b = b * a $), then $ a $ semiconjugates $ b $ to itself (i.e., $ a * b = b * a $ implies $ a * b * a^{-1} = b $, when inverses exist).

Commute.symm_iff theorem

{a b : S} : Commute a b ↔ Commute b a

Full source

@[to_additive]
protected theorem symm_iff {a b : S} : CommuteCommute a b ↔ Commute b a :=
  ⟨Commute.symm, Commute.symm⟩

Symmetry of Commutation Relation: $a * b = b * a \leftrightarrow b * a = a * b$

Informal description

For any elements $a$ and $b$ in a multiplicative structure $S$, $a$ commutes with $b$ if and only if $b$ commutes with $a$. In other words, the commutation relation is symmetric: $a * b = b * a \leftrightarrow b * a = a * b$.

Commute.instIsRefl instance

: IsRefl S Commute

Full source

@[to_additive]
instance : IsRefl S Commute :=
  ⟨Commute.refl⟩

Reflexivity of Commutation Relation

Informal description

The relation `Commute` on a multiplicative structure $S$ is reflexive, meaning every element commutes with itself.

Commute.on_isRefl instance

{f : G → S} : IsRefl G fun a b => Commute (f a) (f b)

Full source

@[to_additive]
instance on_isRefl {f : G → S} : IsRefl G fun a b => Commute (f a) (f b) :=
  ⟨fun _ => Commute.refl _⟩

Reflexivity of Commutation Relation Induced by a Function

Informal description

For any function $f : G \to S$ from a type $G$ to a multiplicative structure $S$, the relation defined by $a \sim b$ if $f(a)$ commutes with $f(b)$ is reflexive. That is, for every $a \in G$, $f(a)$ commutes with itself.

Commute.mul_right theorem

(hab : Commute a b) (hac : Commute a c) : Commute a (b * c)

Full source

/-- If `a` commutes with both `b` and `c`, then it commutes with their product. -/
@[to_additive (attr := simp)
"If `a` commutes with both `b` and `c`, then it commutes with their sum."]
theorem mul_right (hab : Commute a b) (hac : Commute a c) : Commute a (b * c) :=
  SemiconjBy.mul_right hab hac

Commutation with Product of Commuting Elements

Informal description

If an element $a$ commutes with both $b$ and $c$ in a multiplicative structure (i.e., $a * b = b * a$ and $a * c = c * a$), then $a$ also commutes with their product $b * c$ (i.e., $a * (b * c) = (b * c) * a$).

Commute.mul_left theorem

(hac : Commute a c) (hbc : Commute b c) : Commute (a * b) c

Full source

/-- If both `a` and `b` commute with `c`, then their product commutes with `c`. -/
@[to_additive (attr := simp)
"If both `a` and `b` commute with `c`, then their product commutes with `c`."]
theorem mul_left (hac : Commute a c) (hbc : Commute b c) : Commute (a * b) c :=
  SemiconjBy.mul_left hac hbc

Product of Commuting Elements Commutes with Third Element

Informal description

Let $a$, $b$, and $c$ be elements of a multiplicative structure $S$. If $a$ commutes with $c$ and $b$ commutes with $c$, then their product $a * b$ also commutes with $c$, i.e., $(a * b) * c = c * (a * b)$.

Commute.right_comm theorem

(h : Commute b c) (a : S) : a * b * c = a * c * b

Full source

@[to_additive]
protected theorem right_comm (h : Commute b c) (a : S) : a * b * c = a * c * b := by
  simp only [mul_assoc, h.eq]

Right Commutation Identity for Commuting Elements

Informal description

Let $b$ and $c$ be commuting elements in a multiplicative structure $S$ (i.e., $b * c = c * b$). Then for any element $a \in S$, the following equality holds: $$a * b * c = a * c * b.$$

Commute.left_comm theorem

(h : Commute a b) (c) : a * (b * c) = b * (a * c)

Full source

@[to_additive]
protected theorem left_comm (h : Commute a b) (c) : a * (b * c) = b * (a * c) := by
  simp only [← mul_assoc, h.eq]

Left Commutation Identity for Commuting Elements

Informal description

Let $a$ and $b$ be commuting elements in a multiplicative structure $S$ (i.e., $a * b = b * a$). Then for any element $c \in S$, the following equality holds: $$a * (b * c) = b * (a * c).$$

Commute.mul_mul_mul_comm theorem

(hbc : Commute b c) (a d : S) : a * b * (c * d) = a * c * (b * d)

Full source

@[to_additive]
protected theorem mul_mul_mul_comm (hbc : Commute b c) (a d : S) :
    a * b * (c * d) = a * c * (b * d) := by simp only [hbc.left_comm, mul_assoc]

Generalized Commutation Identity for Products with Commuting Elements

Informal description

Let $b$ and $c$ be commuting elements in a multiplicative structure $S$ (i.e., $b * c = c * b$). Then for any elements $a, d \in S$, the following equality holds: $$a * b * (c * d) = a * c * (b * d).$$

Commute.all theorem

[CommMagma S] (a b : S) : Commute a b

Full source

@[to_additive]
protected theorem all [CommMagma S] (a b : S) : Commute a b :=
  mul_comm a b

All Elements Commute in a Commutative Magma

Informal description

In a commutative magma $S$, any two elements $a$ and $b$ commute, i.e., $a * b = b * a$.

Commute.one_right theorem

(a : M) : Commute a 1

Full source

@[to_additive (attr := simp)]
theorem one_right (a : M) : Commute a 1 :=
  SemiconjBy.one_right a

Right Commutation with Identity in a Monoid

Informal description

For any element $a$ in a monoid $M$, the element $a$ commutes with the multiplicative identity $1$, i.e., $a * 1 = 1 * a$.

Commute.one_left theorem

(a : M) : Commute 1 a

Full source

@[to_additive (attr := simp)]
theorem one_left (a : M) : Commute 1 a :=
  SemiconjBy.one_left a

Left Commutation with Identity in a Monoid

Informal description

For any element $a$ in a monoid $M$, the multiplicative identity $1$ commutes with $a$, i.e., $1 * a = a * 1$.

Commute.pow_right theorem

(h : Commute a b) (n : ℕ) : Commute a (b ^ n)

Full source

@[to_additive (attr := simp)]
theorem pow_right (h : Commute a b) (n : ℕ) : Commute a (b ^ n) :=
  SemiconjBy.pow_right h n

Commutation with Powers: $a * b^n = b^n * a$ when $a$ and $b$ commute

Informal description

If two elements $a$ and $b$ in a multiplicative structure commute (i.e., $a * b = b * a$), then for any natural number $n$, the element $a$ commutes with $b^n$ (i.e., $a * b^n = b^n * a$).

Commute.pow_left theorem

(h : Commute a b) (n : ℕ) : Commute (a ^ n) b

Full source

@[to_additive (attr := simp)]
theorem pow_left (h : Commute a b) (n : ℕ) : Commute (a ^ n) b :=
  (h.symm.pow_right n).symm

Commutation of Powers: $a^n * b = b * a^n$ when $a$ and $b$ commute

Informal description

If two elements $a$ and $b$ in a multiplicative structure commute (i.e., $a * b = b * a$), then for any natural number $n$, the element $a^n$ commutes with $b$ (i.e., $a^n * b = b * a^n$).

Commute.pow_pow theorem

(h : Commute a b) (m n : ℕ) : Commute (a ^ m) (b ^ n)

Full source

@[to_additive (attr := simp)]
theorem pow_pow (h : Commute a b) (m n : ℕ) : Commute (a ^ m) (b ^ n) :=
  (h.pow_left m).pow_right n

Commutation of Powers: $a^m * b^n = b^n * a^m$ when $a$ and $b$ commute

Informal description

If two elements $a$ and $b$ in a multiplicative structure commute (i.e., $a * b = b * a$), then for any natural numbers $m$ and $n$, the elements $a^m$ and $b^n$ commute (i.e., $a^m * b^n = b^n * a^m$).

Commute.self_pow theorem

(a : M) (n : ℕ) : Commute a (a ^ n)

Full source

@[to_additive]
theorem self_pow (a : M) (n : ℕ) : Commute a (a ^ n) :=
  (Commute.refl a).pow_right n

Commutation of an Element with Its Own Power: $a * a^n = a^n * a$

Informal description

For any element $a$ in a multiplicative structure $M$ and any natural number $n$, the element $a$ commutes with its $n$-th power, i.e., $a * a^n = a^n * a$.

Commute.pow_self theorem

(a : M) (n : ℕ) : Commute (a ^ n) a

Full source

@[to_additive]
theorem pow_self (a : M) (n : ℕ) : Commute (a ^ n) a :=
  (Commute.refl a).pow_left n

Commutation of Power with Base: $a^n * a = a * a^n$

Informal description

For any element $a$ in a multiplicative structure $M$ and any natural number $n$, the $n$-th power of $a$ commutes with $a$ itself, i.e., $a^n * a = a * a^n$.

Commute.pow_pow_self theorem

(a : M) (m n : ℕ) : Commute (a ^ m) (a ^ n)

Full source

@[to_additive]
theorem pow_pow_self (a : M) (m n : ℕ) : Commute (a ^ m) (a ^ n) :=
  (Commute.refl a).pow_pow m n

Commutation of Powers of the Same Element: $a^m * a^n = a^n * a^m$

Informal description

For any element $a$ in a multiplicative structure $M$ and any natural numbers $m$ and $n$, the $m$-th power of $a$ commutes with the $n$-th power of $a$, i.e., $a^m * a^n = a^n * a^m$.

Commute.mul_pow theorem

(h : Commute a b) : ∀ n, (a * b) ^ n = a ^ n * b ^ n

Full source

@[to_additive] lemma mul_pow (h : Commute a b) : ∀ n, (a * b) ^ n = a ^ n * b ^ n
  | 0 => by rw [pow_zero, pow_zero, pow_zero, one_mul]
  | n + 1 => by simp only [pow_succ', h.mul_pow n, ← mul_assoc, (h.pow_left n).right_comm]

Power of Product of Commuting Elements: $(ab)^n = a^n b^n$

Informal description

For any elements $a$ and $b$ in a multiplicative structure that commute (i.e., $a * b = b * a$), and for any natural number $n$, the $n$-th power of their product equals the product of their $n$-th powers, i.e., $(a * b)^n = a^n * b^n$.

Commute.mul_inv theorem

(hab : Commute a b) : (a * b)⁻¹ = a⁻¹ * b⁻¹

Full source

@[to_additive]
protected theorem mul_inv (hab : Commute a b) : (a * b)⁻¹ = a⁻¹ * b⁻¹ := by rw [hab.eq, mul_inv_rev]

Inverse of Product of Commuting Elements: $(a * b)^{-1} = a^{-1} * b^{-1}$

Informal description

For any elements $a$ and $b$ in a multiplicative structure with inverses, if $a$ and $b$ commute (i.e., $a * b = b * a$), then the inverse of their product equals the product of their inverses, i.e., $(a * b)^{-1} = a^{-1} * b^{-1}$.

Commute.inv theorem

(hab : Commute a b) : (a * b)⁻¹ = a⁻¹ * b⁻¹

Full source

@[to_additive]
protected theorem inv (hab : Commute a b) : (a * b)⁻¹ = a⁻¹ * b⁻¹ := by rw [hab.eq, mul_inv_rev]

Inverse of Product of Commuting Elements: $(a * b)^{-1} = a^{-1} * b^{-1}$

Informal description

For any elements $a$ and $b$ in a multiplicative structure $S$ with inverses, if $a$ and $b$ commute (i.e., $a * b = b * a$), then the inverse of their product equals the product of their inverses, i.e., $(a * b)^{-1} = a^{-1} * b^{-1}$.

Commute.mul_zpow theorem

(h : Commute a b) : ∀ n : ℤ, (a * b) ^ n = a ^ n * b ^ n

Full source

@[to_additive AddCommute.zsmul_add]
protected lemma mul_zpow (h : Commute a b) : ∀ n : ℤ, (a * b) ^ n = a ^ n * b ^ n
  | (n : ℕ)    => by simp [zpow_natCast, h.mul_pow n]
  | .negSucc n => by simp [h.mul_pow, (h.pow_pow _ _).eq, mul_inv_rev]

Integer Power of Product of Commuting Elements: $(ab)^n = a^n b^n$

Informal description

For any elements $a$ and $b$ in a multiplicative structure that commute (i.e., $a * b = b * a$), and for any integer $n$, the $n$-th power of their product equals the product of their $n$-th powers, i.e., $(a * b)^n = a^n * b^n$.

Commute.mul_inv_cancel theorem

(h : Commute a b) : a * b * a⁻¹ = b

Full source

@[to_additive]
protected theorem mul_inv_cancel (h : Commute a b) : a * b * a⁻¹ = b := by
  rw [h.eq, mul_inv_cancel_right]

Conjugation by Commuting Element: $a * b * a^{-1} = b$

Informal description

For any elements $a$ and $b$ in a multiplicative structure with inverses, if $a$ and $b$ commute (i.e., $a * b = b * a$), then $a * b * a^{-1} = b$.

Commute.mul_inv_cancel_assoc theorem

(h : Commute a b) : a * (b * a⁻¹) = b

Full source

@[to_additive]
theorem mul_inv_cancel_assoc (h : Commute a b) : a * (b * a⁻¹) = b := by
  rw [← mul_assoc, h.mul_inv_cancel]

Associative conjugation identity for commuting elements: $a * (b * a^{-1}) = b$

Informal description

For any elements $a$ and $b$ in a multiplicative structure with inverses, if $a$ and $b$ commute (i.e., $a * b = b * a$), then $a * (b * a^{-1}) = b$.