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} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) extends LinearEquiv : Type (max u_5 u_6)

• toFun : M₁ → M₂
• map_add' : ∀ (x y : M₁), AddHom.toFun s.toAddHom (x + y) = AddHom.toFun s.toAddHom x + AddHom.toFun s.toAddHom y
• map_smul' : ∀ (r : R) (x : M₁), AddHom.toFun s.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun s.toAddHom x
• invFun : M₂ → M₁
• left_inv : Function.LeftInverse s.invFun s.toFun
• right_inv : Function.RightInverse s.invFun s.toFun
• map_app' : ∀ (m : M₁), ↑Q₂ (AddHom.toFun s.toAddHom m) = ↑Q₁ m

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.

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

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.

instance QuadraticForm.IsometryEquiv.instLinearEquivClassIsometryEquiv {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} : LinearEquivClass (QuadraticForm.IsometryEquiv Q₁ Q₂) R M₁ M₂

instance QuadraticForm.IsometryEquiv.instCoeOutIsometryEquivLinearEquivIdToNonAssocSemiringIds {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} : CoeOut (QuadraticForm.IsometryEquiv Q₁ Q₂) (M₁ ≃ₗ[R] M₂)

@[simp]

theorem QuadraticForm.IsometryEquiv.coe_toLinearEquiv {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : QuadraticForm.IsometryEquiv Q₁ Q₂) : ↑f.toLinearEquiv = ↑f

@[simp]

theorem QuadraticForm.IsometryEquiv.map_app {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : QuadraticForm.IsometryEquiv Q₁ Q₂) (m : M₁) : ↑Q₂ (↑f m) = ↑Q₁ m

def QuadraticForm.IsometryEquiv.refl {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) : QuadraticForm.IsometryEquiv Q Q

The identity isometric equivalence between a quadratic form and itself.

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

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

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

The composition of two isometric equivalences between quadratic forms.

@[simp]

theorem QuadraticForm.IsometryEquiv.toIsometry_apply {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (g : QuadraticForm.IsometryEquiv Q₁ Q₂) (x : M₁) : ↑(QuadraticForm.IsometryEquiv.toIsometry g) x = ↑g x

def QuadraticForm.IsometryEquiv.toIsometry {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (g : QuadraticForm.IsometryEquiv Q₁ Q₂) : Q₁ →qᵢ Q₂

Isometric equivalences are isometric maps

theorem QuadraticForm.Equivalent.refl {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) : QuadraticForm.Equivalent Q Q

theorem QuadraticForm.Equivalent.symm {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (h : QuadraticForm.Equivalent Q₁ Q₂) : QuadraticForm.Equivalent Q₂ Q₁

theorem QuadraticForm.Equivalent.trans {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₁] [Module R M₂] [Module R M₃] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃} (h : QuadraticForm.Equivalent Q₁ Q₂) (h' : QuadraticForm.Equivalent Q₂ Q₃) : QuadraticForm.Equivalent Q₁ Q₃

def QuadraticForm.isometryEquivOfCompLinearEquiv {R : Type u_2} {M : Type u_4} {M₁ : Type u_5} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] (Q : QuadraticForm R M) (f : M₁ ≃ₗ[R] M) : QuadraticForm.IsometryEquiv Q (QuadraticForm.comp Q ↑f)

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

noncomputable def QuadraticForm.isometryEquivBasisRepr {ι : Type u_1} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (Q : QuadraticForm R M) (v : Basis ι R M) : QuadraticForm.IsometryEquiv Q (QuadraticForm.basisRepr Q v)

A quadratic form is isometrically equivalent to its bases representations.

noncomputable def QuadraticForm.isometryEquivWeightedSumSquares {K : Type u_3} {V : Type u_8} [Field K] [Invertible 2] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (v : Basis (Fin (FiniteDimensional.finrank K V)) K V) (hv₁ : BilinForm.iIsOrtho (↑QuadraticForm.associated Q) ↑v) : QuadraticForm.IsometryEquiv Q (QuadraticForm.weightedSumSquares K fun i => ↑Q (↑v i))

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

theorem QuadraticForm.equivalent_weightedSumSquares {K : Type u_3} {V : Type u_8} [Field K] [Invertible 2] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) : ∃ w, QuadraticForm.Equivalent Q (QuadraticForm.weightedSumSquares K w)

theorem QuadraticForm.equivalent_weightedSumSquares_units_of_nondegenerate' {K : Type u_3} {V : Type u_8} [Field K] [Invertible 2] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : BilinForm.Nondegenerate (↑QuadraticForm.associated Q)) : ∃ w, QuadraticForm.Equivalent Q (QuadraticForm.weightedSumSquares K w)