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 QuadraticMap.IsometryEquiv {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] (Q₁ : QuadraticMap R M₁ N) (Q₂ : QuadraticMap R M₂ N) extends M₁ ≃ₗ[R] M₂ : 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.

• toFun : M₁ → M₂
• map_add' (x y : M₁) : (↑self.toLinearEquiv).toFun (x + y) = (↑self.toLinearEquiv).toFun x + (↑self.toLinearEquiv).toFun y
• map_smul' (m : R) (x : M₁) : (↑self.toLinearEquiv).toFun (m • x) = (RingHom.id R) m • (↑self.toLinearEquiv).toFun x
• invFun : M₂ → M₁
• left_inv : Function.LeftInverse self.invFun (↑self.toLinearEquiv).toFun
• right_inv : Function.RightInverse self.invFun (↑self.toLinearEquiv).toFun
• map_app' (m : M₁) : Q₂ ((↑self.toLinearEquiv).toFun m) = Q₁ m

def QuadraticMap.Equivalent {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] (Q₁ : QuadraticMap R M₁ N) (Q₂ : QuadraticMap R M₂ N) : 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.

@[implicit_reducible]

instance QuadraticMap.IsometryEquiv.instEquivLike {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} : EquivLike (Q₁.IsometryEquiv Q₂) M₁ M₂

instance QuadraticMap.IsometryEquiv.instLinearEquivClass {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} : LinearEquivClass (Q₁.IsometryEquiv Q₂) R M₁ M₂

@[implicit_reducible]

instance QuadraticMap.IsometryEquiv.instCoeOutLinearEquivId {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} : CoeOut (Q₁.IsometryEquiv Q₂) (M₁ ≃ₗ[R] M₂)

@[simp]

theorem QuadraticMap.IsometryEquiv.coe_toLinearEquiv {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (f : Q₁.IsometryEquiv Q₂) : ⇑f.toLinearEquiv = ⇑f

@[simp]

theorem QuadraticMap.IsometryEquiv.map_app {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (f : Q₁.IsometryEquiv Q₂) (m : M₁) : Q₂ (f m) = Q₁ m

def QuadraticMap.IsometryEquiv.refl {R : Type u_2} {M : Type u_4} {N : Type u_9} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (Q : QuadraticMap R M N) : Q.IsometryEquiv Q

The identity isometric equivalence between a quadratic form and itself.

def QuadraticMap.IsometryEquiv.symm {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (f : Q₁.IsometryEquiv Q₂) : Q₂.IsometryEquiv Q₁

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

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

The composition of two isometric equivalences between quadratic forms.

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

Isometric equivalences are isometric maps

@[simp]

theorem QuadraticMap.IsometryEquiv.toIsometry_apply {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (g : Q₁.IsometryEquiv Q₂) (x : M₁) : g.toIsometry x = g x

@[simp]

theorem QuadraticMap.IsometryEquiv.apply_symm_apply {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (f : Q₁.IsometryEquiv Q₂) (x : M₂) : f (f.symm x) = x

@[simp]

theorem QuadraticMap.IsometryEquiv.symm_apply_apply {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (f : Q₁.IsometryEquiv Q₂) (x : M₁) : f.symm (f x) = x

@[simp]

theorem QuadraticMap.IsometryEquiv.coe_symm_toLinearEquiv {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (f : Q₁.IsometryEquiv Q₂) : f.symm = f.symm.toLinearEquiv

theorem QuadraticMap.Equivalent.refl {R : Type u_2} {M : Type u_4} {N : Type u_9} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (Q : QuadraticMap R M N) : Q.Equivalent Q

theorem QuadraticMap.Equivalent.symm {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (h : Q₁.Equivalent Q₂) : Q₂.Equivalent Q₁

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

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

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

noncomputable def QuadraticMap.isometryEquivBasisRepr {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_9} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Finite ι] (Q : QuadraticMap R M N) (v : Module.Basis ι R M) : Q.IsometryEquiv (Q.basisRepr 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 : Module.Basis (Fin (Module.finrank K V)) K V) (hv₁ : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑v) : QuadraticMap.IsometryEquiv Q (QuadraticMap.weightedSumSquares K fun (i : Fin (Module.finrank K V)) => 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 : Fin (Module.finrank K V) → K), QuadraticMap.Equivalent Q (QuadraticMap.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 : LinearMap.SeparatingLeft (QuadraticMap.associated Q)) : ∃ (w : Fin (Module.finrank K V) → Kˣ), QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares K w)

def QuadraticForm.weightedSumSquaresCongr {ι : Type u_10} {S : Type u_11} {R : Type u_12} [Fintype ι] [CommSemiring R] [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] {w w' : ι → S} (h : w = w') : (QuadraticMap.weightedSumSquares R w).IsometryEquiv (QuadraticMap.weightedSumSquares R w')

The isometry between two weighted sum of squares of equal weights.

def QuadraticForm.isometryEquivWeightedSumSquaresWeightedSumSquares {ι : Type u_10} {S : Type u_11} {R : Type u_12} [Fintype ι] [CommSemiring R] [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] [IsScalarTower S R R] {w w' : ι → S} (u : ι → Sˣ) (h : ∀ (i : ι), w' i * ↑(u i) ^ 2 = w i) : (QuadraticMap.weightedSumSquares R w).IsometryEquiv (QuadraticMap.weightedSumSquares R w')

The isometry between two weighted sum of squares, give that each weight is scaled by the square of a unit.