Derivations of the split octonions

G₂ is the derivation algebra of the split octonions, and its fundamental representation is supposed to be the 7-dimensional space of imaginary octonions. Neither statement can even be made until one knows that a derivation of 𝕆 lands in the imaginary octonions and respects the norm form; that is what this file proves first. It then writes down fourteen independent derivations and shows that there are no others, so that Der 𝕆 ≅ 𝔰𝔩₃ × R³ × R³ and finrank (Der 𝕆) = 14.

Let D be a derivation of TauCeti.Octonion R. Applying D to the rank-two equation x² = tr x · x - N x · 1 and to the polarization x * conj y + y * conj x = ⟨x, y⟩ · 1 of the norm gives one identity in 𝕆,

tr (D x) · x = ⟨x, D x⟩ · 1,

and everything follows from it. Evaluated at the diagonal idempotent e = ⟨1, 0, 0, 0⟩ — an element whose existence is exactly the splitness of 𝕆 — its two diagonal entries read tr (D e) = ⟨e, D e⟩ and 0 = ⟨e, D e⟩. Polarizing it and feeding e into the second slot forces tr (D x) = 0 for every x, and with the trace gone the identity itself collapses to ⟨x, D x⟩ = 0: a derivation is skew for the norm form.

So D maps all of 𝕆 into the imaginary octonions, commutes with conjugation, and lies in the orthogonal Lie algebra of the norm: Der 𝕆 ≤ 𝔰𝔬(N) (TauCeti.Octonion.derivationLieAlgebra_le_skewAdjointLieSubalgebra). In particular the imaginary octonions are a Lie submodule (TauCeti.Octonion.imaginaryLieSubmodule) — over a field in which 2 is nonzero this is the 7-dimensional fundamental representation — and Der 𝕆 acts faithfully on it over every commutative ring. Indeed, the diagonal idempotent e is a product of two imaginary vector matrices, and 𝕆 = R · e ⊕ Im 𝕆, so a derivation vanishing on Im 𝕆 vanishes on all of 𝕆.

The derivations exhibited here come from the action of SL₃ on a Zorn vector matrix, ⟨a, b, v, w⟩ ↦ ⟨a, b, A v, (Aᵀ)⁻¹ w⟩, differentiated at the identity: a trace-zero matrix M acts by M on the upper vector entry and by -Mᵀ on the lower one (TauCeti.Octonion.slDerivation), and this is a homomorphism of Lie algebras 𝔰𝔩₃ → Der 𝕆. The Leibniz rule for it is the identity (M u) ⨯₃ w + u ⨯₃ (M w) = -(Mᵀ (u ⨯₃ w)), valid exactly because M has trace zero (Matrix.mulVec_cross_add_cross_mulVec_of_trace_eq_zero). Two further three-parameter families (TauCeti.Octonion.upperDerivation and TauCeti.Octonion.lowerDerivation) are attached to a vector u, are read off the idempotent ⟨1, 0, 0, 0⟩, and exchange the two vector entries; there they are the two nonzero pieces of the ℤ/3-grading of 𝕆 by scalar diagonal, upper vector and lower vector. That grading is visible in the five brackets between the three families: 𝔰𝔩₃ acts on the upper family by its defining representation and on the lower one by the dual, two upper or two lower derivations bracket into the opposite vector family by twice the cross product, and an upper against a lower one brackets back into 𝔰𝔩₃ through TauCeti.Octonion.slOfVectors. Together the three families depend on 8 + 3 + 3 = 14 independent parameters, so 14 ≤ finrank (Der 𝕆).

