Base change preserves multiplicativity (GPR 19.7)

If the norm of a conic algebra A over k permits composition, then so does the norm of S ⊗[k] A for every commutative k-algebra S. Together with the base-change stability of non-singularity, which is built into QuadraticForm.IsGPRNonsingular by definition, this is what makes ConicAlgebra.IsComposition stable under base change, and it is the step that lets a statement about composition algebras over a ring be tested on the residue fields.

Main results

• ConicAlgebra.IsMultiplicative.baseChangeOfProjective : n(XY) = n(X) n(Y) on S ⊗[k] A.

Implementation notes

Multiplicativity is quadratic, so it does not reduce to pure tensors on its own: the additivity step in an induction over S ⊗[k] A produces a cross term n(X₁Y, X₂Y), which is not part of the statement being proved. The proof therefore runs the three levels of linearization from Conic/Multiplicative.lean in the reverse of the usual order, each one supplying the additivity step of the next:

• polar_mul_add_polar_mul_baseChangeOfProjective (n(XZ, YW) + n(XW, YZ) = n(X, Y) n(Z, W)) is additive in each of its four arguments separately, so it does reduce to pure tensors, by four nested inductions;
• polar_mul_mul_right_baseChangeOfProjective and polar_mul_mul_left_baseChangeOfProjective (n(XZ, YZ) = n(X, Y) n(Z) and n(XY, XZ) = n(X) n(Y, Z)) are additive in two of their three arguments and quadratic in the third; the cross term of the quadratic one is the second linearization above;
• multiplicativity itself is quadratic in both arguments, and its two cross terms are the two first linearizations.

The two first linearizations are genuinely two statements: A is not assumed associative or commutative, so neither follows from the other (Conic/Multiplicative.lean makes the same point about A itself). Nothing here needs alternativity, regularity, or a hypothesis on 2; the finite projectivity is inherited from ConicAlgebra.baseChangeOfProjective, which needs it to base change the norm at all.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 19.1, 19.7.

theorem ConicAlgebra.IsMultiplicative.polar_mul_add_polar_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} (h : C.IsMultiplicative) (x y z w : TensorProduct k S A) : QuadraticMap.polar (⇑(QuadraticForm.baseChangeOfProjective S C.norm)) (x * z) (y * w) + QuadraticMap.polar (⇑(QuadraticForm.baseChangeOfProjective S C.norm)) (x * w) (y * z) = QuadraticMap.polar (⇑(QuadraticForm.baseChangeOfProjective S C.norm)) x y * QuadraticMap.polar (⇑(QuadraticForm.baseChangeOfProjective S C.norm)) z w

The second linearization of multiplicativity, after base change: n(XZ, YW) + n(XW, YZ) = n(X, Y) n(Z, W) on S ⊗[k] A.

Both sides are additive in each of the four arguments separately, so four nested inductions reduce this to pure tensors, where it is ConicAlgebra.IsMultiplicative.polar_mul_add_polar_mul in A together with commutativity of S.

theorem ConicAlgebra.IsMultiplicative.polar_mul_mul_right_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} (h : C.IsMultiplicative) (x y z : TensorProduct k S A) : QuadraticMap.polar (⇑(QuadraticForm.baseChangeOfProjective S C.norm)) (x * z) (y * z) = QuadraticMap.polar (⇑(QuadraticForm.baseChangeOfProjective S C.norm)) x y * (QuadraticForm.baseChangeOfProjective S C.norm) z

The first linearization of multiplicativity, after base change, in the left variable: n(XZ, YZ) = n(X, Y) n(Z) on S ⊗[k] A.

Additive in X and in Y, quadratic in Z; the cross term of the induction on Z is ConicAlgebra.IsMultiplicative.polar_mul_add_polar_mul_baseChangeOfProjective.

theorem ConicAlgebra.IsMultiplicative.polar_mul_mul_left_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} (h : C.IsMultiplicative) (x y z : TensorProduct k S A) : QuadraticMap.polar (⇑(QuadraticForm.baseChangeOfProjective S C.norm)) (x * y) (x * z) = (QuadraticForm.baseChangeOfProjective S C.norm) x * QuadraticMap.polar (⇑(QuadraticForm.baseChangeOfProjective S C.norm)) y z

The first linearization of multiplicativity, after base change, in the right variable: n(XY, XZ) = n(X) n(Y, Z) on S ⊗[k] A.

Not a consequence of polar_mul_mul_right_baseChangeOfProjective, since A is not assumed commutative, but proved the same way, with the roles of the additive and the quadratic arguments exchanged.

theorem ConicAlgebra.IsMultiplicative.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} (h : C.IsMultiplicative) : (ConicAlgebra.baseChangeOfProjective S C).IsMultiplicative

Multiplicativity is stable under base change. If the norm of A permits composition, so does the norm of S ⊗[k] A for every commutative k-algebra S.

The induction on the left argument has cross term polar_mul_mul_right_baseChangeOfProjective, the one on the right argument polar_mul_mul_left_baseChangeOfProjective, and on pure tensors the identity is n(ab) = n(a) n(b) in A times (st)² = s²t² in S.