Lie admissible rings and algebras

We define a Lie-admissible ring as a nonunital nonassociative ring such that the associator satisfies the identity

associator x y z + associator z x y + associator y z x =
  associator y x z + associator z y x + associator x z y

Main definitions:

• LieAdmissibleRing
• LieAdmissibleAlgebra

Main results

• LieAdmissibleRing.instLieRing: a Lie-admissible ring as a Lie ring
• LeftPreLieRing.instLieAdmissibleRing: a left pre-Lie ring as a Lie admissible ring
• RightPreLieRing.instLieAdmissibleRing: a right pre-Lie ring as a Lie admissible ring
• LieAdmissibleAlgebra.instLieAlgebra: a Lie-admissible algebra as a Lie algebra
• LeftPreLieAlgebra.instLieAdmissibleAlgebra: a left pre-Lie ring as a Lie admissible algebra
• RightPreLieAlgebra.instLieAdmissibleAlgebra: a right pre-Lie ring as a Lie admissible algebra

Implementation Notes

Algebras are implemented as extending Module, IsScalarTower and SMulCommClass following the documentation of Algebra.

References

[Munthe-Kaas, H.Z., Lundervold, A. On Post-Lie Algebras, Lie–Butcher Series and Moving Frames.][munthe-kaas_lundervold_2013]

class LieAdmissibleRing (L : Type u_1) extends NonUnitalNonAssocRing L : Type u_1

A LieAdmissibleRing is a NonUnitalNonAssocRing such that the canonical bracket ⁅x, y⁆ := x * y - y * x turns it into a LieRing. This is expressed by an associator identity.

• add : L → L → L
• add_assoc (a b c : L) : a + b + c = a + (b + c)
• zero : L
• zero_add (a : L) : 0 + a = a
• add_zero (a : L) : a + 0 = a
• nsmul : ℕ → L → L
• nsmul_zero (x : L) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : L) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• neg : L → L
• sub : L → L → L
• sub_eq_add_neg (a b : L) : a - b = a + -b
• zsmul : ℤ → L → L
• zsmul_zero' (a : L) : SubNegMonoid.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : L) : SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : L) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (a : L) : -a + a = 0
• add_comm (a b : L) : a + b = b + a
• mul : L → L → L
• left_distrib (a b c : L) : a * (b + c) = a * b + a * c
• right_distrib (a b c : L) : (a + b) * c = a * c + b * c
• zero_mul (a : L) : 0 * a = 0
• mul_zero (a : L) : a * 0 = 0
• assoc_def (x y z : L) : associator x y z + associator z x y + associator y z x = associator y x z + associator z y x + associator x z y

theorem LieAdmissibleRing.ext {L : Type u_1} {x y : LieAdmissibleRing L} (add : Add.add = Add.add) (zero : Zero.zero = Zero.zero) (nsmul : AddMonoid.nsmul = AddMonoid.nsmul) (neg : Neg.neg = Neg.neg) (sub : Sub.sub = Sub.sub) (zsmul : SubNegMonoid.zsmul = SubNegMonoid.zsmul) (mul : Mul.mul = Mul.mul) : x = y

theorem LieAdmissibleRing.ext_iff {L : Type u_1} {x y : LieAdmissibleRing L} : x = y ↔ Add.add = Add.add ∧ Zero.zero = Zero.zero ∧ AddMonoid.nsmul = AddMonoid.nsmul ∧ Neg.neg = Neg.neg ∧ Sub.sub = Sub.sub ∧ SubNegMonoid.zsmul = SubNegMonoid.zsmul ∧ Mul.mul = Mul.mul

class LieAdmissibleAlgebra (R : Type u_1) (L : Type u_2) [CommRing R] [LieAdmissibleRing L] extends Module R L, IsScalarTower R L L, SMulCommClass R L L : Type (max u_1 u_2)

A LieAdmissibleAlgebra is a LieAdmissibleRing equipped with a compatible action by scalars from a commutative ring.

• smul : R → L → L
• mul_smul (x y : R) (b : L) : (x * y) • b = x • y • b
• one_smul (b : L) : 1 • b = b
• smul_zero (a : R) : a • 0 = 0
• smul_add (a : R) (x y : L) : a • (x + y) = a • x + a • y
• add_smul (r s : R) (x : L) : (r + s) • x = r • x + s • x
• zero_smul (x : L) : 0 • x = 0
• smul_assoc (x : R) (y z : L) : (x • y) • z = x • y • z
• smul_comm (m : R) (n a : L) : m • n • a = n • m • a

theorem LieAdmissibleAlgebra.ext {R : Type u_1} {L : Type u_2} {inst✝ : CommRing R} {inst✝¹ : LieAdmissibleRing L} {x y : LieAdmissibleAlgebra R L} (smul : SMul.smul = SMul.smul) : x = y

theorem LieAdmissibleAlgebra.ext_iff {R : Type u_1} {L : Type u_2} {inst✝ : CommRing R} {inst✝¹ : LieAdmissibleRing L} {x y : LieAdmissibleAlgebra R L} : x = y ↔ SMul.smul = SMul.smul

@[implicit_reducible]

instance LieAdmissibleRing.instLieRing {L : Type u_2} [LieAdmissibleRing L] : LieRing L

By definition, every LieAdmissibleRing yields a LieRing with the commutator bracket.

@[implicit_reducible]

instance LieAdmissibleAlgebra.instLieAlgebra {R : Type u_1} {L : Type u_2} [CommRing R] [LieAdmissibleRing L] [LieAdmissibleAlgebra R L] : LieAlgebra R L

Every LieAdmissibleAlgebra is a LieAlgebra with the commutator bracket.

@[implicit_reducible]

instance LeftPreLieRing.instLieAdmissibleRing {L : Type u_1} [LeftPreLieRing L] : LieAdmissibleRing L

LeftPreLieRings are examples of LieAdmissibleRings by the commutativity assumption on the associator.

@[implicit_reducible]

instance LeftPreLieAlgebra.instLieAdmissibleAlgebra {R : Type u_1} {L : Type u_2} [CommRing R] [LeftPreLieRing L] [LeftPreLieAlgebra R L] : LieAdmissibleAlgebra R L

@[implicit_reducible]

instance RightPreLieRing.instLieAdmissibleRing {L : Type u_1} [RightPreLieRing L] : LieAdmissibleRing L

RightPreLieRings are examples of LieAdmissibleRings by the commutativity assumption on the associator.

@[implicit_reducible]

instance RightPreLieAlgebra.instLieAdmissibleAlgebra {R : Type u_1} {L : Type u_2} [CommRing R] [RightPreLieRing L] [RightPreLieAlgebra R L] : LieAdmissibleAlgebra R L