Conversely every derivation D is in the family, over any commutative ring. Its value at the idempotent e = ⟨1, 0, 0, 0⟩ has vanishing diagonal entries, so subtracting the upper and the lower derivation attached to its two vector entries leaves a derivation E that kills e. Such an E respects the Peirce decomposition of 𝕆 relative to e: differentiating e x = x and x e = 0 for an upper vector matrix x (and their mirrors for a lower one) shows that E acts on the upper entry by some matrix M, on the lower entry by some matrix N, and kills the diagonal. The product of an upper and a lower vector matrix is diagonal, which forces N = -Mᵀ, and the product of two upper ones is the lower cross product, which by Matrix.mulVec_cross_add_cross_mulVec forces trace M = 0. So E = slDerivation M, and TauCeti.Octonion.tripleEquivDerivationLieAlgebra packages TauCeti.Octonion.derivationOfTriple as a linear equivalence.

Main definitions

• TauCeti.Octonion.imaginaryLieSubmodule: the imaginary octonions as a Lie submodule of 𝕆 over Der 𝕆, so that Im 𝕆 is a representation of Der 𝕆.
• TauCeti.Octonion.slDerivation: the homomorphism of Lie algebras 𝔰𝔩₃ → Der 𝕆, the differentiated action of SL₃ on the vector entries of a Zorn vector matrix.
• TauCeti.Octonion.upperDerivation and TauCeti.Octonion.lowerDerivation: the two three-parameter families of derivations attached to a vector.
• TauCeti.Octonion.derivationOfTriple: the three families assembled into one linear map out of 𝔰𝔩₃ × R³ × R³.
• TauCeti.Octonion.slOfVectors: the trace-zero matrix through which an upper and a lower vector derivation bracket back into 𝔰𝔩₃.
• TauCeti.Octonion.tripleEquivDerivationLieAlgebra: the linear equivalence 𝔰𝔩₃ × R³ × R³ ≃ Der 𝕆 given by the three families.

Main results

• TauCeti.Octonion.trace_derivation_apply_eq_zero: a derivation of 𝕆 has values of trace 0, so (TauCeti.Octonion.derivation_apply_mem_imaginary) its image lies in the imaginary octonions.
• TauCeti.Octonion.derivation_apply_conj: a derivation commutes with conjugation.
• TauCeti.Octonion.polar_derivation_apply_self_eq_zero and TauCeti.Octonion.polar_derivation_apply_left_eq_neg: a derivation is skew for the symmetric bilinear form of the norm, ⟨D x, y⟩ = -⟨x, D y⟩.
• TauCeti.Octonion.derivationLieAlgebra_le_skewAdjointLieSubalgebra: Der 𝕆 ≤ 𝔰𝔬(N), the previous item as an inclusion of Lie subalgebras of Module.End R 𝕆.
• TauCeti.Octonion.isFaithful_imaginaryLieSubmodule: Der 𝕆 acts faithfully on Im 𝕆 over every commutative ring; TauCeti.Octonion.instIsFaithfulImaginaryLieSubmodule is its instance form.
• TauCeti.Octonion.lie_slDerivation_upperDerivation, TauCeti.Octonion.lie_slDerivation_lowerDerivation, TauCeti.Octonion.lie_upperDerivation_upperDerivation, TauCeti.Octonion.lie_lowerDerivation_lowerDerivation and TauCeti.Octonion.lie_upperDerivation_lowerDerivation: the brackets of the three families with one another, the relations of the ℤ/3-grading.
• TauCeti.Octonion.derivationOfTriple_injective: the fourteen parameters are independent. In particular Der 𝕆 is not the zero Lie algebra (TauCeti.Octonion.instNontrivialDerivationLieAlgebra), so none of the above is vacuous.
• TauCeti.Octonion.derivationOfTriple_surjective: every derivation of 𝕆 is in the fourteen-parameter family, over any commutative ring.
• TauCeti.Octonion.finrank_derivationLieAlgebra: finrank (Der 𝕆) = 14, the dimension of G₂, over any commutative ring with the strong rank condition; Der 𝕆 is moreover free and finite as a module.

Implementation notes

Everything is stated over a commutative ring. The rank count finrank (Der 𝕆) = 14 asks in addition for the strong rank condition. Faithfulness needs no further hypothesis on the base ring: the imaginary vector matrices generate the diagonal idempotent by multiplication. In characteristic 2, the imaginary octonions contain the unit, so its line is a trivial subrepresentation; this obstructs irreducibility but does not affect faithfulness.

