The split Albert algebra

The split Albert algebra H₃(𝕆) over a commutative ring R in which 2 is invertible is the space of 3 × 3 Hermitian matrices over the split octonions TauCeti.Octonion R,

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

under the symmetrized product A ∘ B = ½ (A B + B A). A Hermitian matrix is recorded here by the data it consists of — a scalar diagonal d : Fin 3 → R and three octonion entries x : Fin 3 → Octonion R, the entry x i sitting in position (i + 1, i + 2) — rather than as a Matrix (Fin 3) (Fin 3) (Octonion R) cut out by a Hermitian predicate: octonion matrices do not form a ring (their entries do not associate), so Matrix.mul would carry no algebraic structure to inherit, and the subtype would still have to be given its multiplication by hand.

Carrying out the matrix product ½ (A B + B A) on that data leaves an expression in the octonion multiplication and in the symmetric bilinear form of the split-octonion norm. That form is Mathlib's β = QuadraticMap.associated (TauCeti.Octonion.normQuadraticForm R) — half the polar form, and the scalar ½ (x * conj y + y * conj x) — so the bilinearity and symmetry the product needs are Mathlib's. The diagonal of the product is d i * e i + β (x (i + 1)) (y (i + 1)) + β (x (i + 2)) (y (i + 2)), and the entries are ½ ((d (i + 1) + d (i + 2)) • y i + (e (i + 1) + e (i + 2)) • x i) corrected by the conjugate of ½ (x (i + 1) * y (i + 2) + y (i + 1) * x (i + 2)). That expression is the definition below.

The product is commutative, R-bilinear, and unital with the identity matrix as its unit, and the three diagonal idempotents form a complete orthogonal frame. The Jordan identity (A ∘ B) ∘ A² = A ∘ (B ∘ A²) — that is, IsCommJordan (AlbertAlgebra R) — is not proved here; it is what makes H₃(𝕆) an exceptional Jordan algebra rather than merely a commutative one.

The coordinate isomorphism works for any semiring acting on coefficients that form an additive commutative monoid. The trace, its kernel and the decomposition of a Hermitian matrix into the diagonal frame and the off-diagonal slots need only a semiring, while the symmetrized product needs a commutative ring in which 2 is invertible: over ℤ the halved symmetric form of the split-octonion norm is not integral. The dimension counts ask for StrongRankCondition, over a semiring for H₃(𝕆) itself and over a ring for the trace-zero subspace.

Main definitions

• TauCeti.AlbertAlgebra: the split Albert algebra over R, with its NonAssocCommRing and Module R structure and the SMulCommClass and IsScalarTower instances that say the product is R-bilinear.
• TauCeti.AlbertAlgebra.trace: the trace d 0 + d 1 + d 2, an R-linear functional.
• TauCeti.AlbertAlgebra.traceZero: the trace-zero subspace J₀, the kernel of the trace.
• TauCeti.AlbertAlgebra.diagIdempotent: the three diagonal idempotents E₀, E₁, E₂.
• TauCeti.AlbertAlgebra.offDiagSingle: the three off-diagonal slots Fⱼ(a), the Hermitian matrix whose only nonzero entry is the octonion a in position (j + 1, j + 2).

Main results

• TauCeti.AlbertAlgebra.finrank_eq_twentySeven: H₃(𝕆) is 27-dimensional.
• TauCeti.AlbertAlgebra.finrank_traceZero: the trace-zero subspace is 26-dimensional.
• the NonAssocCommRing instance: the product is R-bilinear and commutative, and the identity matrix is a two-sided unit. It is NonAssocCommRing and not CommRing because the product is not associative.
• TauCeti.AlbertAlgebra.diagIdempotent_mul_diagIdempotent and TauCeti.AlbertAlgebra.sum_diagIdempotent: the diagonal idempotents are orthogonal and sum to 1.
• TauCeti.AlbertAlgebra.diagIdempotent_mul_offDiagSingle: the Peirce relation between the diagonal frame and the off-diagonal slots: Eᵢ annihilates its opposite slot and halves the other two.
• TauCeti.AlbertAlgebra.eq_sum_smul_diagIdempotent_add_sum_offDiagSingle: the diagonal frame and the off-diagonal slots span H₃(𝕆).

