Multiplicative conic algebras and norm-associativity

A conic algebra is multiplicative (GPR 19.1; the older literature says its norm permits composition) if n(xy) = n(x) n(y) for all x, y. This is the second half of the definition of a composition algebra (GPR 19.5, Layer 7), the first half being a regularity condition on the norm.

The point of this file is that multiplicativity is much stronger than it looks: linearizing it twice turns the quadratic statement n(xy) = n(x)n(y) into a bilinear one, and that bilinear identity is exactly GPR's norm-associativity

n(xy, z) = n(y, (conj x)z), n(xy, z) = n(x, z(conj y)),

which is the workhorse of the whole composition-algebra theory. Everything here holds in an arbitrary conic algebra over an arbitrary commutative ring: no alternativity, no regularity, no projectivity, and nothing on 2. Only additivity of the norm's polar form is used.

Main definitions

• ConicAlgebra.IsMultiplicative : n(xy) = n(x) n(y).
• ConicAlgebra.HasTwoSidedInverses : every nonzero element has a two-sided multiplicative inverse. ⚠ This is weaker than being a division algebra in the sense of GPR 8.6; see its docstring.

Main results

• QuadraticForm.polar_mul_mul_right_of_map_mul, QuadraticForm.polar_mul_mul_left_of_map_mul, QuadraticForm.polar_mul_add_polar_mul_of_map_mul : the linearizations GPR (19.1.3)–(19.1.5) for any quadratic form permitting composition on a non-associative ring, with no conic structure.
• ConicAlgebra.IsMultiplicative.polar_mul_mul_right, ConicAlgebra.IsMultiplicative.polar_mul_mul_left : the first linearization, in either variable, n(xz, yz) = n(x, y) n(z) and n(xy, xz) = n(x) n(y, z).
• ConicAlgebra.IsMultiplicative.polar_mul_add_polar_mul : the second linearization, n(xz, yw) + n(xw, yz) = n(x, y) n(z, w).
• ConicAlgebra.IsMultiplicative.polar_mul_left : norm-associativity, n(xy, z) = n(y, (conj x)z).
• ConicAlgebra.IsMultiplicative.polar_mul_right : norm-associativity on the other side, n(xy, z) = n(x, z(conj y)).
• ConicAlgebra.IsMultiplicative.trace_mul : t(xy) = t(x)t(y) - n(x, y).
• ConicAlgebra.IsMultiplicative.anisotropic_iff_noZeroDivisors_of_isDomain : over a domain, the norm is anisotropic exactly when the algebra has no zero divisors.
• ConicAlgebra.isMultiplicative_baseRing : the base ring, with norm the squaring map, is multiplicative.

Implementation notes

n(x, y) above is QuadraticMap.polar C.norm x y, the un-halved polar form (overview §6(a)); the two linearizations below are obtained by additivity alone, so every statement here is valid in characteristic 2.

The two norm-associativity identities are genuinely two statements, not one applied to the opposite algebra: A is not assumed associative, commutative or alternative, so there is no symmetry to exploit. They are proved the same way, by specializing the second linearization at y = 1 and at w = 1 respectively.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 16.5, 16.12--16.13, 19.1, 22.18.

Quadratic forms permitting composition

