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.

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) : 0 • x = 0
• nsmul_succ (n : ℕ) (x : L) : (n + 1) • x = n • x + x
• neg : L → L
• sub : L → L → L
• zsmul : ℤ → L → L
• sub_eq_add_neg (a b : L) : a - b = a + -b
• zsmul_zero' (a : L) : 0 • a = 0
• zsmul_succ' (n : ℕ) (a : L) : ↑n.succ • a = ↑n • a + a
• zsmul_neg' (n : ℕ) (a : L) : Int.negSucc n • a = -(↑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_iff {L : Type u_1} {x y : LieAdmissibleRing L} : x = y ↔ Add.add = Add.add ∧ Zero.zero = Zero.zero ∧ NSMul.nsmul = NSMul.nsmul ∧ Neg.neg = Neg.neg ∧ Sub.sub = Sub.sub ∧ ZSMul.zsmul = ZSMul.zsmul ∧ Mul.mul = Mul.mul

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

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_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

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

@[implicit_reducible]

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

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

Equations

• LieAdmissibleRing.instLieRing = { toAddCommGroup := inst✝.toAddCommGroup, toBracket := Ring.instBracket, add_lie := ⋯, lie_add := ⋯, lie_self := ⋯, leibniz_lie := ⋯ }

@[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.

Equations

• LieAdmissibleAlgebra.instLieAlgebra = { toModule := inst✝.toModule, lie_smul := ⋯ }

@[implicit_reducible]

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

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

Equations

• LeftPreLieRing.instLieAdmissibleRing = { toNonUnitalNonAssocRing := inst✝.toNonUnitalNonAssocRing, assoc_def := ⋯ }

@[implicit_reducible]

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

Equations

• LeftPreLieAlgebra.instLieAdmissibleAlgebra = { toModule := inst✝.toModule, toIsScalarTower := ⋯, toSMulCommClass := ⋯ }

@[implicit_reducible]

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

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

Equations

• RightPreLieRing.instLieAdmissibleRing = { toNonUnitalNonAssocRing := inst✝.toNonUnitalNonAssocRing, assoc_def := ⋯ }

@[implicit_reducible]

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

Equations

• RightPreLieAlgebra.instLieAdmissibleAlgebra = { toModule := inst✝.toModule, toIsScalarTower := ⋯, toSMulCommClass := ⋯ }

@[reducible, inline]

abbrev Ring.instLieAdmissibleRing {L : Type u_2} [Ring L] : LieAdmissibleRing L

Every ring is Lie-admissible. See note [reducible non-instances].

Equations

• Ring.instLieAdmissibleRing = { toNonUnitalNonAssocRing := Ring.toNonAssocRing.toNonUnitalNonAssocRing, assoc_def := ⋯ }

@[reducible, inline]

abbrev Algebra.instLieAdmissibleAlgebra {R : Type u_1} {L : Type u_2} [CommRing R] [Ring L] [Algebra R L] : LieAdmissibleAlgebra R L

Every algebra is Lie-admissible. See note [reducible non-instances].

Equations

• Algebra.instLieAdmissibleAlgebra = { toModule := Algebra.toModule, toIsScalarTower := ⋯, toSMulCommClass := ⋯ }