Base change of quadratic maps along R → A, without inverting 2

Mathlib's QuadraticForm.baseChange is built as a special case of the tensor product of two quadratic forms, which is constructed by passing to associated symmetric bilinear forms and therefore carries an Invertible (2 : R) hypothesis. That hypothesis is an artefact of the construction: base change of a quadratic form exists over an arbitrary commutative ring. Uniqueness is already unconditional in mathlib (baseChange_ext); only existence needs work.

This file supplies the missing existence, for M a finitely generated projective R-module, by the classical device of choosing a (not necessarily symmetric) bilinear representative B with B x x = Q x, base changing B (which is unconditional, LinearMap.BilinMap.baseChange) and taking the diagonal. The choice of B is non-canonical, but the result is independent of it by baseChange_ext.

Main definitions

• QuadraticMap.HasBilinRepr R M N: every quadratic map M → N is of the form x ↦ B x x.
• QuadraticMap.bilinRepr Q: a chosen bilinear representative of Q, for M f.g. projective.
• QuadraticMap.baseChange A Q : QuadraticMap A (A ⊗[R] M) (A ⊗[R] N).
• QuadraticForm.baseChangeOfProjective A Q : QuadraticForm A (A ⊗[R] M).

Main results

• QuadraticMap.exists_bilinMap: for M finitely generated projective, toQuadraticMap is surjective, i.e. every quadratic map is x ↦ B x x for some bilinear B.
• QuadraticMap.baseChange_tmul, QuadraticForm.baseChangeOfProjective_tmul: the defining property Q_A (a ⊗ₜ m) = (a * a) ⊗ₜ Q m (resp. Q m • (a * a)).
• QuadraticMap.baseChange_eq_of_toQuadraticMap_eq: independence of the chosen representative.
• QuadraticMap.polarBilin_baseChange, QuadraticForm.polarBilin_baseChangeOfProjective: the polar form of the base change is the base change of the polar form — with no hypothesis on 2, unlike QuadraticForm.polarBilin_baseChange.
• QuadraticForm.baseChangeOfProjective_eq_baseChange: agreement with mathlib's QuadraticForm.baseChange when 2 is invertible.
• QuadraticMap.IsometryEquiv.baseChangeOfProjective: base change of an isometry.
• QuadraticForm.anisotropic_baseChangeOfProjective_iff_of_isLocalization, QuadraticForm.anisotropic_baseChangeOfProjective_iff_of_isFractionRing: GPR Exc. 12.38(b) — anisotropy is unchanged by localizing at non-zero-divisors, in particular by passing to the fraction field.

Implementation notes

A bilinear representative exists on every free module: that is mathlib's LinearMap.BilinMap.toQuadraticMap_surjective. A finitely generated projective module is a retract of some Fin n → R, and representatives transport along retracts (QuadraticMap.HasBilinRepr.of_retract), which gives the projective case.

QuadraticForm and LinearMap.BilinForm are abbrevs for QuadraticMap R M R and LinearMap.BilinMap R M R, so dot notation such as Q.baseChange A can resolve ambiguously against mathlib's QuadraticForm.baseChange. Names are therefore fully qualified throughout, and the QuadraticForm-valued construction is given a distinct name.

TODO

• Drop the projectivity hypothesis entirely by constructing base change through the divided square Γ₂(M) (Roby). mathlib now has the divided power algebra DividedPowerAlgebra R M and polynomial laws PolynomialLaw, but not yet Γ₂(M) as the universal quadratic map, nor any link from either to QuadraticMap.

References

• overview §6(a): the mandatory warning this file exists to satisfy — QuadraticMap.associated and hence mathlib's QuadraticForm.baseChange assume 2 ∈ Rˣ, which is unusable for the characteristic-2 examples (GPR 19.4) this development needs to state.
• GN's definition of non-singularity (QuadraticForm/Regularity.lean) needs base change along finitely generated projective modules specifically — matching this file's hypothesis exactly.
• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, Exc. 12.38.

Bilinear representatives

def QuadraticMap.HasBilinRepr (R : Type uR) (M : Type uM) (N : Type uN) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : Prop

HasBilinRepr R M N says that every quadratic map Q : M → N is the diagonal of some bilinear map, i.e. LinearMap.BilinMap.toQuadraticMap is surjective.

Beware the clash of terminology with QuadraticMap.exists_companion, whose companion B satisfies Q (x + y) = Q x + Q y + B x y (so that B x x = 2 • Q x). Here we ask instead for B x x = Q x, which is a genuine extra condition in characteristic two.

Equations