Implementation notes

The additive and module structures are transported along TauCeti.AlbertAlgebra.addEquivProd, which packages a Hermitian matrix as the pair of its diagonal and its octonion entries; TauCeti.AlbertAlgebra.linearEquivProd upgrades it to a linear isomorphism over any semiring acting on the coefficients. The 27-dimensional count uses this isomorphism with R acting on itself; the trace-zero count uses a separate coordinate isomorphism that drops the last diagonal entry, which a vanishing trace determines.

The multiplication is deliberately left unexposed: its body does not unfold outside this file, and a product is read through the projection simp lemmas TauCeti.AlbertAlgebra.mul_diag and TauCeti.AlbertAlgebra.mul_offDiag, which give its two components.

References

The model is P. Jordan, J. von Neumann and E. Wigner, On an algebraic generalization of the quantum mechanical formalism, Ann. of Math. 35 (1934); see also T. A. Springer and F. D. Veldkamp, Octonions, Jordan Algebras and Exceptional Groups, §5.3, and J. C. Baez, The octonions, Bull. Amer. Math. Soc. 39 (2002), §3.4, from which the coordinate form of the product above is taken.

structure TauCeti.AlbertAlgebra (R : Type u_1) : Type u_1

The split Albert algebra H₃(𝕆) over R: a 3 × 3 Hermitian matrix over the split octonions, recorded as its scalar diagonal together with its three octonion entries.

• diag : Fin 3 → R

  The scalar diagonal of the Hermitian matrix.

• offDiag : Fin 3 → Octonion R

  The octonion entries: offDiag i is the entry in position (i + 1, i + 2), and the entry in position (i + 2, i + 1) is its conjugate.

theorem TauCeti.AlbertAlgebra.ext_iff {R : Type u_1} {x y : AlbertAlgebra R} : x = y ↔ x.diag = y.diag ∧ x.offDiag = y.offDiag

theorem TauCeti.AlbertAlgebra.ext {R : Type u_1} {x y : AlbertAlgebra R} (diag : x.diag = y.diag) (offDiag : x.offDiag = y.offDiag) : x = y

The additive and module structure

@[instance_reducible]

instance TauCeti.AlbertAlgebra.instZero {R : Type u_1} [Zero R] : Zero (AlbertAlgebra R)

Equations

• TauCeti.AlbertAlgebra.instZero = { zero := { diag := 0, offDiag := 0 } }

@[simp]

theorem TauCeti.AlbertAlgebra.zero_diag {R : Type u_1} [Zero R] : diag 0 = 0

@[simp]

theorem TauCeti.AlbertAlgebra.zero_offDiag {R : Type u_1} [Zero R] : offDiag 0 = 0

@[instance_reducible]

instance TauCeti.AlbertAlgebra.instInhabitedOfZero {R : Type u_1} [Zero R] : Inhabited (AlbertAlgebra R)

Equations

• TauCeti.AlbertAlgebra.instInhabitedOfZero = { default := 0 }

@[instance_reducible]

instance TauCeti.AlbertAlgebra.instOneOfZero {R : Type u_1} [Zero R] [One R] : One (AlbertAlgebra R)

Equations

• TauCeti.AlbertAlgebra.instOneOfZero = { one := { diag := 1, offDiag := 0 } }

@[simp]

theorem TauCeti.AlbertAlgebra.one_diag {R : Type u_1} [Zero R] [One R] : diag 1 = 1

@[simp]

theorem TauCeti.AlbertAlgebra.one_offDiag {R : Type u_1} [Zero R] [One R] : offDiag 1 = 0

@[instance_reducible]

instance TauCeti.AlbertAlgebra.instAdd {R : Type u_1} [Add R] : Add (AlbertAlgebra R)

Equations

• TauCeti.AlbertAlgebra.instAdd = { add := fun (A B : TauCeti.AlbertAlgebra R) => { diag := A.diag + B.diag, offDiag := A.offDiag + B.offDiag } }

@[simp]

theorem TauCeti.AlbertAlgebra.add_diag {R : Type u_1} [Add R] (A B : AlbertAlgebra R) : (A + B).diag = A.diag + B.diag

@[simp]