The two coordinate extractions the argument needs — reading the a and b entries of an equation between multiples of ⟨1, 0, 0, 0⟩ and of 1 — are isolated in a private lemma, so none of the public skewness statements is about entries of a vector matrix.

Derivations are taken in the bundled form D : TauCeti.derivationLieAlgebra R (Octonion R) of TauCeti/Algebra/Lie/Derivation/Basic.lean, and are applied through the coercion (D : Module.End R (Octonion R)), which is the simp-normal form of their action there.

References

The type-G₂ Killing-simplicity of Der 𝕆 and its identification with LieAlgebra.g₂ are not proved here.

• T. A. Springer and F. D. Veldkamp, Octonions, Jordan Algebras and Exceptional Groups, §2.
• R. D. Schafer, An Introduction to Nonassociative Algebras, Ch. III, where the skewness of a derivation of a composition algebra for its norm form is Lemma 3.4.

The key identity

theorem TauCeti.Octonion.derivation_apply_conj_eq_neg {R : Type u_1} [CommRing R] (D : ↥(derivationLieAlgebra R (Octonion R))) (x : Octonion R) : ↑D (conj x) = -↑D x

A derivation negates conjugated inputs. It kills 1 and conjugation is the reflection x ↦ tr x · 1 - x, so D (conj x) = -D x. Once the values of D are known to have vanishing trace this upgrades to TauCeti.Octonion.derivation_apply_conj, the statement that D commutes with conjugation; that is the form to use, and this one is what proves it.

Derivations are imaginary-valued and skew

theorem TauCeti.Octonion.trace_derivation_apply_eq_zero {R : Type u_1} [CommRing R] (D : ↥(derivationLieAlgebra R (Octonion R))) (x : Octonion R) : trace (↑D x) = 0

A derivation of 𝕆 has values of trace 0.

Evaluating the key identity tr (D x) · x = ⟨x, D x⟩ · 1 at the diagonal idempotent e gives tr (D e) = 0, because the two sides have different second diagonal entries; polarizing the identity and putting e in the second slot then gives tr (D x) · e = ⟨x, D e⟩ + ⟨e, D x⟩ · 1 for arbitrary x, and the same entry comparison finishes. Not a simp lemma, because TauCeti.Octonion.trace_apply already takes its left-hand side apart.

theorem TauCeti.Octonion.derivation_apply_mem_imaginary {R : Type u_1} [CommRing R] (D : ↥(derivationLieAlgebra R (Octonion R))) (x : Octonion R) : ↑D x ∈ imaginary R

A derivation of 𝕆 takes imaginary values, that is TauCeti.Octonion.trace_derivation_apply_eq_zero read through the definition of the imaginary octonions as the kernel of the trace. In particular the imaginary octonions are stable under D; that is TauCeti.Octonion.imaginaryLieSubmodule. Not a simp lemma, because TauCeti.Octonion.mem_imaginary and TauCeti.Octonion.trace_apply already take its left-hand side apart, for the same reason as TauCeti.Octonion.trace_derivation_apply_eq_zero.

@[simp]

theorem TauCeti.Octonion.derivation_apply_conj {R : Type u_1} [CommRing R] (D : ↥(derivationLieAlgebra R (Octonion R))) (x : Octonion R) : ↑D (conj x) = conj (↑D x)

A derivation commutes with conjugation. Conjugation negates the imaginary octonions and the values of D are imaginary, so the sign in TauCeti.Octonion.derivation_apply_conj_eq_neg is the one conjugation itself supplies.

@[simp]

theorem TauCeti.Octonion.polar_derivation_apply_self_eq_zero {R : Type u_1} [CommRing R] (D : ↥(derivationLieAlgebra R (Octonion R))) (x : Octonion R) : QuadraticMap.polar (⇑(normQuadraticForm R)) x (↑D x) = 0

