mathlib3 documentation

algebra.jordan.basic

Jordan rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 sym_alg.sym_mul_sym) making it into a commutative Jordan algebra (sym_alg.is_comm_jordan). Jordan algebras arising this way are said to be special.

A real Jordan algebra A can be introduced by

variables {A : Type*} [non_unital_non_assoc_ring A] [module ℝ A] [smul_comm_class ℝ A A]
  [is_scalar_tower ℝ A A] [is_comm_jordan 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]
structure is_jordan (A : Type u_1) [has_mul A] :
Type
  • 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

A (non-commutative) Jordan multiplication.

Instances of this typeclass
Instances of other typeclasses for is_jordan
  • is_jordan.has_sizeof_inst
source
@[class]
structure is_comm_jordan (A : Type u_1) [has_mul A] :
Type
  • mul_comm : ∀ (a b : A), a * b = b * a
  • lmul_comm_rmul_rmul : ∀ (a b : A), a * b * (a * a) = a * (b * (a * a))

A commutative Jordan multipication

Instances of this typeclass
Instances of other typeclasses for is_comm_jordan
  • is_comm_jordan.has_sizeof_inst
source
@[protected, instance]
def is_comm_jordan.to_is_jordan (A : Type u_1) [has_mul A] [is_comm_jordan A] :
is_jordan A

A (commutative) Jordan multiplication is also a Jordan multipication

Equations
source
@[protected, instance]
def semigroup.is_jordan (A : Type u_1) [semigroup A] :
is_jordan A

Semigroup multiplication satisfies the (non-commutative) Jordan axioms

Equations
source
@[protected, instance]
def comm_semigroup.is_comm_jordan (A : Type u_1) [comm_semigroup A] :
is_comm_jordan A
Equations

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

source
@[simp]
theorem commute_lmul_rmul {A : Type u_1} [non_unital_non_assoc_ring A] [is_jordan A] (a : A) :
commute (⇑add_monoid.End.mul_left a) (⇑add_monoid.End.mul_right a)
source
@[simp]
theorem commute_lmul_lmul_sq {A : Type u_1} [non_unital_non_assoc_ring A] [is_jordan A] (a : A) :
commute (⇑add_monoid.End.mul_left a) (⇑add_monoid.End.mul_left (a * a))
source
@[simp]
theorem commute_lmul_rmul_sq {A : Type u_1} [non_unital_non_assoc_ring A] [is_jordan A] (a : A) :
commute (⇑add_monoid.End.mul_left a) (⇑add_monoid.End.mul_right (a * a))
source
@[simp]
theorem commute_lmul_sq_rmul {A : Type u_1} [non_unital_non_assoc_ring A] [is_jordan A] (a : A) :
commute (⇑add_monoid.End.mul_left (a * a)) (⇑add_monoid.End.mul_right a)
source
@[simp]
theorem commute_rmul_rmul_sq {A : Type u_1} [non_unital_non_assoc_ring A] [is_jordan A] (a : A) :
commute (⇑add_monoid.End.mul_right a) (⇑add_monoid.End.mul_right (a * a))

The endomorphisms on an additive monoid add_monoid.End form a ring, and this may be equipped with a Lie Bracket via ring.has_bracket.

source
theorem two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add {A : Type u_1} [non_unital_non_assoc_ring A] [is_comm_jordan A] (a b : A) :
2 • (⁅⇑add_monoid.End.mul_left a, ⇑add_monoid.End.mul_left (a * b)⁆ + ⁅⇑add_monoid.End.mul_left b, ⇑add_monoid.End.mul_left (b * a)⁆) = ⁅⇑add_monoid.End.mul_left (a * a), ⇑add_monoid.End.mul_left b⁆ + ⁅⇑add_monoid.End.mul_left (b * b), ⇑add_monoid.End.mul_left a⁆
source
theorem two_nsmul_lie_lmul_lmul_add_add_eq_zero {A : Type u_1} [non_unital_non_assoc_ring A] [is_comm_jordan A] (a b c : A) :
2 • (⁅⇑add_monoid.End.mul_left a, ⇑add_monoid.End.mul_left (b * c)⁆ + ⁅⇑add_monoid.End.mul_left b, ⇑add_monoid.End.mul_left (c * a)⁆ + ⁅⇑add_monoid.End.mul_left c, ⇑add_monoid.End.mul_left (a * b)⁆) = 0