theorem TauCeti.AlbertAlgebra.add_offDiag {R : Type u_1} [Add R] (A B : AlbertAlgebra R) : (A + B).offDiag = A.offDiag + B.offDiag

@[instance_reducible]

instance TauCeti.AlbertAlgebra.instNeg {R : Type u_1} [Neg R] : Neg (AlbertAlgebra R)

Equations

• TauCeti.AlbertAlgebra.instNeg = { neg := fun (A : TauCeti.AlbertAlgebra R) => { diag := -A.diag, offDiag := -A.offDiag } }

@[simp]

theorem TauCeti.AlbertAlgebra.neg_diag {R : Type u_1} [Neg R] (A : AlbertAlgebra R) : (-A).diag = -A.diag

@[simp]

theorem TauCeti.AlbertAlgebra.neg_offDiag {R : Type u_1} [Neg R] (A : AlbertAlgebra R) : (-A).offDiag = -A.offDiag

@[instance_reducible]

instance TauCeti.AlbertAlgebra.instSub {R : Type u_1} [Sub R] : Sub (AlbertAlgebra R)

Equations

• TauCeti.AlbertAlgebra.instSub = { sub := fun (A B : TauCeti.AlbertAlgebra R) => { diag := A.diag - B.diag, offDiag := A.offDiag - B.offDiag } }

@[simp]

theorem TauCeti.AlbertAlgebra.sub_diag {R : Type u_1} [Sub R] (A B : AlbertAlgebra R) : (A - B).diag = A.diag - B.diag

@[simp]

theorem TauCeti.AlbertAlgebra.sub_offDiag {R : Type u_1} [Sub R] (A B : AlbertAlgebra R) : (A - B).offDiag = A.offDiag - B.offDiag

@[instance_reducible]

instance TauCeti.AlbertAlgebra.instSMul {R : Type u_1} {S : Type u_2} [SMul S R] : SMul S (AlbertAlgebra R)

Equations

• TauCeti.AlbertAlgebra.instSMul = { smul := fun (s : S) (A : TauCeti.AlbertAlgebra R) => { diag := s • A.diag, offDiag := s • A.offDiag } }

@[simp]

theorem TauCeti.AlbertAlgebra.smul_diag {R : Type u_1} {S : Type u_2} [SMul S R] (s : S) (A : AlbertAlgebra R) : (s • A).diag = s • A.diag

@[simp]

theorem TauCeti.AlbertAlgebra.smul_offDiag {R : Type u_1} {S : Type u_2} [SMul S R] (s : S) (A : AlbertAlgebra R) : (s • A).offDiag = s • A.offDiag

def TauCeti.AlbertAlgebra.addEquivProd (R : Type u_3) [Add R] : AlbertAlgebra R ≃+ (Fin 3 → R) × (Fin 3 → Octonion R)

The components of a Hermitian matrix, as an additive isomorphism with the pair of its scalar diagonal and its octonion entries. The additive and module structures are transported along it, and TauCeti.AlbertAlgebra.linearEquivProd upgrades it to a linear isomorphism over any semiring acting on the coefficients.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AlbertAlgebra.addEquivProd_apply {R : Type u_1} [Add R] (A : AlbertAlgebra R) : (addEquivProd R) A = (A.diag, A.offDiag)

@[simp]

theorem TauCeti.AlbertAlgebra.addEquivProd_symm_apply {R : Type u_1} [Add R] (p : (Fin 3 → R) × (Fin 3 → Octonion R)) : (addEquivProd R).symm p = { diag := p.1, offDiag := p.2 }

@[instance_reducible]

instance TauCeti.AlbertAlgebra.instAddCommMonoid {R : Type u_1} [AddCommMonoid R] : AddCommMonoid (AlbertAlgebra R)

Equations

• TauCeti.AlbertAlgebra.instAddCommMonoid = Function.Injective.addCommMonoid ⇑(TauCeti.AlbertAlgebra.addEquivProd R) ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

instance TauCeti.AlbertAlgebra.instAddCommGroup {R : Type u_1} [AddCommGroup R] : AddCommGroup (AlbertAlgebra R)

Equations

• TauCeti.AlbertAlgebra.instAddCommGroup = Function.Injective.addCommGroup ⇑(TauCeti.AlbertAlgebra.addEquivProd R) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

