Isometric equivalences with respect to quadratic forms #
Main definitions #
LinearEquivs which map between two different quadratic forms
QuadraticForm.Equivalent: propositional version of the above
Main results #
equivalent_weighted_sum_squares: in finite dimensions, any quadratic form is equivalent to a parametrization of
- toFun : M₁ → M₂
- invFun : M₂ → M₁
- left_inv : Function.LeftInverse s.invFun s.toFun
- right_inv : Function.RightInverse s.invFun s.toFun
An isometric equivalence between two quadratic spaces
M₁, Q₁ and
M₂, Q₂ over a ring
is a linear equivalence between
M₂ that commutes with the quadratic forms.
Two quadratic forms over a ring
R are equivalent
if there exists an isometric equivalence between them:
a linear equivalence that transforms one quadratic form into the other.
The inverse isometric equivalence of an isometric equivalence between two quadratic forms.
The composition of two isometric equivalences between quadratic forms.
Isometric equivalences are isometric maps
A quadratic form composed with a
LinearEquiv is isometric to itself.
A quadratic form is isometrically equivalent to its bases representations.
Given an orthogonal basis, a quadratic form is isometrically equivalent with a weighted sum of squares.