Twisted Zorn vector matrices (GPR 22.14)

For M a k-module equipped with a pair of associated vector products (Module.VectorProductPair), the twisted Zorn vector matrices are the formal matrices

[ρ₁ u*] [v ρ₂], ρᵢ ∈ k, u* ∈ M*, v ∈ M,

multiplied by GPR (22.14.3)

[ρ₁ v*] [σ₁ w*] [ρ₁σ₁ - ⟨v*, w⟩ ρ₁w* + σ₂v* + v × w] [v ρ₂] [w σ₂] = [σ₁v + ρ₂w + v* × w* ρ₂σ₂ - ⟨w*, v⟩ ],

Its norm is ρ₁ρ₂ + ⟨u*, v⟩ and its trace is ρ₁ + ρ₂. With the usual conjugation, it is the octonion analogue of Conic/../TwistedMatrix.lean: there the off-diagonal entries multiply through the canonical pairing alone, here they also multiply through the two vector products.

GPR 22.14 builds the pair of vector products from an orientation θ : ⋀³ M ≅ k of a projective module of rank three, and calls the result Zor(M, θ). By GPR 22.15 (Petersson) every reduced octonion algebra is one of these, and Zor(M, θ) is split when M is free (GPR asserts only this implication).

What is proved here

• the conic structure, its norm, trace and conjugation — for any k-module M with a vector product pair, and with no hypothesis on 2;
• regularity and non-singularity of the norm for M finitely generated projective, and again not by a computation: the norm is the hyperbolic form of k ⊕ M, pairing (ρ₁, u*) against (ρ₂, v), so the hyperbolic-form API applies with no basis and no rank hypothesis;
• multiplicativity of the norm, which consumes the vector-product axioms exactly: the four orthogonality identities kill four of the nine cross terms and Binet–Cauchy converts the ninth, after which n(xy) - n(x)n(y) is identically zero;
• hence that it is a composition algebra, and a reduced one: the matrix unit e₁₁ of GPR (22.14.7) is an elementary idempotent, so GPR 22.9 applies to it.
• alternativity for M finitely generated projective: regularity makes the radical zero, so Kirmse's theorem applies to the multiplicative conic algebra, without a hypothesis on 2.

Combined with Module.VectorProductPair.ofBasis, this produces a composition algebra of rank eight over any commutative ring out of any free module of rank three — the split case, and the case GPR 22.14's localization argument reduces to. The coordinate isomorphism isomorphic_twistedZor_ofBasis proves that this free case is exactly Zor(k) from GPR 21.18.

Main definitions

• ConicAlgebra.TwistedZor P : the module of twisted Zorn vector matrices, with its multiplication.
• ConicAlgebra.twistedZorNorm P, ConicAlgebra.twistedZor P : the norm and the conic structure.

Main results

• ConicAlgebra.isGPRNonsingular_twistedZorNorm : the norm is hyperbolic, hence non-singular.
• ConicAlgebra.isMultiplicative_twistedZor : the norm permits composition.
• ConicAlgebra.isAlternative_twistedZor : the algebra is alternative for M finitely generated projective.
• ConicAlgebra.isComposition_twistedZor : it is a composition algebra.
• ConicAlgebra.hasElementaryIdempotent_twistedZor : it is reduced.
• ConicAlgebra.isomorphic_twistedZor_ofBasis : a pair built from a basis gives the split Zorn algebra.
• ConicAlgebra.instIsAlternativeTwistedZorOfBasis : the basis-built algebra is alternative.
• ConicAlgebra.isSplitOfRank_twistedZor_ofBasis : the basis-built algebra is split of rank eight.

Implementation notes