instance TauCeti.AlbertAlgebra.instDistribMulAction {R : Type u_1} {S : Type u_2} [Monoid S] [AddCommMonoid R] [DistribMulAction S R] : DistribMulAction S (AlbertAlgebra R)

Equations

• TauCeti.AlbertAlgebra.instDistribMulAction = Function.Injective.distribMulAction (TauCeti.AlbertAlgebra.addEquivProd R).toAddMonoidHom ⋯ ⋯

@[instance_reducible]

instance TauCeti.AlbertAlgebra.instModule {R : Type u_1} {S : Type u_2} [Semiring S] [AddCommMonoid R] [Module S R] : Module S (AlbertAlgebra R)

Equations

• TauCeti.AlbertAlgebra.instModule = Function.Injective.module S (TauCeti.AlbertAlgebra.addEquivProd R).toAddMonoidHom ⋯ ⋯

@[instance_reducible]

instance TauCeti.AlbertAlgebra.instAddCommGroupWithOneOfAddCommGroupOfOne {R : Type u_1} [AddCommGroup R] [One R] : AddCommGroupWithOne (AlbertAlgebra R)

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.AlbertAlgebra.linearEquivProd (S : Type u_3) (R : Type u_4) [Semiring S] [AddCommMonoid R] [Module S R] : AlbertAlgebra R ≃ₗ[S] (Fin 3 → R) × (Fin 3 → Octonion R)

The components of a Hermitian matrix, as a linear isomorphism with the pair of its scalar diagonal and its octonion entries, over any semiring acting on the coefficients.

Equations

• TauCeti.AlbertAlgebra.linearEquivProd S R = (TauCeti.AlbertAlgebra.addEquivProd R).toLinearEquiv ⋯

@[simp]

theorem TauCeti.AlbertAlgebra.linearEquivProd_apply {R : Type u_1} {S : Type u_2} [Semiring S] [AddCommMonoid R] [Module S R] (A : AlbertAlgebra R) : (linearEquivProd S R) A = (A.diag, A.offDiag)

@[simp]

theorem TauCeti.AlbertAlgebra.linearEquivProd_symm_apply {R : Type u_1} {S : Type u_2} [Semiring S] [AddCommMonoid R] [Module S R] (p : (Fin 3 → R) × (Fin 3 → Octonion R)) : (linearEquivProd S R).symm p = { diag := p.1, offDiag := p.2 }

instance TauCeti.AlbertAlgebra.instFree {R : Type u_1} [Semiring R] : Module.Free R (AlbertAlgebra R)

instance TauCeti.AlbertAlgebra.instFinite {R : Type u_1} [Semiring R] : Module.Finite R (AlbertAlgebra R)

theorem TauCeti.AlbertAlgebra.finrank_eq_twentySeven (R : Type u_3) [Semiring R] [StrongRankCondition R] : Module.finrank R (AlbertAlgebra R) = 27

The split Albert algebra is 27-dimensional: three scalars on the diagonal and three 8-dimensional octonion entries.

The symmetrized product

@[instance_reducible]

instance TauCeti.AlbertAlgebra.instMulOfInvertibleOfNat {R : Type u_1} [CommRing R] [Invertible 2] : Mul (AlbertAlgebra R)

The symmetrized matrix product A ∘ B = ½ (A B + B A), written out on the diagonal and on the octonion entries of a Hermitian matrix. The symmetric bilinear form associated with the octonion norm — Mathlib's QuadraticMap.associated, half the polar form — enters on the diagonal, and the conjugate of a symmetrized octonion product off it.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AlbertAlgebra.mul_diag {R : Type u_1} [CommRing R] [Invertible 2] (A B : AlbertAlgebra R) (i : Fin 3) : (A * B).diag i = A.diag i * B.diag i + ((QuadraticMap.associated (Octonion.normQuadraticForm R)) (A.offDiag (i + 1))) (B.offDiag (i + 1)) + ((QuadraticMap.associated (Octonion.normQuadraticForm R)) (A.offDiag (i + 2))) (B.offDiag (i + 2))

@[simp]

