Documentation

TauCeti.Algebra.Ring.Associator

Linearity of the associator #

In a possibly nonassociative algebra A over a semiring R, the associator associator a b c = (a * b) * c - a * (b * c) is R-linear in each of its three arguments, and in a unital algebra it vanishes when one argument is 1. By linearity it vanishes on the whole span of a set as soon as it vanishes on triples of elements of that set: to check that a submodule spanned by a set s is associative, it is enough to check the triples from s.

This is how associativity of a subalgebra spanned by a few explicit elements is proved, for instance in Artin's theorem that two elements of the octonions generate an associative subalgebra.

Main results #

source
theorem TauCeti.associator_add_left {A : Type u_1} [NonUnitalNonAssocRing A] (a a' b c : A) :
associator (a + a') b c = associator a b c + associator a' b c

The associator is additive in its first argument.

source
theorem TauCeti.associator_add_middle {A : Type u_1} [NonUnitalNonAssocRing A] (a b b' c : A) :
associator a (b + b') c = associator a b c + associator a b' c

The associator is additive in its second argument.

source
theorem TauCeti.associator_add_right {A : Type u_1} [NonUnitalNonAssocRing A] (a b c c' : A) :
associator a b (c + c') = associator a b c + associator a b c'

The associator is additive in its third argument.

source
@[simp]
theorem TauCeti.associator_zero_left {A : Type u_1} [NonUnitalNonAssocRing A] (b c : A) :
associator 0 b c = 0

The associator vanishes when its first argument is 0.

source
@[simp]
theorem TauCeti.associator_zero_middle {A : Type u_1} [NonUnitalNonAssocRing A] (a c : A) :
associator a 0 c = 0

The associator vanishes when its second argument is 0.

source
@[simp]
theorem TauCeti.associator_zero_right {A : Type u_1} [NonUnitalNonAssocRing A] (a b : A) :
associator a b 0 = 0

The associator vanishes when its third argument is 0.

source
@[simp]
theorem TauCeti.associator_one_left {A : Type u_1} [NonAssocRing A] (a b : A) :
associator 1 a b = 0

The associator vanishes when its first argument is 1.

source
@[simp]
theorem TauCeti.associator_one_middle {A : Type u_1} [NonAssocRing A] (a b : A) :
associator a 1 b = 0

The associator vanishes when its second argument is 1.

source
@[simp]
theorem TauCeti.associator_one_right {A : Type u_1} [NonAssocRing A] (a b : A) :
associator a b 1 = 0

The associator vanishes when its third argument is 1.

source
theorem TauCeti.associator_smul_left {R : Type u_1} {A : Type u_2} [Monoid R] [NonUnitalNonAssocRing A] [DistribMulAction R A] [IsScalarTower R A A] (r : R) (a b c : A) :
associator (r • a) b c = r • associator a b c

The associator commutes with scalars in its first argument.

source
theorem TauCeti.associator_smul_middle {R : Type u_1} {A : Type u_2} [Monoid R] [NonUnitalNonAssocRing A] [DistribMulAction R A] [IsScalarTower R A A] [SMulCommClass R A A] (r : R) (a b c : A) :
associator a (r • b) c = r • associator a b c

The associator commutes with scalars in its second argument.

source
theorem TauCeti.associator_smul_right {R : Type u_1} {A : Type u_2} [Monoid R] [NonUnitalNonAssocRing A] [DistribMulAction R A] [SMulCommClass R A A] (r : R) (a b c : A) :
associator a b (r • c) = r • associator a b c

The associator commutes with scalars in its third argument.

source
theorem TauCeti.associator_eq_zero_of_mem_span {R : Type u_1} {A : Type u_2} [Semiring R] [NonUnitalNonAssocRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} (h : ∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, associator a b c = 0) {a b c : A} (ha : a ∈ Submodule.span R s) (hb : b ∈ Submodule.span R s) (hc : c ∈ Submodule.span R s) :
associator a b c = 0

If the associator vanishes on triples of elements of a set s, then it vanishes on triples of elements of the span of s, the associator being linear in each argument.