Documentation

Mathlib.Algebra.Jordan.Basic

Jordan rings #

Let A be a non-unital, non-associative ring. Then A is said to be a (commutative, linear) Jordan ring if the multiplication is commutative and satisfies a weak associativity law known as the Jordan Identity: for all a and b in A,

(a * b) * a^2 = a * (b * a^2)

i.e. the operators of multiplication by a and a^2 commute.

A more general concept of a (non-commutative) Jordan ring can also be defined, as a (non-commutative, non-associative) ring A where, for each a in A, the operators of left and right multiplication by a and a^2 commute.

Every associative algebra can be equipped with a symmetrized multiplication (characterized by SymAlg.sym_mul_sym) making it into a commutative Jordan algebra (IsCommJordan). Jordan algebras arising this way are said to be special.

A real Jordan algebra A can be introduced by

variable {A : Type*} [NonUnitalNonAssocCommRing A] [Module ℝ A] [SMulCommClass ℝ A A]
  [IsScalarTower ℝ A A] [IsCommJordan A]

Main results #

Implementation notes #

We shall primarily be interested in linear Jordan algebras (i.e. over rings of characteristic not two) leaving quadratic algebras to those better versed in that theory.

The conventional way to linearise the Jordan axiom is to equate coefficients (more formally, assume that the axiom holds in all field extensions). For simplicity we use brute force algebraic expansion and substitution instead.

Motivation #

Every Jordan algebra A has a triple product defined, for a b and c in A by $$ {a\,b\,c} = (a * b) * c - (a * c) * b + a * (b * c). $$ Via this triple product Jordan algebras are related to a number of other mathematical structures: Jordan triples, partial Jordan triples, Jordan pairs and quadratic Jordan algebras. In addition to their considerable algebraic interest ([McC04]) these structures have been shown to have deep connections to mathematical physics, functional analysis and differential geometry. For more information about these connections the interested reader is referred to [AS03], [Chu12], [Fri05], [Ior03] and [Upm87].

There are also exceptional Jordan algebras which can be shown not to be the symmetrization of any associative algebra. The 3x3 matrices of octonions is the canonical example.

Non-commutative Jordan algebras have connections to the Vidav-Palmer theorem [CGRP14].

References #

source
class IsJordan (A : Type u_1) [Mul A] :
Prop

A (non-commutative) Jordan multiplication.

  • lmul_comm_rmul (a b : A) : a * b * a = a * (b * a)
  • lmul_lmul_comm_lmul (a b : A) : a * a * (a * b) = a * (a * a * b)
  • lmul_lmul_comm_rmul (a b : A) : a * a * (b * a) = a * a * b * a
  • lmul_comm_rmul_rmul (a b : A) : a * b * (a * a) = a * (b * (a * a))
  • rmul_comm_rmul_rmul (a b : A) : b * a * (a * a) = b * (a * a) * a
Instances
    source
    class IsCommJordan (A : Type u_1) [CommMagma A] :
    Prop

    A commutative Jordan multiplication

    • lmul_comm_rmul_rmul (a b : A) : a * b * (a * a) = a * (b * (a * a))
    Instances
      source
      @[instance 100]
      instance IsCommJordan.toIsJordan (A : Type u_1) [CommMagma A] [IsCommJordan A] :
      IsJordan A

      A (commutative) Jordan multiplication is also a Jordan multiplication

      source
      @[instance 100]
      instance Semigroup.isJordan (A : Type u_1) [Semigroup A] :
      IsJordan A

      Semigroup multiplication satisfies the (non-commutative) Jordan axioms

      source
      @[instance 100]
      instance CommSemigroup.isCommJordan (A : Type u_1) [CommSemigroup A] :
      IsCommJordan A

      The Jordan axioms can be expressed in terms of commuting multiplication operators.

      source
      @[simp]
      theorem commute_lmul_rmul {A : Type u_1} [NonUnitalNonAssocRing A] [IsJordan A] (a : A) :
      Commute (AddMonoid.End.mulLeft a) (AddMonoid.End.mulRight a)
      source
      @[simp]
      theorem commute_lmul_lmul_sq {A : Type u_1} [NonUnitalNonAssocRing A] [IsJordan A] (a : A) :
      Commute (AddMonoid.End.mulLeft a) (AddMonoid.End.mulLeft (a * a))
      source
      @[simp]
      theorem commute_lmul_rmul_sq {A : Type u_1} [NonUnitalNonAssocRing A] [IsJordan A] (a : A) :
      Commute (AddMonoid.End.mulLeft a) (AddMonoid.End.mulRight (a * a))
      source
      @[simp]
      theorem commute_lmul_sq_rmul {A : Type u_1} [NonUnitalNonAssocRing A] [IsJordan A] (a : A) :
      Commute (AddMonoid.End.mulLeft (a * a)) (AddMonoid.End.mulRight a)
      source
      @[simp]
      theorem commute_rmul_rmul_sq {A : Type u_1} [NonUnitalNonAssocRing A] [IsJordan A] (a : A) :
      Commute (AddMonoid.End.mulRight a) (AddMonoid.End.mulRight (a * a))

      The endomorphisms on an additive monoid AddMonoid.End form a Ring, and this may be equipped with a Lie Bracket via Ring.bracket.

      source
      theorem two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add {A : Type u_1} [NonUnitalNonAssocCommRing A] [IsCommJordan A] (a b : A) :
      2 • (⁅AddMonoid.End.mulLeft a, AddMonoid.End.mulLeft (a * b)⁆ + ⁅AddMonoid.End.mulLeft b, AddMonoid.End.mulLeft (b * a)⁆) = ⁅AddMonoid.End.mulLeft (a * a), AddMonoid.End.mulLeft b⁆ + ⁅AddMonoid.End.mulLeft (b * b), AddMonoid.End.mulLeft a⁆
      source
      theorem two_nsmul_lie_lmul_lmul_add_add_eq_zero {A : Type u_1} [NonUnitalNonAssocCommRing A] [IsCommJordan A] (a b c : A) :
      2 • (⁅AddMonoid.End.mulLeft a, AddMonoid.End.mulLeft (b * c)⁆ + ⁅AddMonoid.End.mulLeft b, AddMonoid.End.mulLeft (c * a)⁆ + ⁅AddMonoid.End.mulLeft c, AddMonoid.End.mulLeft (a * b)⁆) = 0