⚠ The sign of the norm. GPR (22.14.4) prints n = ρ₁ρ₂ - ⟨u*, v⟩, but the norm of these algebras is ρ₁ρ₂ + ⟨u*, v⟩, which is used here. The two cannot both be right: the multiplication GPR (22.14.3) specializes, for M = k³ with the standard orientation, to the multiplication GPR (21.18.4) of ordinary Zorn vector matrices, whose norm is ρ₁ρ₂ + u₁ᵀu₂ by GPR (21.18.6) — the sign difference from the quaternion case GPR (22.12.1) is already present in GPR, and comes from the diagonal entries of (22.14.3) carrying a minus sign where those of (22.12.1) carry a plus. The + sign is also what the Peirce norm formula ConicAlgebra.IsElementaryIdempotent.norm_peirceElement gives, under the identification of C₁₂ with M* by the positive polar duality that GPR 22.15's own proof uses.

The multiplication is not the componentwise one, so TwistedZor is a type synonym; it is indexed by the vector product pair P, not merely by M, because the multiplication depends on P. This is the same device as ConicAlgebra.Cay, which is indexed by the conic structure and the scalar.

Orientation and converse

Composition/Reduced/Orientation.lean constructs the pair from an orientation of a constant-rank-three finite projective module over any commutative ring, by the unbased local exterior-power duality argument in GPR 21.7. The converse GPR 22.15 is proved in Composition/Reduced/RankEight.lean.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 21.18, 22.9, 22.12, 22.14, 22.15.

