Division conic algebras (GPR 8.6, GPR 13.8)

A conic algebra can fall short of being a division algebra in the sense of GPR 8.6 (IsDivision: nonzero, with bijective left and right multiplications by nonzero elements) in two ways: its norm may have a nonzero null vector, or — without alternativity — a two-sided inverse may fail to make the multiplications bijective. This file compares the three conditions

• IsDivision A,
• C.HasTwoSidedInverses (every nonzero element has a two-sided inverse),
• C.norm.Anisotropic,

over a field. Without any hypothesis on the multiplication, division implies anisotropy, and anisotropy implies two-sided inverses (n(x)⁻¹ (conj x)). For an alternative conic algebra all three agree, once A ≠ 0: that is GPR 13.8 for conic algebras. The real sedenions show that the alternativity hypothesis cannot be dropped (ConicAlgebra.not_isDivision_realSedenion, GPR Exc. 19.29(e)).

The engine is the pair of identities (conj x) (x y) = n(x) y = (y x) (conj x), which hold in every alternative conic algebra: write conj x = t(x)·1 - x and apply the alternative laws and x² = t(x) x - n(x)·1. So when n(x) is invertible, n(x)⁻¹ (conj x) inverts left and right multiplication by x.

Main results

• ConicAlgebra.conj_mul_mul_of_isAlternative, ConicAlgebra.mul_mul_conj_of_isAlternative : (conj x) (x y) = n(x) y and (y x) (conj x) = n(x) y in an alternative conic algebra.
• ConicAlgebra.anisotropic_of_isDivision : a division conic algebra has anisotropic norm.
• ConicAlgebra.hasTwoSidedInverses_of_anisotropic : over a field, an anisotropic norm gives two-sided inverses. No alternativity is needed.
• ConicAlgebra.anisotropic_of_hasTwoSidedInverses : for an alternative conic algebra, two-sided inverses force the norm to be anisotropic.
• ConicAlgebra.isDivision_of_anisotropic : over a field, a nonzero alternative conic algebra with anisotropic norm is a division algebra.
• ConicAlgebra.isDivision_iff_hasTwoSidedInverses, ConicAlgebra.isDivision_iff_anisotropic : GPR 13.8 for alternative conic algebras over a field.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 8.6, 13.8, Exc. 19.29.

theorem ConicAlgebra.conj_mul_mul_of_isAlternative {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [IsScalarTower k A A] (C : ConicAlgebra k A) [IsAlternative A] (x y : A) : C.conj x * (x * y) = C.norm x • y

In an alternative conic algebra, (conj x) (x y) = n(x) y: expand conj x = t(x)·1 - x, use the left alternative law x (x y) = (x x) y, and the degree-two identity x x = t(x) x - n(x)·1.

theorem ConicAlgebra.mul_mul_conj_of_isAlternative {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] (C : ConicAlgebra k A) [IsAlternative A] (x y : A) : y * x * C.conj x = C.norm x • y

In an alternative conic algebra, (y x) (conj x) = n(x) y, by the right alternative law.

theorem ConicAlgebra.mul_conj_mul_of_isAlternative {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [IsScalarTower k A A] (C : ConicAlgebra k A) [IsAlternative A] (x y : A) : x * (C.conj x * y) = C.norm x • y

x ((conj x) y) = n(x) y: the identity conj_mul_mul_of_isAlternative for conj x.

theorem ConicAlgebra.mul_conj_mul_conj_of_isAlternative {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] (C : ConicAlgebra k A) [IsAlternative A] (x y : A) : y * C.conj x * x = C.norm x • y

(y (conj x)) x = n(x) y: the identity mul_mul_conj_of_isAlternative for conj x.

theorem ConicAlgebra.anisotropic_of_isDivision {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] (C : ConicAlgebra k A) (h : IsDivision A) : QuadraticMap.Anisotropic C.norm

A division conic algebra has anisotropic norm. If n(x) = 0 then x (conj x) = n(x)·1 = 0, and conj x ≠ 0 when x ≠ 0, so x would be a zero divisor. No alternativity is needed.

theorem ConicAlgebra.anisotropic_of_hasTwoSidedInverses {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [IsScalarTower k A A] (C : ConicAlgebra k A) [IsAlternative A] (h : C.HasTwoSidedInverses) : QuadraticMap.Anisotropic C.norm

For an alternative conic algebra, two-sided inverses force an anisotropic norm. If x y = 1 and n(x) = 0, then conj x = (conj x) (x y) = n(x) y = 0, so x = 0. Only the one-sided inverse x y = 1 is used.

theorem ConicAlgebra.hasTwoSidedInverses_of_anisotropic {K : Type u} {A : Type v} [Field K] [NonAssocRing A] [Module K A] [SMulCommClass K A A] [IsScalarTower K A A] (C : ConicAlgebra K A) (h : QuadraticMap.Anisotropic C.norm) : C.HasTwoSidedInverses

Over a field, an anisotropic norm gives two-sided inverses: n(x)⁻¹ (conj x) inverts any nonzero x. Only x (conj x) = (conj x) x = n(x)·1 is used, so neither alternativity nor associativity is needed — and the result is correspondingly weak: see ConicAlgebra.HasTwoSidedInverses.

theorem ConicAlgebra.hasTwoSidedInverses_of_isDivision {K : Type u} {A : Type v} [Field K] [NonAssocRing A] [Module K A] [SMulCommClass K A A] [IsScalarTower K A A] (C : ConicAlgebra K A) (h : IsDivision A) : C.HasTwoSidedInverses

Over a field, a division conic algebra has two-sided inverses.

theorem ConicAlgebra.isDivision_of_anisotropic {K : Type u} {A : Type v} [Field K] [NonAssocRing A] [Module K A] [SMulCommClass K A A] [IsScalarTower K A A] (C : ConicAlgebra K A) [IsAlternative A] [Nontrivial A] (h : QuadraticMap.Anisotropic C.norm) : IsDivision A

Over a field, a nonzero alternative conic algebra with anisotropic norm is a division algebra in the sense of GPR 8.6. For u ≠ 0 the scalar n(u) is invertible, and v ↦ n(u)⁻¹ ((conj u) v) and v ↦ n(u)⁻¹ (v (conj u)) invert left and right multiplication by u, by the identities (conj x) (x y) = n(x) y = x ((conj x) y) and (y x) (conj x) = n(x) y = (y (conj x)) x.

theorem ConicAlgebra.isDivision_iff_hasTwoSidedInverses {K : Type u} {A : Type v} [Field K] [NonAssocRing A] [Module K A] [SMulCommClass K A A] [IsScalarTower K A A] (C : ConicAlgebra K A) [IsAlternative A] : IsDivision A ↔ Nontrivial A ∧ C.HasTwoSidedInverses

GPR 13.8, for conic algebras over a field. An alternative conic algebra is a division algebra in the sense of GPR 8.6 exactly when it is nonzero and every nonzero element has a two-sided inverse. Without alternativity only → holds: the real sedenions have two-sided inverses but are not a division algebra (ConicAlgebra.not_isDivision_realSedenion).

theorem ConicAlgebra.isDivision_iff_anisotropic {K : Type u} {A : Type v} [Field K] [NonAssocRing A] [Module K A] [SMulCommClass K A A] [IsScalarTower K A A] (C : ConicAlgebra K A) [IsAlternative A] : IsDivision A ↔ Nontrivial A ∧ QuadraticMap.Anisotropic C.norm

An alternative conic algebra over a field is a division algebra exactly when it is nonzero and its norm is anisotropic.