Isometric equivalences with respect to quadratic forms #
Main definitions #
QuadraticForm.IsometryEquiv
:LinearEquiv
s which map between two different quadratic formsQuadraticForm.Equivalent
: propositional version of the above
Main results #
equivalent_weighted_sum_squares
: in finite dimensions, any quadratic form is equivalent to a parametrization ofQuadraticForm.weightedSumSquares
.
An isometric equivalence between two quadratic spaces M₁, Q₁
and M₂, Q₂
over a ring R
,
is a linear equivalence between M₁
and M₂
that commutes with the quadratic forms.
- toFun : M₁ → M₂
- invFun : M₂ → M₁
- left_inv : Function.LeftInverse self.invFun (↑self.toLinearEquiv).toFun
- right_inv : Function.RightInverse self.invFun (↑self.toLinearEquiv).toFun
Instances For
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.
Instances For
Equations
- One or more equations did not get rendered due to their size.
The identity isometric equivalence between a quadratic form and itself.
Equations
Instances For
The inverse isometric equivalence of an isometric equivalence between two quadratic forms.
Instances For
The composition of two isometric equivalences between quadratic forms.
Equations
- f.trans g = { toLinearEquiv := f.trans g.toLinearEquiv, map_app' := ⋯ }
Instances For
Isometric equivalences are isometric maps
Equations
- g.toIsometry = { toFun := fun (x : M₁) => g x, map_add' := ⋯, map_smul' := ⋯, map_app' := ⋯ }
Instances For
A quadratic form composed with a LinearEquiv
is isometric to itself.
Equations
Instances For
A quadratic form is isometrically equivalent to its bases representations.
Instances For
Given an orthogonal basis, a quadratic form is isometrically equivalent with a weighted sum of squares.