Jordan Algebras

Stream: mathlib4

[Mr Proof]

Is there a way to do Jordan algebras? This is what I've got so far:

import Mathlib

structure Jordan (n:Nat)(α:Type) where
  M:Matrix (Fin n) (Fin n) α

instance [Repr α] [One α] [Neg α] : Repr (Jordan n α) :=
  { reprPrec := fun q _ => s!"({repr q.M}:Jordan" }

def Jordan.mul {n:Nat} (a b: Jordan n ℚ) :Jordan n ℚ  := { M:= ((1:Rat)/2) • (a.M*b.M + b.M*a.M) }
def Jordan.add {n:Nat} (a b: Jordan n ℚ) :Jordan n ℚ  := { M:= a.M+b.M }

instance : Mul (Jordan n ℚ) where mul := Jordan.mul
instance : Add (Jordan n ℚ) where add := Jordan.add

def X:Jordan 3 ℚ := {M:=!![1,2,3;4,5,6;7,8,9]}

#eval X * X + X

One problem is I can't divide the matrices by 2. (fixed)

Also I notice that you can do:

def a:Matrix (Fin 6) (Fin 6) ℚ := -3 /- works-/
def b:Matrix (Fin 6) (Fin 6) ℚ := (2:Rat)/5 /- doesn't work-/

A second question is how do I modify this so multiplication is defined on any numerical type. e.g. Rat Nat and Int.

[Utensil Song]

You need [Invertible (2 : \alpha)]

[Kim Morrison]

If you want to follow the link you gave, you should start by defining an abstract Jordan algebra (rather than defining the special Jordan algebra associated to matrices).

[Kim Morrison]

You'd then want a SpecialJordan \a := \a type synonym, on which you would put the Jordan product, given an associative product on \a.

[Mr Proof]

Hmm... I'm more interested in the representations as matrices (for now). I think the problem is that multiplication of a matrix by a rational doesn't work in Lean. I think it's missing that functionality. You can only multiply it by an integer:

import Mathlib

def a:Matrix (Fin 6) (Fin 6) ℚ := 5

#eval a * 4 /-works-/
#eval a * ((1:Rat)/2) /-doesn't work-/

[Eric Wieser]

docs#IsJordan

[Kevin Buzzard]

Use smul not mul for multiplying matrices by scalars, and put the scalar on the left.

[Yaël Dillies]

You should be talking to @Christopher Hoskin

[Christopher Hoskin]

I made a start on Jordan Rings / Algebras here: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Algebra/Jordan/Basic.lean

A MVP for a real (commutative) Jordan algebra would be:

import Mathlib.Algebra.Jordan.Basic
import Mathlib.Data.Real.Basic

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

I then started to think about quadratic Jordan algebras and fell into a rabbit hole of trying to convert all of the forms to maps which I'm yet to crawl out of (reviews on the PRs welcome).