theorem QuadraticForm.polar_mul_mul_right_of_map_mul {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {Q : QuadraticForm k A} (hmul : ∀ (x y : A), Q (x * y) = Q x * Q y) (x y z : A) : QuadraticMap.polar (⇑Q) (x * z) (y * z) = QuadraticMap.polar (⇑Q) x y * Q z

GPR (19.1.4): a quadratic form permitting composition satisfies n(xz, yz) = n(x, y) n(z). Only right distributivity is used; compare ConicAlgebra.IsMultiplicative.polar_mul_mul_right, the same identity for a conic norm.

theorem QuadraticForm.polar_mul_mul_left_of_map_mul {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {Q : QuadraticForm k A} (hmul : ∀ (x y : A), Q (x * y) = Q x * Q y) (x y z : A) : QuadraticMap.polar (⇑Q) (x * y) (x * z) = Q x * QuadraticMap.polar (⇑Q) y z

GPR (19.1.3): a quadratic form permitting composition satisfies n(xy, xz) = n(x) n(y, z). Only left distributivity is used; compare ConicAlgebra.IsMultiplicative.polar_mul_mul_left.

theorem QuadraticForm.polar_mul_add_polar_mul_of_map_mul {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {Q : QuadraticForm k A} (hmul : ∀ (x y : A), Q (x * y) = Q x * Q y) (x y z w : A) : QuadraticMap.polar (⇑Q) (x * z) (y * w) + QuadraticMap.polar (⇑Q) (x * w) (y * z) = QuadraticMap.polar (⇑Q) x y * QuadraticMap.polar (⇑Q) z w

GPR (19.1.5): a quadratic form permitting composition satisfies n(xz, yw) + n(xw, yz) = n(x, y) n(z, w). This is GPR's n(xy, wz) + n(wy, xz) = n(x, w) n(y, z) with the variables renamed, in the shape of ConicAlgebra.IsMultiplicative.polar_mul_add_polar_mul; it is (19.1.4) linearized in z.

def ConicAlgebra.IsMultiplicative {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (C : ConicAlgebra k A) : Prop

A conic algebra is multiplicative (GPR 19.1) if its norm permits composition: n(xy) = n(x) n(y).

This is a property of the pair (A, n), not of A alone — the norm is data — so it is a predicate on C : ConicAlgebra k A rather than a typeclass on A. It carries no regularity and no projectivity: those are separate axes (overview §2), and a composition algebra (GPR 19.5) is a conic algebra having all three.

Equations

• C.IsMultiplicative = ∀ (x y : A), C.norm (x * y) = C.norm x * C.norm y

def ConicAlgebra.HasTwoSidedInverses {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (_C : ConicAlgebra k A) : Prop

Every nonzero element has a two-sided inverse: for each x ≠ 0 there is y with x * y = 1 and y * x = 1.

⚠ This property is weaker than being a division algebra as defined in GPR 8.6, and is deliberately not called IsDivision. GPR 8.6 calls A a division algebra when A ≠ 0 and, for every u ≠ 0, the left and right multiplications L_u and R_u are bijective. Without associativity a two-sided inverse does not give that: the real sedenions have an anisotropic norm, so every nonzero x has the two-sided inverse n(x)⁻¹ (conj x), yet they are not a division algebra (GPR Exc. 19.29(e)). For a unital alternative algebra the two notions agree, given 1 ≠ 0 (GPR 13.8); in particular they agree for composition algebras, which are alternative. Both facts are formalized in Conic/Division.lean and Composition/Sedenion.lean: ConicAlgebra.isDivision_iff_hasTwoSidedInverses is GPR 13.8 for alternative conic algebras over a field, and ConicAlgebra.hasTwoSidedInverses_realSedenion with ConicAlgebra.not_isDivision_realSedenion is the sedenion example. Theorems stated with HasTwoSidedInverses are about this weaker property; the classification theorems over a field are also stated with IsDivision.

The property depends only on the multiplication, but is placed in the conic-algebra namespace because it is used here in the classification of composition algebras. It does not assert associativity.

Equations

• _C.HasTwoSidedInverses = ∀ {x : A}, x ≠ 0 → ∃ (y : A), x * y = 1 ∧ y * x = 1

theorem ConicAlgebra.IsMultiplicative.norm_mul {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {C : ConicAlgebra k A} (h : C.IsMultiplicative) (x y : A) : C.norm (x * y) = C.norm x * C.norm y

Multiplicativity of the norm, as a rewrite rule. ConicAlgebra.IsMultiplicative is a def, so it has to be unfolded before rw/simp can use it.

theorem ConicAlgebra.IsMultiplicative.polar_mul_mul_right {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {C : ConicAlgebra k A} (h : C.IsMultiplicative) (x y z : A) : QuadraticMap.polar (⇑C.norm) (x * z) (y * z) = QuadraticMap.polar (⇑C.norm) x y * C.norm z

First linearization of multiplicativity, in the left variable: n(xz, yz) = n(x, y) n(z).

Obtained from n((x + y)z) = n(x + y) n(z) by subtracting n(xz) = n(x)n(z) and n(yz) = n(y)n(z); only right distributivity and additivity are used.

theorem ConicAlgebra.IsMultiplicative.polar_mul_mul_left {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {C : ConicAlgebra k A} (h : C.IsMultiplicative) (x y z : A) : QuadraticMap.polar (⇑C.norm) (x * y) (x * z) = C.norm x * QuadraticMap.polar (⇑C.norm) y z

First linearization of multiplicativity, in the right variable: n(xy, xz) = n(x) n(y, z).

Not a consequence of ConicAlgebra.IsMultiplicative.polar_mul_mul_right — A is not assumed commutative — but proved the same way, from n(x(y + z)) = n(x) n(y + z).

theorem ConicAlgebra.IsMultiplicative.polar_mul_add_polar_mul {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {C : ConicAlgebra k A} (h : C.IsMultiplicative) (x y z w : A) : QuadraticMap.polar (⇑C.norm) (x * z) (y * w) + QuadraticMap.polar (⇑C.norm) (x * w) (y * z) = QuadraticMap.polar (⇑C.norm) x y * QuadraticMap.polar (⇑C.norm) z w

Second linearization of multiplicativity: n(xz, yw) + n(xw, yz) = n(x, y) n(z, w).

This is the bilinear shadow of n(xy) = n(x)n(y), and the identity from which both halves of norm-associativity below are read off. It is ConicAlgebra.IsMultiplicative.polar_mul_mul_right linearized in its second variable.

theorem ConicAlgebra.IsMultiplicative.polar_mul_left {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [IsScalarTower k A A] {C : ConicAlgebra k A} (h : C.IsMultiplicative) (x y z : A) : QuadraticMap.polar (⇑C.norm) (x * y) z = QuadraticMap.polar (⇑C.norm) y (C.conj x * z)

Norm-associativity (GPR 16.12(4), obtained from multiplicativity by GPR 17.2(a)): n(xy, z) = n(y, (conj x)z).

The left factor may be moved across the polar form at the cost of conjugating it. Specialize the second linearization at y = 1, where n(x, 1) = t(x), and use conj x = t(x)·1 - x.

theorem ConicAlgebra.IsMultiplicative.polar_mul_right {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] {C : ConicAlgebra k A} (h : C.IsMultiplicative) (x y z : A) : QuadraticMap.polar (⇑C.norm) (x * y) z = QuadraticMap.polar (⇑C.norm) x (z * C.conj y)

Norm-associativity, the other side (GPR 16.12(3) and 17.2(a)): n(xy, z) = n(x, z(conj y)).

Not a consequence of ConicAlgebra.IsMultiplicative.polar_mul_left — A is not assumed associative or commutative — but proved the same way, specializing the second linearization at w = 1.

theorem ConicAlgebra.IsMultiplicative.trace_mul {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] {C : ConicAlgebra k A} (h : C.IsMultiplicative) (x y : A) : C.trace (x * y) = C.trace x * C.trace y - QuadraticMap.polar (⇑C.norm) x y

In a multiplicative conic algebra, the trace of a product is t(xy) = t(x)t(y) - n(x, y) [GPR, 16.12(5), 16.13].

theorem ConicAlgebra.IsMultiplicative.norm_conj_mul_conj {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {C : ConicAlgebra k A} (h : C.IsMultiplicative) (x y : A) : C.norm (C.conj x * C.conj y) = C.norm x * C.norm y

The norm of a product of conjugates: n((conj x)(conj y)) = n(x) n(y).

theorem ConicAlgebra.IsMultiplicative.anisotropic_iff_noZeroDivisors_of_isDomain {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] {C : ConicAlgebra k A} [IsDomain k] (h : C.IsMultiplicative) : QuadraticMap.Anisotropic C.norm ↔ NoZeroDivisors A

Over a domain, a multiplicative conic algebra has anisotropic norm if and only if it has no zero divisors. Indeed, multiplicativity sends a zero product to a zero product of norms; in the other direction, a null vector annihilates its conjugate, which is zero only when the original vector is zero. This is the zero-divisor step used in GPR 22.19.

theorem ConicAlgebra.IsMultiplicative.hasTwoSidedInverses_iff_anisotropic {K : Type u_1} [Field K] {B : Type u_2} [NonAssocRing B] [Module K B] [SMulCommClass K B B] [IsScalarTower K B B] {D : ConicAlgebra K B} (h : D.IsMultiplicative) : D.HasTwoSidedInverses ↔ QuadraticMap.Anisotropic D.norm

Over a field, every nonzero element of a multiplicative conic algebra has a two-sided inverse if and only if its norm is anisotropic. Forwards, a null nonzero element cannot have an inverse because norms multiply. Backwards, n(x)⁻¹ (conj x) is a two-sided inverse. This is the step of GPR 22.18 that GPR phrases with division algebras; HasTwoSidedInverses is weaker than that notion in general, and agrees with it for composition algebras (ConicAlgebra.IsComposition.isDivision_iff_hasTwoSidedInverses).

theorem ConicAlgebra.isMultiplicative_baseRing (k : Type u) [CommRing k] : (baseRing k).IsMultiplicative

The base ring is a multiplicative conic algebra: (xy)² = x² y². Together with QuadraticForm.isGPRNonsingular_rankOne this makes k the rank-one composition algebra.