# Isometric equivalences with respect to quadratic forms #

## Main definitions #

• QuadraticForm.IsometryEquiv: 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 QuadraticForm.weightedSumSquares.
structure QuadraticForm.IsometryEquiv {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [] [] [] [Module R M₁] [Module R M₂] (Q₁ : ) (Q₂ : ) extends :
Type (max u_5 u_6)

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.

Instances For
def QuadraticForm.Equivalent {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [] [] [] [Module R M₁] [Module R M₂] (Q₁ : ) (Q₂ : ) :

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
instance QuadraticForm.IsometryEquiv.instLinearEquivClassIsometryEquiv {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [] [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } :
LinearEquivClass () R M₁ M₂
instance QuadraticForm.IsometryEquiv.instCoeOutIsometryEquivLinearEquivIdToNonAssocSemiringIds {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [] [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } :
CoeOut () (M₁ ≃ₗ[R] M₂)
@[simp]
theorem QuadraticForm.IsometryEquiv.coe_toLinearEquiv {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [] [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } (f : ) :
f.toLinearEquiv = f
@[simp]
theorem QuadraticForm.IsometryEquiv.map_app {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [] [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } (f : ) (m : M₁) :
Q₂ (f m) = Q₁ m
def QuadraticForm.IsometryEquiv.refl {R : Type u_2} {M : Type u_4} [] [] [Module R M] (Q : ) :

The identity isometric equivalence between a quadratic form and itself.

Instances For
def QuadraticForm.IsometryEquiv.symm {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [] [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } (f : ) :

The inverse isometric equivalence of an isometric equivalence between two quadratic forms.

Instances For
def QuadraticForm.IsometryEquiv.trans {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R M₃] {Q₁ : } {Q₂ : } {Q₃ : } (f : ) (g : ) :

The composition of two isometric equivalences between quadratic forms.

Instances For
@[simp]
theorem QuadraticForm.IsometryEquiv.toIsometry_apply {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [] [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } (g : ) (x : M₁) :
= g x
def QuadraticForm.IsometryEquiv.toIsometry {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [] [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } (g : ) :
Q₁ →qᵢ Q₂

Isometric equivalences are isometric maps

Instances For
theorem QuadraticForm.Equivalent.refl {R : Type u_2} {M : Type u_4} [] [] [Module R M] (Q : ) :
theorem QuadraticForm.Equivalent.symm {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [] [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } (h : ) :
theorem QuadraticForm.Equivalent.trans {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} [] [] [] [] [Module R M₁] [Module R M₂] [Module R M₃] {Q₁ : } {Q₂ : } {Q₃ : } (h : ) (h' : ) :
def QuadraticForm.isometryEquivOfCompLinearEquiv {R : Type u_2} {M : Type u_4} {M₁ : Type u_5} [] [] [] [Module R M] [Module R M₁] (Q : ) (f : M₁ ≃ₗ[R] M) :

A quadratic form composed with a LinearEquiv is isometric to itself.

Instances For
noncomputable def QuadraticForm.isometryEquivBasisRepr {ι : Type u_1} {R : Type u_2} {M : Type u_4} [] [] [Module R M] [] (Q : ) (v : Basis ι R M) :

A quadratic form is isometrically equivalent to its bases representations.

Instances For
noncomputable def QuadraticForm.isometryEquivWeightedSumSquares {K : Type u_3} {V : Type u_8} [] [] [] [Module K V] (Q : ) (v : Basis () K V) (hv₁ : BilinForm.iIsOrtho (QuadraticForm.associated Q) v) :

Given an orthogonal basis, a quadratic form is isometrically equivalent with a weighted sum of squares.

Instances For
theorem QuadraticForm.equivalent_weightedSumSquares {K : Type u_3} {V : Type u_8} [] [] [] [Module K V] [] (Q : ) :
theorem QuadraticForm.equivalent_weightedSumSquares_units_of_nondegenerate' {K : Type u_3} {V : Type u_8} [] [] [] [Module K V] [] (Q : ) (hQ : BilinForm.Nondegenerate (QuadraticForm.associated Q)) :