def ConicAlgebra.TwistedZor {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (_P : Module.VectorProductPair k M) : Type (max u v)

The k-module of twisted Zorn vector matrices attached to a vector product pair (GPR 22.14), as a type synonym for (k × M*) × (k × M): the element x is the matrix

[x.1.1 x.1.2] [x.2.2 x.2.1]

whose top row is x.1 = (ρ₁, u*) and whose bottom row is (x.2.2, x.2.1) = (v, ρ₂). The grouping puts the two diagonal entries first in their pairs, so that the norm is visibly the pairing of x.1 against x.2.

Equations

• ConicAlgebra.TwistedZor _P = ((k × Module.Dual k M) × k × M)

@[instance_reducible]

instance ConicAlgebra.TwistedZor.instAddCommGroup {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : Module.VectorProductPair k M) : AddCommGroup (TwistedZor P)

Equations

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

@[instance_reducible]

instance ConicAlgebra.TwistedZor.instModule {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : Module.VectorProductPair k M) : Module k (TwistedZor P)

Equations

• ConicAlgebra.TwistedZor.instModule P = { smul := ConicAlgebra.TwistedZor.instModule._aux_1 P, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

instance ConicAlgebra.TwistedZor.instFiniteOfProjective {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : Module.VectorProductPair k M) [Module.Finite k M] [Module.Projective k M] : Module.Finite k (TwistedZor P)

instance ConicAlgebra.TwistedZor.instProjectiveOfFinite {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : Module.VectorProductPair k M) [Module.Finite k M] [Module.Projective k M] : Module.Projective k (TwistedZor P)

theorem ConicAlgebra.TwistedZor.ext {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} {x y : TwistedZor P} (h₁ : x.1.1 = y.1.1) (h₂ : x.1.2 = y.1.2) (h₃ : x.2.1 = y.2.1) (h₄ : x.2.2 = y.2.2) : x = y

Two twisted Zorn vector matrices agree as soon as their four entries do.

@[simp]

theorem ConicAlgebra.TwistedZor.fst_zero {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} : 0.1 = 0

@[simp]

theorem ConicAlgebra.TwistedZor.snd_zero {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} : 0.2 = 0

@[simp]

theorem ConicAlgebra.TwistedZor.fst_add {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} (x y : TwistedZor P) : (x + y).1 = x.1 + y.1

@[simp]

theorem ConicAlgebra.TwistedZor.snd_add {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} (x y : TwistedZor P) : (x + y).2 = x.2 + y.2

@[simp]

theorem ConicAlgebra.TwistedZor.fst_neg {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} (x : TwistedZor P) : (-x).1 = -x.1

@[simp]

theorem ConicAlgebra.TwistedZor.snd_neg {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} (x : TwistedZor P) : (-x).2 = -x.2

@[simp]

theorem ConicAlgebra.TwistedZor.fst_sub {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} (x y : TwistedZor P) : (x - y).1 = x.1 - y.1

@[simp]

theorem ConicAlgebra.TwistedZor.snd_sub {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} (x y : TwistedZor P) : (x - y).2 = x.2 - y.2

@[simp]

theorem ConicAlgebra.TwistedZor.fst_smul {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} (c : k) (x : TwistedZor P) : (c • x).1 = c • x.1

@[simp]

theorem ConicAlgebra.TwistedZor.snd_smul {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} (c : k) (x : TwistedZor P) : (c • x).2 = c • x.2

@[instance_reducible]

instance ConicAlgebra.TwistedZor.instMul {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : Module.VectorProductPair k M) : Mul (TwistedZor P)

Multiplication of twisted Zorn vector matrices, GPR (22.14.3): the entries of M* and of M multiply through the canonical pairing on the diagonal and through the two vector products off it.

Equations

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

@[instance_reducible]

instance ConicAlgebra.TwistedZor.instOne {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : Module.VectorProductPair k M) : One (TwistedZor P)

The identity matrix.

Equations

• ConicAlgebra.TwistedZor.instOne P = { one := ((1, 0), 1, 0) }

@[simp]

theorem ConicAlgebra.TwistedZor.mul_fst_fst {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} (x y : TwistedZor P) : (x * y).1.1 = x.1.1 * y.1.1 - x.1.2 y.2.2

@[simp]

theorem ConicAlgebra.TwistedZor.mul_fst_snd {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} (x y : TwistedZor P) : (x * y).1.2 = x.1.1 • y.1.2 + y.2.1 • x.1.2 + (P.cross x.2.2) y.2.2

@[simp]

theorem ConicAlgebra.TwistedZor.mul_snd_fst {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} (x y : TwistedZor P) : (x * y).2.1 = x.2.1 * y.2.1 - y.1.2 x.2.2

@[simp]

theorem ConicAlgebra.TwistedZor.mul_snd_snd {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} (x y : TwistedZor P) : (x * y).2.2 = y.1.1 • x.2.2 + x.2.1 • y.2.2 + (P.crossDual x.1.2) y.1.2

@[simp]

theorem ConicAlgebra.TwistedZor.one_fst_fst {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} : 1.1.1 = 1

@[simp]

theorem ConicAlgebra.TwistedZor.one_fst_snd {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} : 1.1.2 = 0

@[simp]

theorem ConicAlgebra.TwistedZor.one_snd_fst {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} : 1.2.1 = 1

@[simp]

theorem ConicAlgebra.TwistedZor.one_snd_snd {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} : 1.2.2 = 0

@[instance_reducible]

instance ConicAlgebra.TwistedZor.instNonAssocRing {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : Module.VectorProductPair k M) : NonAssocRing (TwistedZor P)

Equations

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

instance ConicAlgebra.TwistedZor.instSMulCommClass {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : Module.VectorProductPair k M) : SMulCommClass k (TwistedZor P) (TwistedZor P)

instance ConicAlgebra.TwistedZor.instIsScalarTower {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : Module.VectorProductPair k M) : IsScalarTower k (TwistedZor P) (TwistedZor P)

The norm

n = ρ₁ρ₂ + ⟨u*, v⟩ pairs the top row against the bottom row, with the bottom row read in k ⊕ M and the top row in its dual. That is what makes it hyperbolic, and it is why no rank hypothesis and no basis is needed for non-singularity.

def ConicAlgebra.twistedZorDualProdEquiv {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : Module.VectorProductPair k M) : TwistedZor P ≃ₗ[k] Module.Dual k (k × M) × k × M

The linear equivalence presenting a twisted Zorn vector matrix as an element of (k ⊕ M)* ⊕ (k ⊕ M), under which the norm becomes the hyperbolic form QuadraticForm.dualProd k (k × M). The sign on the dual coordinate compensates the one built into ConicAlgebra.dualProdEquiv, which was chosen for the quaternion norm ρ₁ρ₂ - ⟨u*, v⟩ of GPR (22.12.1).

Equations

• ConicAlgebra.twistedZorDualProdEquiv P = (((LinearEquiv.refl k k).prodCongr (LinearEquiv.neg k)).trans (ConicAlgebra.dualProdEquiv k M)).prodCongr (LinearEquiv.refl k (k × M))

@[simp]

theorem ConicAlgebra.twistedZorDualProdEquiv_apply {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : Module.VectorProductPair k M) (x : TwistedZor P) : (twistedZorDualProdEquiv P) x = ((dualProdEquiv k M) (x.1.1, -x.1.2), x.2)

def ConicAlgebra.twistedZorNorm {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : Module.VectorProductPair k M) : QuadraticForm k (TwistedZor P)

The norm of a twisted Zorn vector matrix, GPR (22.14.4): n = ρ₁ρ₂ + ⟨u*, v⟩.

⚠ GPR (22.14.4) prints a minus sign; see the module docstring for why it must be a plus.

Equations

• ConicAlgebra.twistedZorNorm P = QuadraticMap.comp (QuadraticForm.dualProd k (k × M)) ↑(ConicAlgebra.twistedZorDualProdEquiv P)

@[simp]

theorem ConicAlgebra.twistedZorNorm_apply {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} (x : TwistedZor P) : (twistedZorNorm P) x = x.1.1 * x.2.1 + x.1.2 x.2.2

theorem ConicAlgebra.polar_twistedZorNorm {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} (x y : TwistedZor P) : QuadraticMap.polar (⇑(twistedZorNorm P)) x y = x.1.1 * y.2.1 + y.1.1 * x.2.1 + x.1.2 y.2.2 + y.1.2 x.2.2

@[simp]

theorem ConicAlgebra.polar_twistedZorNorm_one {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} (x : TwistedZor P) : QuadraticMap.polar (⇑(twistedZorNorm P)) 1 x = x.1.1 + x.2.1

def ConicAlgebra.twistedZor {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : Module.VectorProductPair k M) : ConicAlgebra k (TwistedZor P)

GPR 22.14: the twisted Zorn vector matrices form a conic algebra, with norm ρ₁ρ₂ + ⟨u*, v⟩ and trace ρ₁ + ρ₂. The degree-two identity uses only that the two products are alternating; no other axiom, no hypothesis on M, and none on 2.

Equations

• ConicAlgebra.twistedZor P = { norm := ConicAlgebra.twistedZorNorm P, norm_one := ⋯, mul_self := ⋯ }

@[simp]

theorem ConicAlgebra.twistedZor_norm {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} : (twistedZor P).norm = twistedZorNorm P

@[simp]

theorem ConicAlgebra.trace_twistedZor_apply {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} (x : TwistedZor P) : (twistedZor P).trace x = x.1.1 + x.2.1

The trace of a twisted Zorn vector matrix is the trace of the matrix, GPR (22.14.5).

@[simp]

theorem ConicAlgebra.conj_twistedZor_apply {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} (x : TwistedZor P) : (twistedZor P).conj x = ((x.2.1, -x.1.2), x.1.1, -x.2.2)

The conjugation exchanges the diagonal entries and negates the off-diagonal ones, GPR (22.14.6).

Non-singularity, multiplicativity, and the composition algebra

theorem ConicAlgebra.isGPRNonsingular_twistedZorNorm {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : Module.VectorProductPair k M) [Module.Finite k M] [Module.Projective k M] : (twistedZorNorm P).IsGPRNonsingular

The norm of the twisted Zorn vector matrices is non-singular for M finitely generated projective: it is the hyperbolic form of k ⊕ M. No rank hypothesis and no hypothesis on 2.

theorem ConicAlgebra.isGPRRegular_twistedZorNorm {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : Module.VectorProductPair k M) [Module.Finite k M] [Module.Projective k M] : (twistedZorNorm P).IsGPRRegular

The norm of the twisted Zorn vector matrices is regular for M finitely generated projective: it is the hyperbolic form of k ⊕ M, transported along a linear equivalence. This is stronger than the non-singularity needed for composition and requires no hypothesis on 2.

theorem ConicAlgebra.isGPRNondegenerate_twistedZorNorm {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : Module.VectorProductPair k M) [Module.Finite k M] [Module.Projective k M] : (twistedZorNorm P).IsGPRNondegenerate

The twisted Zorn norm has zero radical when M is finitely generated projective.

theorem ConicAlgebra.isMultiplicative_twistedZor {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} : (twistedZor P).IsMultiplicative

The norm of the twisted Zorn vector matrices permits composition, n(xy) = n(x)n(y).

This is where the vector-product axioms are consumed, and they are consumed exactly: of the nine terms of the off-diagonal pairing, four vanish by orthogonality of a product to its own arguments and one is ⟨v × w, v* × w*⟩, which Binet–Cauchy turns into the two remaining products of pairings; what is left cancels identically. No hypothesis on M.

theorem ConicAlgebra.isAlternative_twistedZor {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} [Module.Finite k M] [Module.Projective k M] : IsAlternative (TwistedZor P)

GPR 22.14: twisted Zorn vector matrices are alternative when M is finitely generated projective. The hyperbolic norm is regular, hence has zero radical, so Kirmse's theorem applies to the multiplicative conic structure. No hypothesis on 2 and no direct Grassmann-identity calculation is needed.

theorem ConicAlgebra.isComposition_twistedZor {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] {P : Module.VectorProductPair k M} [Module.Finite k M] [Module.Projective k M] : (twistedZor P).IsComposition

The twisted Zorn vector matrices form a composition algebra, for M finitely generated projective carrying a vector product pair. With Module.VectorProductPair.ofBasis this gives a composition algebra of rank eight over any commutative ring, with no hypothesis on 2; by GPR 22.14 it is Zor(M, θ) whenever the pair comes from an orientation of a rank-three module.

theorem ConicAlgebra.hasElementaryIdempotent_twistedZor {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : Module.VectorProductPair k M) : (twistedZor P).HasElementaryIdempotent

The twisted Zorn vector matrices are reduced. The matrix unit e₁₁ of GPR (22.14.7) has norm 0 and trace 1, so it is an elementary idempotent and GPR 22.9 applies: the norm is isotropic and the algebra contains a split quadratic étale subalgebra. No hypothesis on M.

The free case

When the vector product pair comes from a basis of M, reading the two off-diagonal entries in the coordinates of that basis and its dual identifies the twisted construction with Zor(k). Thus Module.VectorProductPair.ofBasis produces exactly the split octonion algebra, independently of the chosen basis.

noncomputable def ConicAlgebra.twistedZorOfBasisEquiv {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Module.Basis (Fin 3) k M) : TwistedZor (Module.VectorProductPair.ofBasis b) ≃ₗ[k] Zor k

The coordinate equivalence from the twisted Zorn algebra attached to a basis to the split Zorn algebra. The lower-left entry uses the coordinates of b, while the upper-right entry uses the coordinates of the dual basis.

Equations

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

@[simp]

theorem ConicAlgebra.twistedZorOfBasisEquiv_apply {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Module.Basis (Fin 3) k M) (x : TwistedZor (Module.VectorProductPair.ofBasis b)) : (twistedZorOfBasisEquiv b) x = ((x.1.1, b.equivFun x.2.2), x.2.1, b.dualCoord x.1.2)

theorem ConicAlgebra.zorNorm_twistedZorOfBasisEquiv {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Module.Basis (Fin 3) k M) (x : TwistedZor (Module.VectorProductPair.ofBasis b)) : (zorNorm k) ((twistedZorOfBasisEquiv b) x) = (twistedZorNorm (Module.VectorProductPair.ofBasis b)) x

The coordinate equivalence preserves the norm.

theorem ConicAlgebra.twistedZorOfBasisEquiv_one {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Module.Basis (Fin 3) k M) : (twistedZorOfBasisEquiv b) 1 = 1

The coordinate equivalence preserves the identity matrix.

theorem ConicAlgebra.twistedZorOfBasisEquiv_mul {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Module.Basis (Fin 3) k M) (x y : TwistedZor (Module.VectorProductPair.ofBasis b)) : (twistedZorOfBasisEquiv b) (x * y) = (twistedZorOfBasisEquiv b) x * (twistedZorOfBasisEquiv b) y

The coordinate equivalence preserves multiplication.

noncomputable def ConicAlgebra.twistedZorOfBasisIsometryEquiv {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Module.Basis (Fin 3) k M) : QuadraticMap.IsometryEquiv (twistedZor (Module.VectorProductPair.ofBasis b)).norm (zor k).norm

The norm isometry from the basis-built twisted Zorn algebra to the split Zorn algebra.

Equations

• ConicAlgebra.twistedZorOfBasisIsometryEquiv b = { toLinearEquiv := ConicAlgebra.twistedZorOfBasisEquiv b, map_app' := ⋯ }

theorem ConicAlgebra.isomorphic_twistedZor_ofBasis {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Module.Basis (Fin 3) k M) : (twistedZor (Module.VectorProductPair.ofBasis b)).Isomorphic (zor k)

The free case of GPR 22.14: a twisted Zorn algebra whose vector products come from a basis is isomorphic to the split Zorn algebra Zor(k) of GPR 21.18.

theorem ConicAlgebra.isomorphic_twistedZor_of_exists_basis {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : Module.VectorProductPair k M) (b : Module.Basis (Fin 3) k M) : (twistedZor P).Isomorphic (zor k)

Any twisted Zorn algebra on a module admitting a basis of size three is split. Binet–Cauchy forces its vector-product pair to be the pair attached to a suitably rescaled basis.

theorem ConicAlgebra.isSplitOfRank_twistedZor_of_exists_basis {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (P : Module.VectorProductPair k M) (b : Module.Basis (Fin 3) k M) : (twistedZor P).IsSplitOfRank 8

Any twisted Zorn algebra on a module admitting a basis of size three satisfies the rank-eight splitness clause of GPR 21.19(d).

instance ConicAlgebra.instIsAlternativeTwistedZorOfBasis {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Module.Basis (Fin 3) k M) : IsAlternative (TwistedZor (Module.VectorProductPair.ofBasis b))

A basis-built twisted Zorn algebra is alternative, because its coordinate equivalence identifies its multiplication with that of the alternative algebra Zor(k). This proves the free case of the alternativity assertion in GPR 22.14 without any hypothesis on 2.

@[simp]

theorem ConicAlgebra.finrank_twistedZor_ofBasis {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Module.Basis (Fin 3) k M) [Nontrivial k] : Module.finrank k (TwistedZor (Module.VectorProductPair.ofBasis b)) = 8

A basis-built twisted Zorn algebra has rank eight.

theorem ConicAlgebra.isSplitOfRank_twistedZor_ofBasis {k : Type u} {M : Type v} [CommRing k] [AddCommGroup M] [Module k M] (b : Module.Basis (Fin 3) k M) : (twistedZor (Module.VectorProductPair.ofBasis b)).IsSplitOfRank 8

The basis-built twisted Zorn algebra satisfies the rank-eight splitness clause of GPR 21.19(d).