• QuadraticMap.HasBilinRepr R M N = Function.Surjective LinearMap.BilinMap.toQuadraticMap

theorem QuadraticMap.apply_self_of_toQuadraticMap_eq {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {B : LinearMap.BilinMap R M N} {Q : QuadraticMap R M N} (hB : B.toQuadraticMap = Q) (x : M) : (B x) x = Q x

theorem QuadraticMap.HasBilinRepr.of_retract {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : Type u_1} [AddCommGroup P] [Module R P] (h : HasBilinRepr R P N) (i : M →ₗ[R] P) (r : P →ₗ[R] M) (hir : r ∘ₗ i = LinearMap.id) : HasBilinRepr R M N

Transport along a retract: if M is a direct summand of P (witnessed by r ∘ₗ i = id) and every quadratic map on P has a bilinear representative, then so does every quadratic map on M.

theorem QuadraticMap.hasBilinRepr_of_projective (R : Type uR) (M : Type uM) (N : Type uN) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Finite R M] [Module.Projective R M] : HasBilinRepr R M N

Existence of bilinear representatives over finitely generated projective modules. Every finitely generated projective module is a retract of some Fin n → R, which is free, and on a free module every quadratic map has a bilinear representative (LinearMap.BilinMap.toQuadraticMap_surjective).

theorem QuadraticMap.exists_bilinMap {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Finite R M] [Module.Projective R M] (Q : QuadraticMap R M N) : ∃ (B : LinearMap.BilinMap R M N), B.toQuadraticMap = Q

For M finitely generated projective, LinearMap.BilinMap.toQuadraticMap is surjective: every quadratic map is x ↦ B x x for some, generally non-symmetric, bilinear B.

This is the characteristic-free replacement for QuadraticMap.associated, which requires 2 to be invertible in order to pick out the symmetric representative.

noncomputable def QuadraticMap.bilinRepr {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Finite R M] [Module.Projective R M] (Q : QuadraticMap R M N) : LinearMap.BilinMap R M N

A choice of bilinear representative of Q. Non-canonical: only its diagonal is determined (see toQuadraticMap_bilinRepr). Every construction below is proved to be independent of this choice.

Equations

• Q.bilinRepr = ⋯.choose

@[simp]

theorem QuadraticMap.toQuadraticMap_bilinRepr {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Finite R M] [Module.Projective R M] (Q : QuadraticMap R M N) : Q.bilinRepr.toQuadraticMap = Q

@[simp]

theorem QuadraticMap.bilinRepr_apply_self {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Finite R M] [Module.Projective R M] (Q : QuadraticMap R M N) (x : M) : (Q.bilinRepr x) x = Q x

An extensionality lemma for bilinear maps on a base changed module

