Associator in a ring

If R is a non-associative ring, then (x * y) * z - x * (y * z) is called the associator of ring elements x y z : R.

The associator vanishes exactly when R is associative.

We prove variants of this statement also for the AddMonoidHom bundled version of the associator, as well as the bundled version of mulLeft₃ and mulRight₃, the multiplications (x * y) * z and x * (y * z).

def associator {R : Type u_1} [NonUnitalNonAssocRing R] (x y z : R) : R

The associator (x * y) * z - x * (y * z)

Equations

• associator x y z = x * y * z - x * (y * z)

theorem associator_apply {R : Type u_1} [NonUnitalNonAssocRing R] (x y z : R) : associator x y z = x * y * z - x * (y * z)

theorem associator_eq_zero_iff_associative {R : Type u_1} [NonUnitalNonAssocRing R] : associator = 0 ↔ Std.Associative fun (x y : R) => x * y

theorem associator_cocycle {R : Type u_1} [NonUnitalNonAssocRing R] (a b c d : R) : a * associator b c d - associator (a * b) c d + associator a (b * c) d - associator a b (c * d) + associator a b c * d = 0

@[simp]

theorem associator_eq_zero {R : Type u_1} [NonUnitalRing R] : associator = 0

def AddMonoidHom.mulLeft₃ {R : Type u_1} [NonUnitalNonAssocSemiring R] : R →+ R →+ R →+ R

The multiplication (x * y) * z of three elements of a (non-associative) (semi)-ring is an AddMonoidHom in each argument. See also LinearMap.mulLeftRight for a related functions realized as a linear map.

Equations

• AddMonoidHom.mulLeft₃ = { toFun := fun (x : R) => AddMonoidHom.mul.comp (AddMonoidHom.mulLeft x), map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AddMonoidHom.mulLeft₃_apply {R : Type u_1} [NonUnitalNonAssocSemiring R] (x y z : R) : ((mulLeft₃ x) y) z = x * y * z

def AddMonoidHom.mulRight₃ {R : Type u_1} [NonUnitalNonAssocSemiring R] : R →+ R →+ R →+ R

The multiplication x * (y * z) of three elements of a (non-associative) (semi)-ring is an AddMonoidHom in each argument.

Equations

• AddMonoidHom.mulRight₃ = { toFun := fun (x : R) => AddMonoidHom.mul.compr₂ (AddMonoidHom.mulLeft x), map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AddMonoidHom.mulRight₃_apply {R : Type u_1} [NonUnitalNonAssocSemiring R] (x y z : R) : ((mulRight₃ x) y) z = x * (y * z)

theorem AddMonoidHom.mulLeft₃_eq_mulRight₃_iff_associative {R : Type u_1} [NonUnitalNonAssocSemiring R] : mulLeft₃ = mulRight₃ ↔ Std.Associative fun (x y : R) => x * y

An a priori non-associative semiring is associative if the AddMonoidHom versions of the multiplications (x * y) * z and x * (y * z) agree.

theorem AddMonoidHom.mulLeft₃_eq_mulRight₃ {R : Type u_1} [NonUnitalSemiring R] : mulLeft₃ = mulRight₃

def AddMonoidHom.associator {R : Type u_1} [NonUnitalNonAssocRing R] : R →+ R →+ R →+ R

The associator for a non-associative ring is (x * y) * z - x * (y * z). It is an AddMonoidHom in each argument.

Equations

• AddMonoidHom.associator = AddMonoidHom.mulLeft₃ - AddMonoidHom.mulRight₃

@[simp]

theorem AddMonoidHom.associator_apply {R : Type u_1} [NonUnitalNonAssocRing R] (a b c : R) : ((associator a) b) c = _root_.associator a b c

theorem AddMonoidHom.associator_eq_zero_iff_associative {R : Type u_1} [NonUnitalNonAssocRing R] : associator = 0 ↔ Std.Associative fun (x y : R) => x * y

An a priori non-associative ring is associative iff the AddMonoidHom version of the associator vanishes.

@[simp]

theorem AddMonoidHom.associator_eq_zero {R : Type u_1} [NonUnitalRing R] : associator = 0