theorem TauCeti.AlbertAlgebra.mul_offDiag {R : Type u_1} [CommRing R] [Invertible 2] (A B : AlbertAlgebra R) (i : Fin 3) : (A * B).offDiag i = ⅟2 • ((A.diag (i + 1) + A.diag (i + 2)) • B.offDiag i + (B.diag (i + 1) + B.diag (i + 2)) • A.offDiag i) + Octonion.conj (⅟2 • (A.offDiag (i + 1) * B.offDiag (i + 2) + B.offDiag (i + 1) * A.offDiag (i + 2)))

@[instance_reducible]

instance TauCeti.AlbertAlgebra.instNonAssocCommRing {R : Type u_1} [CommRing R] [Invertible 2] : NonAssocCommRing (AlbertAlgebra R)

Equations

• One or more equations did not get rendered due to their size.

instance TauCeti.AlbertAlgebra.instSMulCommClass {R : Type u_1} [CommRing R] [Invertible 2] : SMulCommClass R (AlbertAlgebra R) (AlbertAlgebra R)

instance TauCeti.AlbertAlgebra.instIsScalarTower {R : Type u_1} [CommRing R] [Invertible 2] : IsScalarTower R (AlbertAlgebra R) (AlbertAlgebra R)

The trace

def TauCeti.AlbertAlgebra.trace {R : Type u_1} [Semiring R] : AlbertAlgebra R →ₗ[R] R

The trace of a Hermitian octonion matrix: the sum of its three scalar diagonal entries.

Equations