theorem QuadraticMap.bilin_ext_of_tmul {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] {N₁ : Type u_1} [AddCommGroup N₁] [Module A N₁] ⦃B₁ B₂ : LinearMap.BilinMap A (TensorProduct R A M) N₁⦄ (h : ∀ (m m' : M), (B₁ (1 ⊗ₜ[R] m)) (1 ⊗ₜ[R] m') = (B₂ (1 ⊗ₜ[R] m)) (1 ⊗ₜ[R] m')) : B₁ = B₂

Bilinear maps on A ⊗[R] M are determined by their values on pure tensors 1 ⊗ₜ m. Compare baseChange_ext for quadratic maps.

Base change of quadratic maps

noncomputable def QuadraticMap.baseChange {R : Type uR} (A : Type uA) {M : Type uM} {N : Type uN} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Finite R M] [Module.Projective R M] (Q : QuadraticMap R M N) : QuadraticMap A (TensorProduct R A M) (TensorProduct R A N)

Base change of a quadratic map along an algebra map R → A, for M a finitely generated projective R-module. No invertibility of 2 is required.

Concretely this is the unique quadratic map with Q_A (a ⊗ₜ m) = (a * a) ⊗ₜ Q m; uniqueness is baseChange_ext, and independence of the auxiliary choice is baseChange_eq_of_toQuadraticMap_eq.

Equations

• QuadraticMap.baseChange A Q = (LinearMap.BilinMap.baseChange A Q.bilinRepr).toQuadraticMap

@[simp]

theorem QuadraticMap.baseChange_tmul {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Finite R M] [Module.Projective R M] (Q : QuadraticMap R M N) (a : A) (m : M) : (baseChange A Q) (a ⊗ₜ[R] m) = (a * a) ⊗ₜ[R] Q m

theorem QuadraticMap.baseChange_eq_of_toQuadraticMap_eq {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Finite R M] [Module.Projective R M] (Q : QuadraticMap R M N) {B : LinearMap.BilinMap R M N} (hB : B.toQuadraticMap = Q) : baseChange A Q = (LinearMap.BilinMap.baseChange A B).toQuadraticMap

The base change does not depend on the choice of bilinear representative: any bilinear B with B x x = Q x computes it.

theorem QuadraticMap.baseChange_eq_iff {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Finite R M] [Module.Projective R M] (Q : QuadraticMap R M N) (Q' : QuadraticMap A (TensorProduct R A M) (TensorProduct R A N)) : Q' = baseChange A Q ↔ ∀ (m : M), Q' (1 ⊗ₜ[R] m) = 1 ⊗ₜ[R] Q m

Characterisation of the base change: it is the unique quadratic map on A ⊗[R] M taking the value (a * a) ⊗ₜ Q m on pure tensors.

theorem QuadraticMap.polarBilin_baseChange {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Finite R M] [Module.Projective R M] (Q : QuadraticMap R M N) : (baseChange A Q).polarBilin = LinearMap.BilinMap.baseChange A Q.polarBilin

The polar form of the base change is the base change of the polar form. Unlike QuadraticForm.polarBilin_baseChange, this needs no hypothesis on 2.

Base change of quadratic forms

noncomputable def QuadraticForm.baseChangeOfProjective {R : Type uR} (A : Type uA) {M : Type uM} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (Q : QuadraticForm R M) : QuadraticForm A (TensorProduct R A M)

Base change of a quadratic form along R → A, for M finitely generated projective.

This agrees with mathlib's QuadraticForm.baseChange whenever the latter is defined (baseChangeOfProjective_eq_baseChange) but, unlike it, does not require 2 to be invertible. It is stated separately from QuadraticMap.baseChange so as to land in QuadraticForm A (A ⊗[R] M) rather than QuadraticMap A (A ⊗[R] M) (A ⊗[R] R).

Equations

• QuadraticForm.baseChangeOfProjective A Q = LinearMap.BilinMap.toQuadraticMap (LinearMap.BilinForm.baseChange A (QuadraticMap.bilinRepr Q))

@[simp]

theorem QuadraticForm.baseChangeOfProjective_tmul {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (Q : QuadraticForm R M) (a : A) (m : M) : (baseChangeOfProjective A Q) (a ⊗ₜ[R] m) = Q m • (a * a)

theorem QuadraticForm.baseChangeOfProjective_eq_of_toQuadraticMap_eq {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (Q : QuadraticForm R M) {B : LinearMap.BilinForm R M} (hB : LinearMap.BilinMap.toQuadraticMap B = Q) : baseChangeOfProjective A Q = LinearMap.BilinMap.toQuadraticMap (LinearMap.BilinForm.baseChange A B)

theorem QuadraticForm.polarBilin_baseChangeOfProjective {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (Q : QuadraticForm R M) : QuadraticMap.polarBilin (baseChangeOfProjective A Q) = LinearMap.BilinForm.baseChange A (QuadraticMap.polarBilin Q)

The polar form of the base change is the base change of the polar form, with no hypothesis on 2.

theorem QuadraticForm.baseChangeOfProjective_smul {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (a : R) (Q : QuadraticForm R M) : baseChangeOfProjective A (a • Q) = (algebraMap R A) a • baseChangeOfProjective A Q

Base change commutes with scaling. Rescaling Q by a ∈ R and then base changing is the same as base changing and rescaling by the image of a in A. Compared on pure tensors 1 ⊗ₜ m, where both sides give (a * Q m) • 1 = algebraMap a * algebraMap (Q m).

theorem QuadraticForm.baseChangeOfProjective_comp {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] {P : Type u_1} [AddCommGroup P] [Module R P] [Module.Finite R P] [Module.Projective R P] (Q : QuadraticForm R M) (f : P →ₗ[R] M) : baseChangeOfProjective A (QuadraticMap.comp Q f) = QuadraticMap.comp (baseChangeOfProjective A Q) (LinearMap.baseChange A f)

Base change commutes with pullback along a linear map. For f : P →ₗ[R] M with P and M finitely generated projective, base changing Q ∘ f is the same as pulling back Q_A along f_A.

Both sides are quadratic forms on A ⊗[R] P, so by baseChange_ext it is enough to compare them on the pure tensors 1 ⊗ₜ p, where both give Q (f p). Note that this holds despite baseChangeOfProjective being built from a chosen bilinear representative: the two sides may well be built from unrelated representatives, but a quadratic form on a base changed module is determined by its values on 1 ⊗ₜ p.

noncomputable def QuadraticMap.IsometryEquiv.baseChangeOfProjective {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] {N : Type uN} [AddCommGroup N] [Module R N] [Module.Finite R N] [Module.Projective R N] (Q : QuadraticForm R M) (Q' : QuadraticForm R N) (e : IsometryEquiv Q Q') : IsometryEquiv (QuadraticForm.baseChangeOfProjective A Q) (QuadraticForm.baseChangeOfProjective A Q')

Base change of an isometry between quadratic forms on finite projective modules.

Equations

• QuadraticMap.IsometryEquiv.baseChangeOfProjective Q Q' e = { toLinearEquiv := LinearEquiv.baseChange R A M N e.toLinearEquiv, map_app' := ⋯ }

theorem QuadraticForm.baseChangeOfProjective_eq_baseChange {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] [Invertible 2] (Q : QuadraticForm R M) : baseChangeOfProjective A Q = QuadraticForm.baseChange A Q

When 2 is invertible this recovers mathlib's QuadraticForm.baseChange.

Transitivity

theorem QuadraticForm.baseChangeOfProjective_baseChangeOfProjective_comp_symm {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (S : Type u_1) (T : Type u_2) [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : QuadraticForm R M) : QuadraticMap.comp (baseChangeOfProjective T (baseChangeOfProjective S Q)) ↑(TensorProduct.AlgebraTensorModule.cancelBaseChange R S T T M).symm = baseChangeOfProjective T Q

Base change is transitive, in the form that avoids naming the comparison map on the right-hand side: base changing to S and then to T, and reading the result back along T ⊗[S] (S ⊗[R] M) ≃ T ⊗[R] M, gives the direct base change to T.

Stated this way round because QuadraticMap.baseChange_ext compares two forms on T ⊗[R] M by their values at 1 ⊗ₜ m only, whereas comparing them on T ⊗[S] (S ⊗[R] M) would require knowing them at 1 ⊗ₜ x for every x in S ⊗[R] M — a quadratic condition that does not reduce to pure tensors.

noncomputable def QuadraticForm.baseChangeOfProjectiveIsometryEquiv {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (S : Type u_1) (T : Type u_2) [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : QuadraticForm R M) : QuadraticMap.IsometryEquiv (baseChangeOfProjective T (baseChangeOfProjective S Q)) (baseChangeOfProjective T Q)

Base change is transitive, as an isometry T ⊗[S] (S ⊗[R] M) ≃ T ⊗[R] M.

This is the form the residue-field arguments consume: a predicate on Q.baseChangeOfProjective F for every field F over R can be tested on (Q.baseChangeOfProjective S).baseChangeOfProjective F for every field F over S, since the two forms differ by this isometry.

Equations

• QuadraticForm.baseChangeOfProjectiveIsometryEquiv S T Q = { toLinearEquiv := TensorProduct.AlgebraTensorModule.cancelBaseChange R S T T M, map_app' := ⋯ }

Anisotropy and localization (GPR Exc. 12.38(b))

theorem QuadraticForm.anisotropic_baseChangeOfProjective_iff_of_isLocalization {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (S : Submonoid R) (hS : S ≤ nonZeroDivisors R) (L : Type u_1) [CommRing L] [Algebra R L] [IsLocalization S L] (Q : QuadraticForm R M) : QuadraticMap.Anisotropic (baseChangeOfProjective L Q) ↔ QuadraticMap.Anisotropic Q

GPR Exc. 12.38(b), for quadratic forms. Let L be the localization of R at a multiplicative set S of non-zero-divisors. A quadratic form on a finitely generated projective R-module is anisotropic if and only if its base change to L is; equivalently, it represents zero if and only if its base change does.

A null vector m ≠ 0 gives the null vector 1 ⊗ m ≠ 0, since a projective module has no S-torsion. Conversely a null vector x of L ⊗[R] M satisfies s • x = 1 ⊗ m for some s ∈ S and m ∈ M, and then Q m maps to s² Q_L(x) = 0.

theorem QuadraticForm.anisotropic_baseChangeOfProjective_iff_of_isFractionRing {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (F : Type u_1) [CommRing F] [Algebra R F] [IsFractionRing R F] (Q : QuadraticForm R M) : QuadraticMap.Anisotropic (baseChangeOfProjective F Q) ↔ QuadraticMap.Anisotropic Q

GPR Exc. 12.38(b) over the fraction field. A quadratic form on a finitely generated projective module is anisotropic if and only if its base change to the fraction field is.