A derivation is skew for the norm form, in the quadratic form of that statement: ⟨x, D x⟩ = 0. This is the key identity once its left-hand side is known to vanish, and it is the infinitesimal norm-preservation statement d/dt|₀ N (x + t • D x) = 0.

theorem TauCeti.Octonion.polar_derivation_apply_left_eq_neg {R : Type u_1} [CommRing R] (D : ↥(derivationLieAlgebra R (Octonion R))) (x y : Octonion R) : QuadraticMap.polar (⇑(normQuadraticForm R)) (↑D x) y = -QuadraticMap.polar (⇑(normQuadraticForm R)) x (↑D y)

A derivation is skew for the norm form: ⟨D x, y⟩ = -⟨x, D y⟩, the bilinear form of TauCeti.Octonion.polar_derivation_apply_self_eq_zero. Packaged as an inclusion of Lie subalgebras this is TauCeti.Octonion.derivationLieAlgebra_le_skewAdjointLieSubalgebra.

theorem TauCeti.Octonion.derivationLieAlgebra_le_skewAdjointLieSubalgebra (R : Type u_2) [CommRing R] : derivationLieAlgebra R (Octonion R) ≤ skewAdjointLieSubalgebra (QuadraticMap.polarBilin (normQuadraticForm R))

Der 𝕆 ≤ 𝔰𝔬(N): every derivation of the split octonions is skew-adjoint for the symmetric bilinear form of the norm, so the derivation algebra is a Lie subalgebra of the orthogonal Lie algebra of that form. This is the inclusion Der 𝕆 ↪ 𝔰𝔬(N) that the dimension count of Der 𝕆 runs through; once Der 𝕆 is identified with G₂ — which is not done here — it becomes the familiar G₂ ↪ 𝔰𝔬₈.

The imaginary octonions as a representation of Der 𝕆

def TauCeti.Octonion.imaginaryLieSubmodule (R : Type u_2) [CommRing R] : LieSubmodule R (↥(derivationLieAlgebra R (Octonion R))) (Octonion R)

The imaginary octonions as a Lie submodule of 𝕆 over Der 𝕆. A derivation takes imaginary values on all of 𝕆, so in particular it preserves the imaginary octonions. This is the carrier of the 7-dimensional fundamental representation of G₂; its dimension is TauCeti.Octonion.finrank_imaginary, reached through TauCeti.Octonion.toSubmodule_imaginaryLieSubmodule, and its irreducibility over a field in which 2 is nonzero is TauCeti.Octonion.isIrreducible_imaginaryLieSubmodule in TauCeti/Algebra/Octonion/Fundamental.lean.

Equations

• TauCeti.Octonion.imaginaryLieSubmodule R = { toSubmodule := TauCeti.Octonion.imaginary R, lie_mem := ⋯ }

@[simp]

theorem TauCeti.Octonion.toSubmodule_imaginaryLieSubmodule (R : Type u_2) [CommRing R] : ↑(imaginaryLieSubmodule R) = imaginary R

@[simp]

theorem TauCeti.Octonion.mem_imaginaryLieSubmodule {R : Type u_1} [CommRing R] {x : Octonion R} : x ∈ imaginaryLieSubmodule R ↔ trace x = 0

theorem TauCeti.Octonion.isFaithful_imaginaryLieSubmodule {R : Type u_1} [CommRing R] : LieModule.IsFaithful R ↥(derivationLieAlgebra R (Octonion R)) ↥(imaginaryLieSubmodule R)

Der 𝕆 acts faithfully on the imaginary octonions over every commutative ring, so no information is lost by restricting the derivation algebra to its candidate fundamental representation, including in characteristic 2.

instance TauCeti.Octonion.instIsFaithfulImaginaryLieSubmodule {R : Type u_1} [CommRing R] : LieModule.IsFaithful R ↥(derivationLieAlgebra R (Octonion R)) ↥(imaginaryLieSubmodule R)

Der 𝕆 acts faithfully on the imaginary octonions over every commutative ring, the typeclass form of TauCeti.Octonion.isFaithful_imaginaryLieSubmodule.

