Reduced composition algebras of rank eight (GPR 22.15) #
At an elementary idempotent c, put M = C₂₁. Regularity identifies C₁₂ with M*
through the polar form. Multiplication within the two off-diagonal Peirce components then gives
the associated vector products
M × M → M*, M* × M* → M.
The second linearization of norm multiplicativity is exactly their Binet–Cauchy identity. Thus
the Peirce-coordinate map identifies the algebra with the twisted Zorn vector matrices attached
to this vector-product pair. In constant rank eight the rank count makes M projective of
constant rank three. This is Petersson's converse theorem GPR 22.15, in vector-product-pair
form. GPR 22.15 states it with an orientation θ of M, as C ≅ Zor(M, θ); that form is
Composition/Reduced/OrientedRankEight.lean, which builds from any vector-product pair on a
rank-three module the orientation inducing it.
Main definitions #
ConicAlgebra.IsElementaryIdempotent.peirceVectorProductPair: the vector products read from Peirce multiplication.ConicAlgebra.IsElementaryIdempotent.twistedZorEquiv: the Peirce-coordinate equivalence from the resulting twisted Zorn algebra.
Main results #
ConicAlgebra.IsElementaryIdempotent.isomorphic_twistedZor: the twisted Zorn algebra is isomorphic to the original algebra.ConicAlgebra.IsElementaryIdempotent.rankAtStalk_twistingModule_eq_three: in rank eight the twisting module has constant rank three.
References #
- [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, Exc. 19.35, 22.15.
The lower-left Peirce component used as the twisting module in GPR 22.15.
Equations
Instances For
Multiplication of two elements of the lower-left Peirce component ZornTwistingModule c,
which lands in the upper-right component.
Equations
- hc.lowerProduct = LinearMap.mk₂ k (fun (x y : ↥(ConicAlgebra.IsElementaryIdempotent.ZornTwistingModule c)) => ⟨↑x * ↑y, ⋯⟩) ⋯ ⋯ ⋯ ⋯
Instances For
Multiplication of two elements of the upper-right Peirce component, which lands in
ZornTwistingModule c.
Equations
- hc.upperProduct = LinearMap.mk₂ k (fun (x y : ↥(IsAlternative.peirceComponent c false true)) => ⟨↑x * ↑y, ⋯⟩) ⋯ ⋯ ⋯ ⋯
Instances For
The vector-product pair read from Peirce multiplication. The two products are
multiplication within C₂₁ and C₁₂, transported across polar duality. Their
Binet–Cauchy identity is the second linearization of norm multiplicativity.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The complete Peirce-coordinate multiplication formula. It is the twisted Zorn multiplication formula before naming the two same-component products as vector products.
The Peirce-coordinate map from the twisted Zorn algebra obtained from multiplication back to the original algebra.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Peirce-coordinate map from the associated twisted Zorn algebra is bijective.
The linear equivalence underlying the converse construction of GPR 22.15.
Equations
- hc.twistedZorEquiv hmul hreg = LinearEquiv.ofBijective (hc.twistedZorToPeirce hmul hreg) ⋯
Instances For
The twisted Zorn equivalence preserves the norm.
The twisted Zorn equivalence preserves the identity.
The twisted Zorn equivalence preserves multiplication.
The norm isometry underlying the converse construction of GPR 22.15.
Equations
- hc.twistedZorIsometryEquiv hmul hreg = { toLinearEquiv := hc.twistedZorEquiv hmul hreg, map_app' := ⋯ }
Instances For
The converse construction of GPR 22.15: a regular multiplicative conic algebra with
an elementary idempotent is a twisted Zorn algebra on its lower-left Peirce component.
The rank count in GPR 22.15. At an elementary idempotent in a constant-rank-eight
composition algebra with regular norm, both off-diagonal Peirce components have constant rank
three.
In a reduced composition algebra of constant rank eight, the lower-left Peirce component is
finite projective of constant rank three. The regularity is supplied by GPR 19.11.
GPR 22.15 (Petersson), converse form: a reduced constant-rank-eight composition algebra
is the twisted Zorn algebra whose vector products are its off-diagonal Peirce multiplication.