Pre-Lie rings and algebras

In this file we introduce left and right pre-Lie rings, defined as a NonUnitalNonAssocRing where the associator associator x y z := (x * y) * z - x * (y * z) is left or right symmetric, respectively.

We prove that every Left(Right)PreLieRing L is a Right(Left)PreLieRing L with the opposite mul. The equivalence is simple given by op : L ≃* Lᵐᵒᵖ.

Everything holds for the algebra versions where L is also an R-Module over a commutative ring R.

Main definitions

All are a defined as a NonUnitalNonAssocRing whose associator satisfies an identity.

• LeftPreLieRing
• RightPreLieRing
• LeftPreLieAlgebra
• RightPreLieAlgebra

Main results

• Every LeftPreLieRing is a RightPreLieRing with the opposite multiplication.

Implementation notes

There are left and right versions of the structures, equivalent via ᵐᵒᵖ. Perhaps one could be favored but there is no real reason to.

References

[F. Chapoton, M. Livernet, Pre-Lie algebras and the rooted trees operad][chapoton_livernet_2001] [D. Manchon, A short survey on pre-Lie algebras][manchon_2011] [J.-M. Oudom, D. Guin, On the Lie enveloping algebra of a pre-Lie algebra][oudom_guin_2008] https://ncatlab.org/nlab/show/pre-Lie+algebra

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

LeftPreLieRings are NonUnitalNonAssocRings such that the associator is symmetric in the first two variables.

• 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_symm' (x y z : L) : associator x y z = associator y x z

theorem LeftPreLieRing.ext_iff {L : Type u_1} {x y : LeftPreLieRing 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

theorem LeftPreLieRing.ext {L : Type u_1} {x y : LeftPreLieRing 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

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

RightPreLieRings are NonUnitalNonAssocRings such that the associator is symmetric in the last two variables.

• 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_symm' (x y z : L) : associator x y z = associator x z y

theorem RightPreLieRing.ext {L : Type u_1} {x y : RightPreLieRing 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 RightPreLieRing.ext_iff {L : Type u_1} {x y : RightPreLieRing 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 LeftPreLieAlgebra (R : Type u_1) [CommRing R] (L : Type u_2) [LeftPreLieRing L] extends Module R L, IsScalarTower R L L, SMulCommClass R L L : Type (max u_1 u_2)

A LeftPreLieAlgebra is a LeftPreLieRing with an action of a CommRing satisfying r • x * y = r • (x * y) and x * (r • y) = r • (x * y).

• 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 LeftPreLieAlgebra.ext_iff {R : Type u_1} {inst✝ : CommRing R} {L : Type u_2} {inst✝¹ : LeftPreLieRing L} {x y : LeftPreLieAlgebra R L} : x = y ↔ SMul.smul = SMul.smul

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

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

A RightPreLieAlgebra is a RightPreLieRing with an action of a CommRing satisfying r • x * y = r • (x * y) and x * (r • y) = r • (x * y).

• 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 RightPreLieAlgebra.ext {R : Type u_1} {inst✝ : CommRing R} {L : Type u_2} {inst✝¹ : RightPreLieRing L} {x y : RightPreLieAlgebra R L} (smul : SMul.smul = SMul.smul) : x = y

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

theorem LeftPreLieRing.assoc_symm {L : Type u_2} [LeftPreLieRing L] (x y z : L) : associator x y z = associator y x z

@[implicit_reducible]

instance LeftPreLieRing.instRightPreLieRingMulOpposite {L : Type u_2} [LeftPreLieRing L] : RightPreLieRing Lᵐᵒᵖ

Every left pre-Lie ring is a right pre-Lie ring with the opposite multiplication

@[implicit_reducible]

instance LeftPreLieAlgebra.instRightPreLieAlgebraMulOpposite {R : Type u_1} {L : Type u_2} [CommRing R] [LeftPreLieRing L] [LeftPreLieAlgebra R L] : RightPreLieAlgebra R Lᵐᵒᵖ

Every left pre-Lie algebra is a right pre-Lie algebra with the opposite multiplication

theorem RightPreLieRing.assoc_symm {L : Type u_2} [RightPreLieRing L] (x y z : L) : associator x y z = associator x z y

@[implicit_reducible]

instance RightPreLieRing.instLeftPreLieRingMulOpposite {L : Type u_2} [RightPreLieRing L] : LeftPreLieRing Lᵐᵒᵖ

Every left pre-Lie ring is a right pre-Lie ring with the opposite multiplication

@[implicit_reducible]

instance RightPreLieAlgebra.instLeftPreLieAlgebraMulOpposite {R : Type u_1} {L : Type u_2} [CommRing R] [RightPreLieRing L] [RightPreLieAlgebra R L] : LeftPreLieAlgebra R Lᵐᵒᵖ

Every left pre-Lie algebra is a right pre-Lie algebra with the opposite multiplication