Base change of quadratic forms #
This file supplies the functorial API for extending quadratic spaces along a commutative algebra.
The pure-tensor map also restricts to the polar kernel of a vector, so orthogonal parameters can
be extended before passing to quotient spaces.
It lifts isometries and isometric equivalences by extending their underlying linear maps, records
the interaction with the additive operations on forms, compares direct and successive extension
through a scalar tower, and proves that finite-dimensional nondegenerate forms remain
nondegenerate over a field extension. It also identifies the base change of a diagonal form with
the diagonal form obtained by mapping its coefficients into the target algebra, extends
orthogonal and special orthogonal automorphisms so a quadratic space's rational symmetries act on
each scalar extension, and shows that extending scalars carries the reflection in a vector v to
the reflection in 1 ⊗ₜ v.
These results complement Mathlib's construction QuadraticForm.baseChange and its pure-tensor
evaluation theorem. They allow localizations of a quadratic space to inherit maps, injective
representations, isotropy, and regularity from the original space without choosing bases in each
completion.
Base change of an isometry of quadratic forms.
Unlike QuadraticMap.Isometry.tmul, this construction is heterobasic: the original forms are
over R, while their base changes are over the possibly different algebra A.
Equations
- f.baseChange A = { toLinearMap := LinearMap.baseChange A f.toLinearMap, map_app' := ⋯ }
Instances For
On pure tensors, base change of an isometry applies the original isometry to the vector.
The linear map underlying a base-changed isometry is the base change of the original linear map.
Base change sends the identity isometry to the identity isometry.
Base change commutes with composition of isometries.
Base change of an isometric equivalence of quadratic forms.
Equations
- f.baseChange A = { toLinearEquiv := LinearEquiv.baseChange R A M N f.toLinearEquiv, map_app' := ⋯ }
Instances For
On pure tensors, base change of an isometric equivalence applies the original equivalence to the vector.
The linear equivalence underlying a base-changed isometric equivalence is the base change of the original linear equivalence.
Passing from a base-changed isometric equivalence to an isometry commutes with base change.
Base change sends the identity isometric equivalence to the identity equivalence.
Base change commutes with composition of isometric equivalences.
Base change commutes with inversion of isometric equivalences.
Isometric quadratic forms remain isometric after base change.
A scalar represented by a quadratic form remains represented after base change.
Polarization after base change, evaluated on pure tensors.
The canonical coordinate equivalence identifies the base change of a diagonal quadratic form with the diagonal form obtained by mapping each coefficient into the target algebra.
Equations
- QuadraticForm.baseChangeWeightedSumSquares w = { toLinearEquiv := TensorProduct.piScalarRight R A A ι, map_app' := ⋯ }
Instances For
The underlying linear equivalence for diagonal base change is the canonical distribution of tensor product over the finite coordinate space.
The canonical equivalence distributing tensor product over a product identifies the base change of an orthogonal sum with the orthogonal sum of the base changes.
Equations
- Q.baseChangeProd Q' = { toLinearEquiv := TensorProduct.prodRight R A A M N, map_app' := ⋯ }
Instances For
On pure tensors, the equivalence identifying base change with an orthogonal sum separates the two components.
The inverse equivalence identifying an orthogonal sum with a base change combines a pair of pure tensors with the same scalar into a pure tensor of the paired vectors.
Base change sends the zero quadratic form to the zero quadratic form.
Base change commutes with addition of quadratic forms.
Base change commutes with negation of quadratic forms.
Base change commutes with subtraction of quadratic forms.
Scaling before base change agrees with scaling by the image of the scalar afterward.
A quadratic form vanishes after a faithful scalar extension exactly when it vanishes.
This is the quadratic-form analogue of Mathlib's
LinearMap.BilinForm.baseChange_eq_zero_iff.
Isotropy is preserved by a faithful scalar extension when the underlying module is flat.
Representation of one quadratic form by another is preserved by flat base change.
Orthogonal groups #
Extending scalars carries an orthogonal automorphism of Q to an orthogonal automorphism of
Q.baseChange A. Over a field extension this is the map that compares the rational and local
orthogonal groups.
Equations
- TauCeti.QuadraticMap.orthogonalGroupBaseChange Q = { toFun := fun (g : ↥(TauCeti.QuadraticMap.orthogonalGroup Q)) => ⟨LinearEquiv.baseChange R A M M ↑g, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The linear equivalence underlying an orthogonal automorphism after scalar extension is the base change of its original linear equivalence.
The matrix of a scalar-extended orthogonal automorphism in a base-changed basis is obtained by applying the algebra map to each entry.
On a pure tensor, base change of an orthogonal automorphism applies the automorphism to the second tensor factor.
The determinant of a base-changed orthogonal automorphism is the image of its original determinant.
Scalar extension of orthogonal automorphisms is injective whenever the extension is faithful and the original module is flat. In particular, this applies to extensions of fields.
Base change preserves the determinant-one condition, giving the corresponding map on special orthogonal groups.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The linear equivalence underlying a base-changed special orthogonal automorphism is the base change of its underlying linear equivalence.
The special-orthogonal base-change map is the orthogonal base-change map restricted to the determinant-one subgroup.
Base change commutes with the inclusion SO(Q) →* O(Q).
On pure tensors, base change of a special orthogonal automorphism acts on the second factor.
Scalar extension of special orthogonal automorphisms is injective whenever the extension is faithful and the original module is flat.
Extending scalars carries the reflection in v to the reflection in 1 ⊗ₜ v: the base change
of τ_v is τ_{1 ⊗ v} for Q.baseChange A.
Direct base change through a scalar tower is isometric to successive base change.
The underlying linear equivalence is the inverse of Mathlib's canonical cancellation
B ⊗[A] (A ⊗[R] M) ≃ B ⊗[R] M.
Equations
- Q.baseChangeBaseChange = { toLinearEquiv := (TensorProduct.AlgebraTensorModule.cancelBaseChange R A B B M).symm, map_app' := ⋯ }
Instances For
The linear equivalence underlying repeated base change is Mathlib's canonical tensor-product cancellation, read in the direction from direct to successive base change.
On a pure tensor, the scalar-tower base-change equivalence inserts the intermediate unit tensor.
The inverse scalar-tower base-change equivalence multiplies the intermediate scalar into the outer tensor factor.
Conjugating a directly extended orthogonal automorphism by the canonical scalar-tower equivalence agrees with extending it successively.
The special-orthogonal scalar-extension maps satisfy the same scalar-tower law, read through the canonical inclusion into the orthogonal group.
A finite-dimensional nondegenerate quadratic form stays nondegenerate after extending its base field.
On a space of dimension at most one, a quadratic form is anisotropic exactly when its
extension to a nontrivial ring without zero divisors is anisotropic. Dimension one is sharp:
⟨1, 1⟩ over ℚ is anisotropic, while its extension to ℂ is not.
Pure tensors carry the orthogonal kernel of u into that of 1 ⊗ u.
Equations
- TauCeti.QuadraticMap.polarKernelBaseChange Q u = { toFun := fun (w : ↥((QuadraticMap.polarBilin Q) u).ker) => ⟨1 ⊗ₜ[R] ↑w, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }
Instances For
The scalar-extension map on an orthogonal kernel is the pure-tensor map on vectors.