Documentation

TauCeti.Algebra.Ring.Commutator

Commutators in associative semirings and rings #

This file records identities for moving elements past powers when the two elements almost commute.

Over a semiring the hypothesis is written as a relation, x * y = y * x + z, since there is no subtraction to form a commutator with: the power identities need only that z commutes with the element being powered, and the nilpotency results additionally need a ℚ-algebra structure, to divide by the multiplicity a power releases. Over a ring the same z is the commutator x * y - y * x, which is the form the integer-eigenvector results take.

Main results #

source
theorem TauCeti.Associative.mul_pow_eq_pow_mul_add_nsmul_of_commutator_eq {A : Type u_1} [Semiring A] {x y z : A} (hxy : x * y = y * x + z) (hyz : Commute y z) (n : ℕ) :
x * y ^ n = y ^ n * x + n • (y ^ (n - 1) * z)

Moving an element across a power releases that many copies of the correction term. If x * y = y * x + z and z commutes with y, then x * y ^ n is y ^ n * x plus n copies of y ^ (n - 1) * z.

source
theorem TauCeti.Associative.mul_pow_eq_pow_mul_add_nsmul {A : Type u_1} [Semiring A] {a x c : A} (h : a * x = x * (a + c)) (hc : Commute c x) (n : ℕ) :
a * x ^ n = x ^ n * (a + n • c)

Moving an element across a power accumulates the additive shift, provided that shift commutes with the element being powered.

source
theorem TauCeti.Associative.pow_mul_eq_mul_pow_add_nsmul_of_commutator_eq {A : Type u_1} [Semiring A] {x y z : A} (hxy : x * y = y * x + z) (hxz : Commute x z) (n : ℕ) :
x ^ n * y = y * x ^ n + n • (x ^ (n - 1) * z)

Moving y past a power of x releases that many copies of the correction term. If x * y = y * x + z and z commutes with x, then x ^ n * y is y * x ^ n plus n copies of x ^ (n - 1) * z.

source
theorem TauCeti.Associative.pow_mul_eq_add_nsmul_mul_pow {A : Type u_1} [Semiring A] {a x c : A} (h : x * a = (a + c) * x) (hc : Commute c x) (n : ℕ) :
x ^ n * a = (a + n • c) * x ^ n

Moving an element past a power standing to its left accumulates the additive shift, provided that shift commutes with the element being powered.

source
theorem TauCeti.Associative.mul_pow_eq_pow_mul_add_intCast {A : Type u_1} [Ring A] {x y : A} {c : ℤ} (hxy : x * y - y * x = c • y) (n : ℕ) :
x * y ^ n = y ^ n * (x + ↑c * ↑n)

Moving an element past a power of an integer-eigenvector for its commutator shifts that element by the eigenvalue times the exponent.

source
theorem TauCeti.Associative.mul_pow_eq_pow_mul_add_zsmul {A : Type u_1} [Ring A] {x y : A} {c : ℤ} (hxy : x * y - y * x = c • y) (n : ℕ) :
x * y ^ n = y ^ n * x + (↑n * c) • y ^ n

If y has integer eigenvalue c for commutation with x, then moving x past yⁿ adds n * c copies of yⁿ.

source
theorem TauCeti.Associative.isNilpotent_of_commutator_eq {A : Type u_1} [Semiring A] [Algebra ℚ A] {x y z : A} (hxy : x * y = y * x + z) (hxz : Commute x z) (hyz : Commute y z) (hx : IsNilpotent x) :
IsNilpotent z

Nilpotency of a central commutator. If x * y = y * x + z with z commuting with both x and y, then z is nilpotent as soon as x is, with the same nilpotency exponent.

source
theorem TauCeti.Associative.isNilpotent_of_commutator_eq_nsmul {A : Type u_1} [Semiring A] [Algebra ℚ A] {x y z : A} {n : ℕ} (hn : n ≠ 0) (hxy : x * y = y * x + n • z) (hxz : Commute x z) (hyz : Commute y z) (hx : IsNilpotent x) :
IsNilpotent z

If x * y = y * x + n • z for a nonzero natural number n, with z commuting with x and y, then z is nilpotent whenever x is.