Doubling inside an ambient conic algebra (GPR 18.1) #
Let A be a conic alternative algebra, B ⊆ A a unital subalgebra, and v ∈ A an element
orthogonal to B — n(b, v) = 0 for every b ∈ B — whose norm is a unit. Then the three
identities
x(yv) = (yx)v, (xv)y = (x (conj y))v, (xv)(yv) = -n(v) ((conj y) x) (x, y ∈ B)
hold. They are exactly the three clauses of the Cayley–Dickson multiplication
(u₁ + v₁j)(u₂ + v₂j) = (u₁u₂ + μ (conj v₂)v₁) + (v₂u₁ + v₁(conj u₂)) j with μ = -n(v), so
B + Bv is a copy of Cay(B, μ) sitting inside A. Conic/CayleyDickson.lean builds Cay(B, μ)
externally; this file is the internal counterpart, and the comparison between the two is
ConicAlgebra.cayToAlgebra.
The mechanism #
Everything rests on one unconditional observation. The linearized degree-two identity
xy + yx = t(x)y + t(y)x - n(x,y)·1 (ConicAlgebra.mul_add_mul, valid in every conic algebra)
collapses, for x ∈ B and v ⊥ B, to
xv = v (conj x), vx = (conj x) v
(ConicAlgebra.mul_eq_mul_conj, ConicAlgebra.mul_eq_conj_mul): orthogonality to B turns
multiplication by v into a twisted commutation rule. Note 1 ∈ B, so t(v) = n(1, v) = 0 and
hence conj v = -v and v² = -n(v)·1.
Given that rule, the three identities follow from the alternative laws alone — the alternating
property of the associator, the middle Moufang identity (ab)(ca) = a(bc)a, and flexibility —
together with n(v) being a unit, which lets right multiplication by v be cancelled:
(zv)v = -n(v)z.
Why no regularity hypothesis #
GPR 19.3 produces alternativity of a composition algebra from the vanishing of the radical of
its norm, which over a general commutative ring is not implied by non-singularity (see
Composition/Basic.lean). Alternativity is therefore assumed here rather than derived, as an honest
hypothesis on a conic algebra. For a composition algebra it is automatic over every commutative ring
(ConicAlgebra.IsComposition.isAlternative_general, Composition/Alternative.lean, which this
layer may not import).
What is not assumed is any regularity of the norm — not on A, not on B. The three identities
below are cancellation statements proved by multiplying by v and using n(v) ∈ kˣ, so no
non-degeneracy of the ambient norm is used anywhere. Nor is B assumed associative, nor
multiplicativity of the norm; those enter only when the norm of the doubled algebra is computed.
Main definitions #
ConicAlgebra.cayToAlgebra: the mapCay(B, -n(v)) → A,u + wj ↦ u + wv.
Main results #
ConicAlgebra.mul_eq_mul_conj,ConicAlgebra.mul_eq_conj_mul: the commutation rulexv = v (conj x),vx = (conj x) vforx ∈ B, in any conic algebra whatsoever.ConicAlgebra.mul_mul_orthogonal:x(yv) = (yx)v,GPR 18.1(1).ConicAlgebra.mul_orthogonal_mul:(xv)y = (x (conj y))v,GPR 18.1(2).ConicAlgebra.mul_orthogonal_mul_mul_orthogonal:(xv)(yv) = -n(v)((conj y)x),GPR 18.1(3).ConicAlgebra.cayToAlgebra_mul:GPR 18.1— the doubling map is multiplicative, soB + Bvis a copy ofCay(B, -n(v))insideA.ConicAlgebra.norm_cayToAlgebra: it is an isometry for the Cayley–Dickson norm. This is where multiplicativity ofnis used, throughB ⊥ Bv.ConicAlgebra.cayToAlgebra_injective: it is injective whenn|_Bis regular.
References #
- [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 18.1, 18.3.
An element of trace zero #
An element of trace zero is the negative of its conjugate.
The degree-two identity for an element of trace zero: v² = -n(v)·1.
Right multiplication by v squares to -n(v): (zv)v = -n(v)·z, for v of trace zero
and any z. This is the cancellation device of the whole file; it consumes right alternativity
and nothing else.
Cancelling v. If n(v) is a unit then right multiplication by v is injective, so an
element killed by v is zero.
An element orthogonal to a subalgebra #
A unital subalgebra is closed under conjugation, since conj b = t(b)·1 - b.
An element orthogonal to a unital subalgebra has trace zero: the unit lies in the
subalgebra, and t(v) = n(1, v).
The commutation rule, first form: xv = v (conj x) for x ∈ B and v ⊥ B.
This holds in every conic algebra — no alternativity, no regularity, no hypothesis on 2. It is
the linearized degree-two identity xy + yx = t(x)y + t(y)x - n(x,y)·1 with y = v, where both
t(v) and n(x, v) vanish.
The commutation rule, second form: vx = (conj x) v for x ∈ B and v ⊥ B.
Conjugating by v: (vc)v = -n(v) (conj c) for c ∈ B.
(xv)(vy) = -n(v)(yx) for x, y ∈ B.
The two commutation rules put the product in the shape (vb)(cv) of the middle Moufang identity
(ab)(ca) = a(bc)a, and flexibility then turns v(bc)v into a single conjugation by v.
GPR 18.1(3): (xv)(yv) = -n(v)((conj y)x) for x, y ∈ B.
This is the first component of the Cayley–Dickson product (0 + v₁j)(0 + v₂j) = μ (conj v₂)v₁, with
μ = -n(v).
GPR 18.1(1): x(yv) = (yx)v for x, y ∈ B.
Both sides are cancelled against v on the right: ((yx)v)v = -n(v)(yx) at once, while
(x(yv))v is unwound by moving the associator ⁅x, yv, v⁆ around its cyclic orbit to
⁅yv, v, x⁆, whose two terms are -n(v)(yx) and -n(v)(xy). The xy terms cancel.
GPR 18.1(2): (xv)y = (x (conj y))v for x, y ∈ B.
Conjugating GPR 18.1(1) at the pair (conj y, x) turns it into this, because conjugation is an
anti-homomorphism and negates every element of Bv.
The comparison with the external double #
The internal doubling map Cay(B, -n(v)) → A, u + wj ↦ u + wv (GPR 18.1).
It is defined for every v, with no orthogonality or invertibility hypothesis; those are what make
it multiplicative (ConicAlgebra.cayToAlgebra_mul) and injective
(ConicAlgebra.cayToAlgebra_injective). The Cayley–Dickson scalar is forced to be -n(v), which
is GPR 18.1's μ.
Equations
Instances For
The internal doubling map is unital.
B ⊥ Bv. Norm-associativity moves the v across the polar form, where orthogonality to B
kills it: n(b, wv) = n((conj w)b, v) = 0. This is what makes the internal doubling map an isometry
onto its image, and needs the norm to be multiplicative.
The internal doubling map is an isometry: it carries the Cayley–Dickson norm
n_B ⊥ ⟨n(v)⟩ n_B to the ambient norm. This is GPR 18.1's norm formula, and it uses
multiplicativity (for n(wv) = n(w)n(v)) and B ⊥ Bv.
The polar form of the Cayley–Dickson norm is the ambient polar form, pulled back.
GPR 18.1. The internal doubling map is multiplicative: B + Bv really is a copy of
Cay(B, -n(v)) inside A.
The three components of the Cayley–Dickson product are the three identities of this file, and
μ = -n(v) is forced by the last of them.
The internal doubling map is injective, as soon as the radical of the restricted norm
vanishes and n(v) is a unit.
The map is an isometry, so its kernel lands in the radical of the Cayley–Dickson norm
n_B ⊥ ⟨n(v)⟩ n_B, which vanishes by GN (C.8.3): the first summand has injective polar form and
rescaling by a unit does not change a radical.
⚠ Regularity of n|_B — not merely a vanishing radical — is what GN (C.8.3) consumes, and the
asymmetry is real: in characteristic 2 the non-singular form ⟨1⟩ doubles to ⟨1⟩ ⊥ ⟨1⟩, whose
radical is nonzero. This is the same hypothesis ConicAlgebra.IsComposition.cay carries on the
constructive side.