The determinant of the split Albert algebra and its cubic equation

A Hermitian octonion matrix

⟦a, x⟧ = [[a 0, x 2, conj (x 1)], [conj (x 2), a 1, x 0], [x 1, conj (x 0), a 2]]

of the split Albert algebra H₃(𝕆) has a determinant, the cubic form

`det A = a 0 * a 1 * a 2 - a 0 * N (x 0) - a 1 * N (x 1) - a 2 * N (x 2)

• trace ((x 0 * x 1) * x 2)`,

where N and trace are the norm and the trace of the split octonions. The octonion entry x i sits opposite the diagonal entry a i, in position (i + 1, i + 2), so each diagonal entry is paired with the norm of the octonion entry it does not share a row or column with; the last term is the trace of the product of the three octonion entries taken around the matrix. That trace does not depend on the bracketing of the triple product nor on which entry the cycle starts from (TauCeti.Octonion.trace_mul_assoc and TauCeti.Octonion.trace_mul_cycle), so the determinant can be read off starting from any diagonal entry (TauCeti.AlbertAlgebra.det_eq_rotate).

Together with the trace T and the quadratic spur S, the sum of the principal 2 × 2 minors

spur A = a 0 * a 1 + a 1 * a 2 + a 2 * a 0 - N (x 0) - N (x 1) - N (x 2),

the determinant is, up to sign, the constant term of the generic minimal polynomial t³ - T(A) t² + S(A) t - det A of H₃(𝕆), and the spur is its coefficient of t: every element satisfies the cubic equation

A ∘ (A ∘ A) = T(A) • (A ∘ A) - S(A) • A + det A • 1

(TauCeti.AlbertAlgebra.mul_mul_self), the Albert-algebra analogue of the rank-two equation TauCeti.Octonion.mul_self of the octonions, with powers taken in the Jordan product. Taking traces in it, and using 2 S(A) = T(A)² - T(A ∘ A), gives Newton's formula for the determinant in terms of the traces of powers, 6 det A = T(A)³ - 3 T(A) T(A ∘ A) + 2 T(A ∘ (A ∘ A)).

The determinant and the spur are defined over every commutative ring; only the Jordan product, and so the cubic equation, needs 2 to be invertible, and dividing Newton's formula by 6 needs 3 to be invertible as well.

Main definitions

• TauCeti.AlbertAlgebra.det: the determinant, the cubic norm form of H₃(𝕆).
• TauCeti.AlbertAlgebra.spur: the spur, a quadratic form in A and the coefficient of t in the generic minimal polynomial.

Main results

• TauCeti.AlbertAlgebra.det_smul and TauCeti.AlbertAlgebra.spur_smul: the determinant is homogeneous of degree three and the spur homogeneous of degree two.
• TauCeti.AlbertAlgebra.two_mul_spur and TauCeti.AlbertAlgebra.spur_eq_invOf_two_mul: the spur is (T(A)² - T(A ∘ A)) / 2.
• TauCeti.AlbertAlgebra.spur_add and TauCeti.AlbertAlgebra.spur_sub: the polarization of the spur, S(A + B) = S(A) + S(B) + T(A) T(B) - T(A ∘ B).
• TauCeti.AlbertAlgebra.det_add_sub_det_sub: the gradient of the determinant, in polarized form.
• TauCeti.AlbertAlgebra.mul_mul_self: the cubic equation satisfied by every element.
• TauCeti.AlbertAlgebra.mul_mul_self_add_two_smul_mul_mul: the linearized cubic equation, the polarization of the cubic equation.
• TauCeti.AlbertAlgebra.six_mul_det and TauCeti.AlbertAlgebra.det_eq_invOf_two_mul_invOf_three_mul: Newton's formula for the determinant in terms of the traces of the powers.

References

• J. C. Baez, The octonions, Bull. Amer. Math. Soc. 39 (2002), §3.4, for the coordinate formula of the determinant and the trace formula for it.
• K. McCrimmon, A Taste of Jordan Algebras, Springer (2004), the chapter on Jordan algebras of cubic forms, for the generic minimal polynomial t³ - T t² + S t - N of a cubic Jordan algebra, its spur form S, and the cubic equation.
• T. A. Springer and F. D. Veldkamp, Octonions, Jordan Algebras and Exceptional Groups, Springer (2000), Chapter 5.

def TauCeti.AlbertAlgebra.det {R : Type u_1} [CommRing R] (A : AlbertAlgebra R) : R

The determinant of a Hermitian octonion matrix, the cubic norm form of the split Albert algebra: a₀ a₁ a₂ - a₀ N(x₀) - a₁ N(x₁) - a₂ N(x₂) + trace ((x₀ x₁) x₂), with aᵢ the diagonal entries and xᵢ the octonion entry in position (i + 1, i + 2).

