Base change of conic algebras (the final paragraph of `GPR 16.1`) #

A conic algebra (A, n) over k gives a conic algebra (S ⊗[k] A, n_S) over every commutative k-algebra S. This is what lets the classification arguments localize, and it is a prerequisite for Cayley–Dickson doubling (Layer 6), whose compatibility with base change is GPR 18.x.

Main definitions #

ConicAlgebra.baseChangeOfProjective : the conic algebra S ⊗[k] A.

Main results #

ConicAlgebra.mul_add_mul_baseChangeOfProjective : the linearized degree-two identity holds on S ⊗[k] A. It is proved before the degree-two identity itself, because it is bi-additive and so reduces to pure tensors, whereas the degree-two identity is quadratic and its additivity step is exactly the linearized identity.
ConicAlgebra.baseChangeOfProjective_norm_tmul, ConicAlgebra.baseChangeOfProjective_trace_tmul, ConicAlgebra.baseChangeOfProjective_conj_tmul : norm, trace and conjugation on pure tensors.

Implementation notes #

Finitely generated projective, and why the name says so. The norm is base changed with QuadraticForm.baseChangeOfProjective (QuadraticForm/BaseChangeProjective.lean), which needs A finitely generated projective over k but — unlike mathlib's QuadraticForm.baseChange — nothing about 2. So this is not base change of conic algebras in general, and the name carries the restriction to the call site rather than burying it in a docstring: a hypothesis on a definition is against overview §2, and one that is invisible would be worse.

The final paragraph of GPR 16.1 has no such restriction, because a quadratic form base changes over an arbitrary module: q_S is the unique form on S ⊗[k] M with q_S(s ⊗ m) = s² q(m) and the expected polar form. Proving that needs quadratic maps as degree-two polynomial laws (Roby); mathlib now has polynomial laws (PolynomialLaw) but does not yet relate them to QuadraticMap, and this project does not either. baseChangeOfProjective sidesteps it by choosing a bilinear b with b(x, x) = q(x), which exists whenever the module is projective (QuadraticMap.hasBilinRepr_of_projective) — though not only then: the zero form has one on every module, and when 2 is invertible half the polar form represents every form. Nothing downstream needs the general case: composition algebras are finitely generated projective by definition, and Cayley–Dickson doubling preserves that. See the TODO below.

The multiplication is mathlib's. S ⊗[k] A carries NonAssocRing from Mathlib/RingTheory/TensorProduct/Basic.lean, which builds the multiplication on a tensor product of two possibly non-associative algebras. Nothing has to be constructed here beyond the norm.

References #

[GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 16.1.
N. Roby, Lois polynômes et lois formelles en théorie des modules, Ann. Sci. ÉNS 80 (1963), 213–348: quadratic maps as degree-two polynomial laws, which is what general base change needs.

TODO #

Base change of a quadratic form over an arbitrary module, hence the full statement following GPR 16.1 without the projectivity hypothesis. This is missing from mathlib too, and is all that stands between ConicAlgebra.baseChangeOfProjective and ConicAlgebra.baseChange.

The base-changed norm #

source

theorem ConicAlgebra.baseChangeOfProjective_norm_tmul {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [Module.Finite k A] [Module.Projective k A] (S : Type w) [CommRing S] [Algebra k S] (C : ConicAlgebra k A) (s : S) (a : A) :

(QuadraticForm.baseChangeOfProjective S C.norm) (s ⊗ₜ[k] a) = C.norm a • (s * s)

The norm of the base-changed algebra on a pure tensor.

source

theorem ConicAlgebra.baseChangeOfProjective_polar_tmul {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [Module.Finite k A] [Module.Projective k A] (S : Type w) [CommRing S] [Algebra k S] (C : ConicAlgebra k A) (s s' : S) (a a' : A) :

QuadraticMap.polar (⇑(QuadraticForm.baseChangeOfProjective S C.norm)) (s ⊗ₜ[k] a) (s' ⊗ₜ[k] a') = QuadraticMap.polar (⇑C.norm) a a' • (s * s')

The polar form of the base-changed norm on pure tensors.

source

theorem ConicAlgebra.baseChangeOfProjective_trace_tmul {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [Module.Finite k A] [Module.Projective k A] (S : Type w) [CommRing S] [Algebra k S] (C : ConicAlgebra k A) (s : S) (a : A) :

QuadraticMap.polar (⇑(QuadraticForm.baseChangeOfProjective S C.norm)) 1 (s ⊗ₜ[k] a) = C.trace a • s

The trace of the base-changed algebra on a pure tensor: t(s ⊗ a) = t(a) • s.

The degree-two identity #

source

theorem ConicAlgebra.mul_add_mul_baseChangeOfProjective {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] (S : Type w) [CommRing S] [Algebra k S] (C : ConicAlgebra k A) (x y : TensorProduct k S A) :

x * y + y * x = QuadraticMap.polar (⇑(QuadraticForm.baseChangeOfProjective S C.norm)) 1 x • y + QuadraticMap.polar (⇑(QuadraticForm.baseChangeOfProjective S C.norm)) 1 y • x - QuadraticMap.polar (⇑(QuadraticForm.baseChangeOfProjective S C.norm)) x y • 1

The linearized degree-two identity on S ⊗[k] A. Both sides are additive in each argument, so this reduces to pure tensors, where it is ConicAlgebra.mul_add_mul in A.

source

theorem ConicAlgebra.mul_self_baseChangeOfProjective {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] (S : Type w) [CommRing S] [Algebra k S] (C : ConicAlgebra k A) (x : TensorProduct k S A) :

x * x = QuadraticMap.polar (⇑(QuadraticForm.baseChangeOfProjective S C.norm)) 1 x • x - (QuadraticForm.baseChangeOfProjective S C.norm) x • 1

The degree-two identity on S ⊗[k] A. On pure tensors it is the identity in A; the additivity step is ConicAlgebra.mul_add_mul_baseChangeOfProjective.

source