• TauCeti.AlbertAlgebra.trace = { toFun := fun (A : TauCeti.AlbertAlgebra R) => ∑ i : Fin 3, A.diag i, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.AlbertAlgebra.trace_apply {R : Type u_1} [Semiring R] (A : AlbertAlgebra R) : trace A = ∑ i : Fin 3, A.diag i

theorem TauCeti.AlbertAlgebra.trace_one {R : Type u_1} [Semiring R] : trace 1 = 3

The trace of the identity matrix is 3, one for each diagonal entry. Not a simp lemma, because TauCeti.AlbertAlgebra.trace_apply already takes its left-hand side apart.

theorem TauCeti.AlbertAlgebra.trace_surjective {R : Type u_1} [Semiring R] : Function.Surjective ⇑trace

The trace is a surjection onto the base ring: it already is on the first diagonal entry.

def TauCeti.AlbertAlgebra.traceZero (R : Type u_3) [Semiring R] : Submodule R (AlbertAlgebra R)

The trace-zero submodule J₀ ⊆ H₃(𝕆), the kernel of the trace. Over a ring satisfying StrongRankCondition it is 26-dimensional (TauCeti.AlbertAlgebra.finrank_traceZero). Over a ring in which 3 is invertible, it complements the scalar matrices; in characteristic 3, it contains the identity matrix.

Equations

• TauCeti.AlbertAlgebra.traceZero R = TauCeti.AlbertAlgebra.trace.ker

@[simp]

theorem TauCeti.AlbertAlgebra.mem_traceZero {R : Type u_1} [Semiring R] {A : AlbertAlgebra R} : A ∈ traceZero R ↔ trace A = 0

theorem TauCeti.AlbertAlgebra.finrank_traceZero (R : Type u_3) [Ring R] [StrongRankCondition R] : Module.finrank R ↥(traceZero R) = 26

The trace-zero subspace of the split Albert algebra is 26-dimensional: a vanishing trace pins the last diagonal entry to the negative of the sum of the other two.

The diagonal frame of idempotents

def TauCeti.AlbertAlgebra.diagIdempotent (R : Type u_3) [Zero R] [One R] (i : Fin 3) : AlbertAlgebra R

The i-th diagonal idempotent Eᵢ of H₃(𝕆): the Hermitian matrix with a single 1 in position (i, i).

Equations

• TauCeti.AlbertAlgebra.diagIdempotent R i = { diag := Pi.single i 1, offDiag := 0 }

@[simp]

theorem TauCeti.AlbertAlgebra.diagIdempotent_diag {R : Type u_1} [Zero R] [One R] (i : Fin 3) : (diagIdempotent R i).diag = Pi.single i 1

@[simp]

theorem TauCeti.AlbertAlgebra.diagIdempotent_offDiag {R : Type u_1} [Zero R] [One R] (i : Fin 3) : (diagIdempotent R i).offDiag = 0

@[simp]

theorem TauCeti.AlbertAlgebra.diagIdempotent_mul_diagIdempotent {R : Type u_1} [CommRing R] [Invertible 2] (i j : Fin 3) : diagIdempotent R i * diagIdempotent R j = if i = j then diagIdempotent R i else 0

The diagonal idempotents are orthogonal: Eᵢ ∘ Eⱼ is Eᵢ when i = j and 0 otherwise.

@[simp]

theorem TauCeti.AlbertAlgebra.sum_diagIdempotent {R : Type u_1} [AddCommMonoid R] [One R] : ∑ i : Fin 3, diagIdempotent R i = 1

The diagonal idempotents add up to the identity matrix.

theorem TauCeti.AlbertAlgebra.trace_diagIdempotent {R : Type u_1} [Semiring R] (i : Fin 3) : trace (diagIdempotent R i) = 1

Each diagonal idempotent has trace 1, so the frame accounts for the whole trace of the identity.

The off-diagonal slots

def TauCeti.AlbertAlgebra.offDiagSingle {R : Type u_1} [Zero R] (j : Fin 3) (a : Octonion R) : AlbertAlgebra R

The Hermitian octonion matrix whose only nonzero entry is the octonion a, in position (j + 1, j + 2): the j-th off-diagonal slot Fⱼ(a) of H₃(𝕆). Together with the diagonal frame TauCeti.AlbertAlgebra.diagIdempotent these span the algebra.

Equations

• TauCeti.AlbertAlgebra.offDiagSingle j a = { diag := 0, offDiag := Pi.single j a }

@[simp]

theorem TauCeti.AlbertAlgebra.offDiagSingle_diag {R : Type u_1} [Zero R] (j : Fin 3) (a : Octonion R) : (offDiagSingle j a).diag = 0

@[simp]

theorem TauCeti.AlbertAlgebra.offDiagSingle_offDiag {R : Type u_1} [Zero R] (j : Fin 3) (a : Octonion R) : (offDiagSingle j a).offDiag = Pi.single j a

@[simp]

theorem TauCeti.AlbertAlgebra.offDiagSingle_zero {R : Type u_1} [Zero R] (j : Fin 3) : offDiagSingle j 0 = 0

@[simp]

theorem TauCeti.AlbertAlgebra.offDiagSingle_add {R : Type u_1} [AddCommMonoid R] (j : Fin 3) (a b : Octonion R) : offDiagSingle j (a + b) = offDiagSingle j a + offDiagSingle j b

@[simp]

theorem TauCeti.AlbertAlgebra.offDiagSingle_neg {R : Type u_1} [AddCommGroup R] (j : Fin 3) (a : Octonion R) : offDiagSingle j (-a) = -offDiagSingle j a

@[simp]

theorem TauCeti.AlbertAlgebra.offDiagSingle_smul {R : Type u_1} {S : Type u_2} [Monoid S] [AddCommMonoid R] [DistribMulAction S R] (s : S) (j : Fin 3) (a : Octonion R) : offDiagSingle j (s • a) = s • offDiagSingle j a

@[simp]

theorem TauCeti.AlbertAlgebra.diagIdempotent_mul_offDiagSingle {R : Type u_1} [CommRing R] [Invertible 2] (i j : Fin 3) (a : Octonion R) : diagIdempotent R i * offDiagSingle j a = if i = j then 0 else ⅟2 • offDiagSingle j a

The Peirce relation between the diagonal frame and the off-diagonal slots: the j-th slot sits in position (j + 1, j + 2), so Eⱼ — whose only entry is in position (j, j) — annihilates it, while the two other idempotents halve it.

theorem TauCeti.AlbertAlgebra.eq_sum_smul_diagIdempotent_add_sum_offDiagSingle {R : Type u_1} [Semiring R] (A : AlbertAlgebra R) : A = ∑ i : Fin 3, A.diag i • diagIdempotent R i + ∑ i : Fin 3, offDiagSingle i (A.offDiag i)

The diagonal frame and the off-diagonal slots span H₃(𝕆): a Hermitian octonion matrix is the combination of the diagonal idempotents read off its diagonal, plus its three off-diagonal slots.