theorem TauCeti.AlbertAlgebra.det_def {R : Type u_1} [CommRing R] (A : AlbertAlgebra R) : A.det = A.diag 0 * A.diag 1 * A.diag 2 - A.diag 0 * (A.offDiag 0).norm - A.diag 1 * (A.offDiag 1).norm - A.diag 2 * (A.offDiag 2).norm + Octonion.trace (A.offDiag 0 * A.offDiag 1 * A.offDiag 2)

theorem TauCeti.AlbertAlgebra.trace_offDiag_mul_offDiag_mul_offDiag {R : Type u_1} [CommRing R] (A : AlbertAlgebra R) (i : Fin 3) : Octonion.trace (A.offDiag i * A.offDiag (i + 1) * A.offDiag (i + 2)) = Octonion.trace (A.offDiag 0 * A.offDiag 1 * A.offDiag 2)

The triple-product term of the determinant does not depend on where the cycle starts: the octonion entries can be multiplied in any cyclic order, xᵢ xᵢ₊₁ xᵢ₊₂.

theorem TauCeti.AlbertAlgebra.det_eq_rotate {R : Type u_1} [CommRing R] (A : AlbertAlgebra R) (i : Fin 3) : A.det = A.diag i * A.diag (i + 1) * A.diag (i + 2) - A.diag i * (A.offDiag i).norm - A.diag (i + 1) * (A.offDiag (i + 1)).norm - A.diag (i + 2) * (A.offDiag (i + 2)).norm + Octonion.trace (A.offDiag i * A.offDiag (i + 1) * A.offDiag (i + 2))

The determinant, read off starting from an arbitrary diagonal entry.

@[simp]

theorem TauCeti.AlbertAlgebra.det_zero {R : Type u_1} [CommRing R] : det 0 = 0

@[simp]

theorem TauCeti.AlbertAlgebra.det_one {R : Type u_1} [CommRing R] : det 1 = 1

@[simp]

theorem TauCeti.AlbertAlgebra.det_smul {R : Type u_1} [CommRing R] (r : R) (A : AlbertAlgebra R) : (r • A).det = r ^ 3 * A.det

The determinant is homogeneous of degree three: det (r • A) = r ^ 3 * det A.

@[simp]

theorem TauCeti.AlbertAlgebra.det_neg {R : Type u_1} [CommRing R] (A : AlbertAlgebra R) : (-A).det = -A.det

def TauCeti.AlbertAlgebra.spur {R : Type u_1} [CommRing R] (A : AlbertAlgebra R) : R

The spur of a Hermitian octonion matrix, the sum of its three principal 2 × 2 minors: a₀ a₁ + a₁ a₂ + a₂ a₀ - N(x₀) - N(x₁) - N(x₂). It is a quadratic form in A and the coefficient of t in the generic minimal polynomial of the split Albert algebra (TauCeti.AlbertAlgebra.mul_mul_self), and equals (T(A)² - T(A ∘ A)) / 2 when 2 is invertible (TauCeti.AlbertAlgebra.spur_eq_invOf_two_mul).

theorem TauCeti.AlbertAlgebra.spur_def {R : Type u_1} [CommRing R] (A : AlbertAlgebra R) : A.spur = A.diag 0 * A.diag 1 + A.diag 1 * A.diag 2 + A.diag 2 * A.diag 0 - (A.offDiag 0).norm - (A.offDiag 1).norm - (A.offDiag 2).norm

theorem TauCeti.AlbertAlgebra.spur_eq_rotate {R : Type u_1} [CommRing R] (A : AlbertAlgebra R) (i : Fin 3) : A.spur = A.diag i * A.diag (i + 1) + A.diag (i + 1) * A.diag (i + 2) + A.diag (i + 2) * A.diag i - (A.offDiag i).norm - (A.offDiag (i + 1)).norm - (A.offDiag (i + 2)).norm

The spur, read off starting from an arbitrary diagonal entry.

@[simp]

theorem TauCeti.AlbertAlgebra.spur_zero {R : Type u_1} [CommRing R] : spur 0 = 0

@[simp]

theorem TauCeti.AlbertAlgebra.spur_one {R : Type u_1} [CommRing R] : spur 1 = 3

The spur of the identity matrix is 3, one for each principal 2 × 2 minor.

@[simp]

theorem TauCeti.AlbertAlgebra.spur_smul {R : Type u_1} [CommRing R] (r : R) (A : AlbertAlgebra R) : (r • A).spur = r ^ 2 * A.spur

The spur is homogeneous of degree two: spur (r • A) = r ^ 2 * spur A.

