Documentation

LeanPool.CompositionAlgebrasOverRings.Composition.Doubling

A regular subalgebra of a composition algebra splits off (GPR 19.16(a)) #

Let C be a composition algebra over an LG ring k and let B ⊆ C be a unital subalgebra whose restricted norm is regular. If the orthogonal complement Bᗮ has full support — the precise sense in which B is properly contained in C — then there is a v ∈ Bᗮ with n(v) a unit, and

Cay(B, -n(v)) ↪ C, u + wj ↦ u + wv,

is an injective homomorphism. This is GPR 19.16(a): the doubling process, run backwards.

The three steps #

  1. Split. n|_B regular makes B a direct summand, C = B ⊕ Bᗮ, with n = n|_B ⊥ n|_{Bᗮ} (QuadraticForm/OrthogonalComplement.lean). In particular Bᗮ is again finitely generated projective, and n|_{Bᗮ} is non-singular by GN (C.8.3).
  2. Represent. Over an LG ring a non-singular form on a finitely generated projective module of full support represents a unit (GPR 11.26, QuadraticForm/Representation.lean). Applied to n|_{Bᗮ} this produces the element v.
  3. Double. v ⊥ B and n(v) ∈ kˣ are exactly the hypotheses of GPR 18.1 (Conic/Doubling.lean), which turns B + Bv into a copy of Cay(B, -n(v)).

Hypotheses #

Alternativity is derived, not assumed. Every composition algebra is alternative over an arbitrary commutative ring; ConicAlgebra.IsComposition.isAlternative_general supplies the instance used by the doubling identities.

Full support of Bᗮ, not B ≠ C. Over a ring the two are genuinely different: on a product ring a subalgebra may fill up one factor and not the other, and then no single v can work. Full support of the complement — F ⊗ Bᗮ ≠ 0 for every field F ∈ k-alg — is what the representation lemma consumes, and it is the honest hypothesis.

Regularity of n|_B, not non-singularity. It is used twice: to split C at all, and, in ConicAlgebra.cayToAlgebra_injective, to know that the doubled norm has vanishing radical (GN (C.8.3)). Both fail for merely non-singular forms in characteristic 2.

Main results #

References #

source
theorem ConicAlgebra.mem_toSubmodule_iff {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {B : NonAssocSubalgebra k A} {x : A} :
x ∈ B.toSubmodule ↔ x ∈ B

The submodule underlying a unital subalgebra, as a subset of the algebra.

source
theorem ConicAlgebra.hasFullSupport_polarOrthogonal_of_finrank_lt {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [Module.Finite k A] {C : ConicAlgebra k A} {B : NonAssocSubalgebra k A} (hreg : (C.restrict B).norm.IsGPRRegular) (hlt : ∀ (F : Type u) [inst : Field F] [inst_1 : Algebra k F], Module.finrank F (TensorProduct k F ↥B.toSubmodule) < Module.finrank F (TensorProduct k F A)) :
Module.HasFullSupport k ↥(C.norm.polarOrthogonal B.toSubmodule)

B is properly contained in C at every point. If the rank of B is smaller than that of C over every field in k-alg, the orthogonal complement has full support, which is what the representation lemma consumes.

This is the usable form of the hypothesis: over a ring, B ≠ C is not enough — on a product ring a subalgebra can fill up one factor — and the rank inequality is exactly the pointwise statement that it does not.

source
theorem ConicAlgebra.IsComposition.exists_isUnit_norm_orthogonal {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} {B : NonAssocSubalgebra k A} (hLG : IsLGRing k) (h : C.IsComposition) (hreg : (C.restrict B).norm.IsGPRRegular) (hsupp : Module.HasFullSupport k ↥(C.norm.polarOrthogonal B.toSubmodule)) :
∃ (v : A), IsUnit (C.norm v) ∧ ∀ b ∈ B, QuadraticMap.polar (⇑C.norm) b v = 0

GPR 19.16(a), steps 1–2: the element v.

The complement of B is finitely generated projective with non-singular restricted norm, so over an LG ring the representation lemma GPR 11.26 finds a vector of unit norm in it as soon as it has full support.

source
theorem ConicAlgebra.IsComposition.exists_cayToAlgebra {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} {B : NonAssocSubalgebra k A} (hLG : IsLGRing k) (h : C.IsComposition) (hreg : (C.restrict B).norm.IsGPRRegular) (hsupp : Module.HasFullSupport k ↥(C.norm.polarOrthogonal B.toSubmodule)) :
∃ (v : A), IsUnit (C.norm v) ∧ (∀ b ∈ B, QuadraticMap.polar (⇑C.norm) b v = 0) ∧ Function.Injective ⇑(C.cayToAlgebra B v) ∧ (∀ (p q : (C.restrict B).Cay (-C.norm v)), (C.cayToAlgebra B v) (p * q) = (C.cayToAlgebra B v) p * (C.cayToAlgebra B v) q) ∧ ∀ (p : (C.restrict B).Cay (-C.norm v)), C.norm ((C.cayToAlgebra B v) p) = ((C.restrict B).cay (-C.norm v)).norm p

GPR 19.16(a). Over an LG ring, a unital subalgebra B of a composition algebra C whose restricted norm is regular and whose orthogonal complement has full support is doubled inside C: there is a unit μ = -n(v) and an injective, unital, multiplicative, isometric map Cay(B, μ) → C.

The map is ConicAlgebra.cayToAlgebra, u + wj ↦ u + wv; its image is the subalgebra B + Bv.

source
theorem ConicAlgebra.IsComposition.exists_cayToAlgebra_of_field {K : Type u} {A : Type v} [Field K] [NonAssocRing A] [Module K A] [SMulCommClass K A A] [IsScalarTower K A A] [Module.Finite K A] [Module.Projective K A] {C : ConicAlgebra K A} {B : NonAssocSubalgebra K A} (h : C.IsComposition) (hreg : (C.restrict B).norm.IsGPRRegular) (hsupp : Module.HasFullSupport K ↥(C.norm.polarOrthogonal B.toSubmodule)) :
∃ (v : A), IsUnit (C.norm v) ∧ (∀ b ∈ B, QuadraticMap.polar (⇑C.norm) b v = 0) ∧ Function.Injective ⇑(C.cayToAlgebra B v) ∧ (∀ (p q : (C.restrict B).Cay (-C.norm v)), (C.cayToAlgebra B v) (p * q) = (C.cayToAlgebra B v) p * (C.cayToAlgebra B v) q) ∧ ∀ (p : (C.restrict B).Cay (-C.norm v)), C.norm ((C.cayToAlgebra B v) p) = ((C.restrict B).cay (-C.norm v)).norm p

GPR 19.16(a) over a field, where alternativity of C is automatic (GPR 19.3) and the LG hypothesis is discharged by isLGRing_of_field.