The special linear derivations

The two vector families of derivations

The three families, bundled

def TauCeti.Octonion.slDerivation {R : Type u_1} [CommRing R] : ↥(LieAlgebra.SpecialLinear.sl (Fin 3) R) →ₗ⁅R⁆ ↥(derivationLieAlgebra R (Octonion R))

The special linear derivations of 𝕆: the homomorphism of Lie algebras 𝔰𝔩₃ → Der 𝕆 that sends a trace-zero matrix M to the derivation acting by M on the upper vector entry of a Zorn vector matrix and by -Mᵀ on the lower one.

Equations

• TauCeti.Octonion.slDerivation = { toFun := fun (M : ↥(LieAlgebra.SpecialLinear.sl (Fin 3) R)) => ⟨TauCeti.Octonion.slDerivationEnd✝ ↑M, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

@[simp]

theorem TauCeti.Octonion.slDerivation_apply_a {R : Type u_1} [CommRing R] (M : ↥(LieAlgebra.SpecialLinear.sl (Fin 3) R)) (x : Octonion R) : (↑(slDerivation M) x).a = 0

@[simp]

theorem TauCeti.Octonion.slDerivation_apply_b {R : Type u_1} [CommRing R] (M : ↥(LieAlgebra.SpecialLinear.sl (Fin 3) R)) (x : Octonion R) : (↑(slDerivation M) x).b = 0

@[simp]

theorem TauCeti.Octonion.slDerivation_apply_v {R : Type u_1} [CommRing R] (M : ↥(LieAlgebra.SpecialLinear.sl (Fin 3) R)) (x : Octonion R) : (↑(slDerivation M) x).v = (↑M).mulVec x.v

@[simp]

theorem TauCeti.Octonion.slDerivation_apply_w {R : Type u_1} [CommRing R] (M : ↥(LieAlgebra.SpecialLinear.sl (Fin 3) R)) (x : Octonion R) : (↑(slDerivation M) x).w = -(↑M).transpose.mulVec x.w

def TauCeti.Octonion.upperDerivation {R : Type u_1} [CommRing R] : (Fin 3 → R) →ₗ[R] ↥(derivationLieAlgebra R (Octonion R))

The upper vector derivations of 𝕆: the linear map sending u : R³ to the derivation that takes the idempotent ⟨1, 0, 0, 0⟩ to the vector matrix with upper entry u.

Equations

• TauCeti.Octonion.upperDerivation = { toFun := fun (u : Fin 3 → R) => ⟨TauCeti.Octonion.upperDerivationEnd✝ u, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.Octonion.upperDerivation_apply_a {R : Type u_1} [CommRing R] (u : Fin 3 → R) (x : Octonion R) : (↑(upperDerivation u) x).a = -(u ⬝ᵥ x.w)

@[simp]

theorem TauCeti.Octonion.upperDerivation_apply_b {R : Type u_1} [CommRing R] (u : Fin 3 → R) (x : Octonion R) : (↑(upperDerivation u) x).b = u ⬝ᵥ x.w

@[simp]

theorem TauCeti.Octonion.upperDerivation_apply_v {R : Type u_1} [CommRing R] (u : Fin 3 → R) (x : Octonion R) : (↑(upperDerivation u) x).v = (x.a - x.b) • u

@[simp]

theorem TauCeti.Octonion.upperDerivation_apply_w {R : Type u_1} [CommRing R] (u : Fin 3 → R) (x : Octonion R) : (↑(upperDerivation u) x).w = (crossProduct u) x.v

def TauCeti.Octonion.lowerDerivation {R : Type u_1} [CommRing R] : (Fin 3 → R) →ₗ[R] ↥(derivationLieAlgebra R (Octonion R))

The lower vector derivations of 𝕆: the linear map sending t : R³ to the derivation that takes the idempotent ⟨1, 0, 0, 0⟩ to the vector matrix with lower entry t.

Equations

• TauCeti.Octonion.lowerDerivation = { toFun := fun (t : Fin 3 → R) => ⟨TauCeti.Octonion.lowerDerivationEnd✝ t, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.Octonion.lowerDerivation_apply_a {R : Type u_1} [CommRing R] (t : Fin 3 → R) (x : Octonion R) : (↑(lowerDerivation t) x).a = -(t ⬝ᵥ x.v)

@[simp]

theorem TauCeti.Octonion.lowerDerivation_apply_b {R : Type u_1} [CommRing R] (t : Fin 3 → R) (x : Octonion R) : (↑(lowerDerivation t) x).b = t ⬝ᵥ x.v

@[simp]

theorem TauCeti.Octonion.lowerDerivation_apply_v {R : Type u_1} [CommRing R] (t : Fin 3 → R) (x : Octonion R) : (↑(lowerDerivation t) x).v = (crossProduct t) x.w

@[simp]

theorem TauCeti.Octonion.lowerDerivation_apply_w {R : Type u_1} [CommRing R] (t : Fin 3 → R) (x : Octonion R) : (↑(lowerDerivation t) x).w = (x.a - x.b) • t

The brackets of the three families

def TauCeti.Octonion.slOfVectors {R : Type u_1} [CommRing R] (u t : Fin 3 → R) : ↥(LieAlgebra.SpecialLinear.sl (Fin 3) R)

The 𝔰𝔩₃ parameter of the bracket of an upper and a lower vector derivation: the matrix ⟨u, t⟩ • 1 - 3 • u tᵀ, whose trace vanishes because the rank-one matrix u tᵀ has trace ⟨u, t⟩. See TauCeti.Octonion.lie_upperDerivation_lowerDerivation.

Equations

• TauCeti.Octonion.slOfVectors u t = ⟨(u ⬝ᵥ t) • 1 - 3 • Matrix.vecMulVec u t, ⋯⟩

@[simp]

theorem TauCeti.Octonion.coe_slOfVectors {R : Type u_1} [CommRing R] (u t : Fin 3 → R) : ↑(slOfVectors u t) = (u ⬝ᵥ t) • 1 - 3 • Matrix.vecMulVec u t

@[simp]

theorem TauCeti.Octonion.lie_slDerivation_upperDerivation {R : Type u_1} [CommRing R] (M : ↥(LieAlgebra.SpecialLinear.sl (Fin 3) R)) (u : Fin 3 → R) : ⁅slDerivation M, upperDerivation u⁆ = upperDerivation ((↑M).mulVec u)

The upper vector derivations carry the defining representation of 𝔰𝔩₃: ⁅slDerivation M, upperDerivation u⁆ = upperDerivation (M u), the degree 0 piece of the ℤ/3-grading acting on the degree 1 piece.

@[simp]

theorem TauCeti.Octonion.lie_slDerivation_lowerDerivation {R : Type u_1} [CommRing R] (M : ↥(LieAlgebra.SpecialLinear.sl (Fin 3) R)) (t : Fin 3 → R) : ⁅slDerivation M, lowerDerivation t⁆ = lowerDerivation (-(↑M).transpose.mulVec t)

The lower vector derivations carry the dual of the defining representation of 𝔰𝔩₃: ⁅slDerivation M, lowerDerivation t⁆ = lowerDerivation (-(Mᵀ t)), the degree 0 piece of the ℤ/3-grading acting on the degree 2 piece.

@[simp]

theorem TauCeti.Octonion.lie_upperDerivation_upperDerivation {R : Type u_1} [CommRing R] (u u' : Fin 3 → R) : ⁅upperDerivation u, upperDerivation u'⁆ = lowerDerivation (2 • (crossProduct u) u')

Two upper vector derivations bracket into the lower family, by twice the cross product: ⁅upperDerivation u, upperDerivation u'⁆ = lowerDerivation (2 (u ⨯₃ u')). In the ℤ/3-grading this is 1 + 1 = 2.

@[simp]

theorem TauCeti.Octonion.lie_lowerDerivation_lowerDerivation {R : Type u_1} [CommRing R] (t t' : Fin 3 → R) : ⁅lowerDerivation t, lowerDerivation t'⁆ = upperDerivation (2 • (crossProduct t) t')

Two lower vector derivations bracket into the upper family, by twice the cross product: ⁅lowerDerivation t, lowerDerivation t'⁆ = upperDerivation (2 (t ⨯₃ t')). In the ℤ/3-grading this is 2 + 2 = 1.

@[simp]

theorem TauCeti.Octonion.lie_upperDerivation_lowerDerivation {R : Type u_1} [CommRing R] (u t : Fin 3 → R) : ⁅upperDerivation u, lowerDerivation t⁆ = slDerivation (slOfVectors u t)

An upper and a lower vector derivation bracket back into 𝔰𝔩₃: ⁅upperDerivation u, lowerDerivation t⁆ = slDerivation (slOfVectors u t). In the ℤ/3-grading this is 1 + 2 = 0, the bracket that makes the fourteen derivations a Lie subalgebra.

Fourteen independent derivations

def TauCeti.Octonion.derivationOfTriple {R : Type u_1} [CommRing R] : ↥(LieAlgebra.SpecialLinear.sl (Fin 3) R) × (Fin 3 → R) × (Fin 3 → R) →ₗ[R] ↥(derivationLieAlgebra R (Octonion R))

The fourteen-parameter family of derivations of 𝕆: a trace-zero matrix together with an upper and a lower vector. The three summands are TauCeti.Octonion.slDerivation, TauCeti.Octonion.upperDerivation and TauCeti.Octonion.lowerDerivation.

Equations

• TauCeti.Octonion.derivationOfTriple = (↑TauCeti.Octonion.slDerivation).coprod (TauCeti.Octonion.upperDerivation.coprod TauCeti.Octonion.lowerDerivation)

@[simp]

theorem TauCeti.Octonion.derivationOfTriple_apply {R : Type u_1} [CommRing R] (M : ↥(LieAlgebra.SpecialLinear.sl (Fin 3) R)) (u t : Fin 3 → R) : derivationOfTriple (M, u, t) = slDerivation M + (upperDerivation u + lowerDerivation t)

theorem TauCeti.Octonion.derivationOfTriple_injective {R : Type u_1} [CommRing R] : Function.Injective ⇑derivationOfTriple

The fourteen-parameter family is faithful in its parameters. Applying a derivation in the family to the idempotent ⟨1, 0, 0, 0⟩ reads off the upper and the lower vector, and applying it to a vector matrix with upper entry v and nothing else then reads off M v.

Every derivation lies in the fourteen-parameter family

theorem TauCeti.Octonion.derivationOfTriple_surjective {R : Type u_1} [CommRing R] : Function.Surjective ⇑derivationOfTriple

Every derivation of 𝕆 lies in the fourteen-parameter family: a derivation D is slDerivation M + upperDerivation u + lowerDerivation t, where u and t are the upper and lower entries of D ⟨1, 0, 0, 0⟩ and M is the matrix by which D then acts on the upper entries. No hypothesis on the commutative ring R is needed.

noncomputable def TauCeti.Octonion.tripleEquivDerivationLieAlgebra {R : Type u_1} [CommRing R] : (↥(LieAlgebra.SpecialLinear.sl (Fin 3) R) × (Fin 3 → R) × (Fin 3 → R)) ≃ₗ[R] ↥(derivationLieAlgebra R (Octonion R))

The derivations of the split octonions are 𝔰𝔩₃ × R³ × R³, as an R-module: the fourteen-parameter family TauCeti.Octonion.derivationOfTriple is a linear equivalence, over any commutative ring. This is the ℤ/3-graded decomposition G₂ = 𝔰𝔩₃ ⊕ V ⊕ V* of Der 𝕆; its inverse reads the vector parameters off the value at ⟨1, 0, 0, 0⟩ (TauCeti.Octonion.tripleEquivDerivationLieAlgebra_symm_apply_snd_fst and TauCeti.Octonion.tripleEquivDerivationLieAlgebra_symm_apply_snd_snd) and the matrix off the values at the upper vector matrices (TauCeti.Octonion.tripleEquivDerivationLieAlgebra_symm_apply_fst_mulVec).

Equations

• TauCeti.Octonion.tripleEquivDerivationLieAlgebra = LinearEquiv.ofBijective TauCeti.Octonion.derivationOfTriple ⋯

@[simp]

theorem TauCeti.Octonion.tripleEquivDerivationLieAlgebra_apply {R : Type u_1} [CommRing R] (p : ↥(LieAlgebra.SpecialLinear.sl (Fin 3) R) × (Fin 3 → R) × (Fin 3 → R)) : tripleEquivDerivationLieAlgebra p = derivationOfTriple p

@[simp]

theorem TauCeti.Octonion.tripleEquivDerivationLieAlgebra_symm_apply_snd_fst {R : Type u_1} [CommRing R] (D : ↥(derivationLieAlgebra R (Octonion R))) : (tripleEquivDerivationLieAlgebra.symm D).2.1 = (↑D { a := 1, b := 0, v := 0, w := 0 }).v

The upper vector parameter of a derivation is the upper entry of its value at ⟨1, 0, 0, 0⟩.

@[simp]

theorem TauCeti.Octonion.tripleEquivDerivationLieAlgebra_symm_apply_snd_snd {R : Type u_1} [CommRing R] (D : ↥(derivationLieAlgebra R (Octonion R))) : (tripleEquivDerivationLieAlgebra.symm D).2.2 = (↑D { a := 1, b := 0, v := 0, w := 0 }).w

The lower vector parameter of a derivation is the lower entry of its value at ⟨1, 0, 0, 0⟩.

@[simp]

theorem TauCeti.Octonion.tripleEquivDerivationLieAlgebra_symm_apply_fst_mulVec {R : Type u_1} [CommRing R] (D : ↥(derivationLieAlgebra R (Octonion R))) (v : Fin 3 → R) : (↑(tripleEquivDerivationLieAlgebra.symm D).1).mulVec v = (↑D { a := 0, b := 0, v := v, w := 0 }).v

The 𝔰𝔩₃ parameter of a derivation is the matrix by which it acts on the upper vector matrices: M v is the upper entry of D ⟨0, 0, v, 0⟩.

instance TauCeti.Octonion.instFreeSubtypeEndMemLieSubalgebraDerivationLieAlgebra {R : Type u_1} [CommRing R] : Module.Free R ↥(derivationLieAlgebra R (Octonion R))

Der 𝕆 is a free module, being isomorphic to 𝔰𝔩₃ × R³ × R³.

instance TauCeti.Octonion.instFiniteSubtypeEndMemLieSubalgebraDerivationLieAlgebra {R : Type u_1} [CommRing R] : Module.Finite R ↥(derivationLieAlgebra R (Octonion R))

Der 𝕆 is a finite module, being isomorphic to 𝔰𝔩₃ × R³ × R³.

@[simp]

theorem TauCeti.Octonion.finrank_derivationLieAlgebra (R : Type u_2) [CommRing R] [StrongRankCondition R] : Module.finrank R ↥(derivationLieAlgebra R (Octonion R)) = 14

Der 𝕆 has rank 14: eight for 𝔰𝔩₃ and three for each of the two vector families of TauCeti.Octonion.tripleEquivDerivationLieAlgebra. This is the dimension of the exceptional Lie algebra G₂.

instance TauCeti.Octonion.instNontrivialDerivationLieAlgebra {R : Type u_1} [CommRing R] [Nontrivial R] : Nontrivial ↥(derivationLieAlgebra R (Octonion R))

𝕆 has nonzero derivations, so the derivation algebra whose skewness the rest of this file establishes is not the zero Lie algebra. The witness is the upper vector derivation attached to the first basis vector, which sends the idempotent ⟨1, 0, 0, 0⟩ to ⟨0, 0, e₀, 0⟩.