@[simp]

theorem TauCeti.AlbertAlgebra.spur_neg {R : Type u_1} [CommRing R] (A : AlbertAlgebra R) : (-A).spur = A.spur

The Jordan square and the cubic equation

theorem TauCeti.AlbertAlgebra.two_mul_spur {R : Type u_1} [CommRing R] [Invertible 2] (A : AlbertAlgebra R) : 2 * A.spur = trace A ^ 2 - trace (A * A)

Twice the spur is T(A)² - T(A ∘ A).

theorem TauCeti.AlbertAlgebra.spur_eq_invOf_two_mul {R : Type u_1} [CommRing R] [Invertible 2] (A : AlbertAlgebra R) : A.spur = ⅟2 * (trace A ^ 2 - trace (A * A))

The spur is half of T(A)² - T(A ∘ A), the usual coefficient of a characteristic polynomial in terms of traces of powers.

theorem TauCeti.AlbertAlgebra.spur_add {R : Type u_1} [CommRing R] [Invertible 2] (A B : AlbertAlgebra R) : (A + B).spur = A.spur + B.spur + (trace A * trace B - trace (A * B))

The polarization of the spur: S(A + B) = S(A) + S(B) + T(A) T(B) - T(A ∘ B).

theorem TauCeti.AlbertAlgebra.spur_sub {R : Type u_1} [CommRing R] [Invertible 2] (A B : AlbertAlgebra R) : (A - B).spur = A.spur + B.spur - (trace A * trace B - trace (A * B))

The polarization of the spur at a difference: S(A - B) = S(A) + S(B) - (T(A) T(B) - T(A ∘ B)).

theorem TauCeti.AlbertAlgebra.det_add_sub_det_sub {R : Type u_1} [CommRing R] [Invertible 2] (A B : AlbertAlgebra R) : (A + B).det - (A - B).det - 2 * B.det = 2 * (trace (A * A * B) - trace A * trace (A * B) + A.spur * trace B)

The gradient of the determinant, in polarized form: the part of det (A + B) linear in B is T(A^# ∘ B) = T(A² ∘ B) - T(A) T(A ∘ B) + S(A) T(B).

theorem TauCeti.AlbertAlgebra.mul_mul_self {R : Type u_1} [CommRing R] [Invertible 2] (A : AlbertAlgebra R) : A * (A * A) = trace A • (A * A) - A.spur • A + A.det • 1

The cubic equation of the split Albert algebra. Every Hermitian octonion matrix is a root of its generic minimal polynomial t³ - T(A) t² + S(A) t - det A, with powers taken in the Jordan product: A ∘ (A ∘ A) = T(A) • (A ∘ A) - S(A) • A + det A • 1.

theorem TauCeti.AlbertAlgebra.mul_mul_self_add_two_smul_mul_mul {R : Type u_1} [CommRing R] [Invertible 2] (A B : AlbertAlgebra R) : B * (A * A) + 2 • (A * (A * B)) = trace B • (A * A) + (2 * trace A) • (A * B) - (trace A * trace B - trace (A * B)) • A - A.spur • B + (trace (A * A * B) - trace A * trace (A * B) + A.spur * trace B) • 1

The linearized cubic equation of the split Albert algebra: the part linear in B of the cubic equation TauCeti.AlbertAlgebra.mul_mul_self at A + B, `B ∘ A² + 2 A ∘ (A ∘ B) = T(B) A² + 2 T(A) A ∘ B - (T(A) T(B) - T(A ∘ B)) A - S(A) B

• T(A^# ∘ B) 1, with T(A^# ∘ B) = T(A² ∘ B) - T(A) T(A ∘ B) + S(A) T(B)`.

theorem TauCeti.AlbertAlgebra.six_mul_det {R : Type u_1} [CommRing R] [Invertible 2] (A : AlbertAlgebra R) : 6 * A.det = trace A ^ 3 - 3 * trace A * trace (A * A) + 2 * trace (A * (A * A))

Newton's formula for the determinant, without division: 6 det A = T(A)³ - 3 T(A) T(A ∘ A) + 2 T(A ∘ (A ∘ A)).

theorem TauCeti.AlbertAlgebra.det_eq_invOf_two_mul_invOf_three_mul {R : Type u_1} [CommRing R] [Invertible 2] [Invertible 3] (A : AlbertAlgebra R) : A.det = ⅟2 * ⅟3 * (trace A ^ 3 - 3 * trace A * trace (A * A) + 2 * trace (A * (A * A)))

Newton's formula for the determinant: when 2 and 3 are invertible, det A = (T(A)³ - 3 T(A) T(A ∘ A) + 2 T(A ∘ (A ∘ A))) / 6.