# Isometries with respect to quadratic forms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main definitions #

• quadratic_form.isometry: linear_equivs which map between two different quadratic forms
• quadratic_form.equvialent: propositional version of the above

## Main results #

• equivalent_weighted_sum_squares: in finite dimensions, any quadratic form is equivalent to a parametrization of quadratic_form.weighted_sum_squares.
@[nolint]
structure quadratic_form.isometry {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (Q₁ : M₁) (Q₂ : M₂) :
Type (max u_5 u_6)

An isometry 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 quadratic_form.isometry
def quadratic_form.equivalent {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (Q₁ : M₁) (Q₂ : M₂) :
Prop

Two quadratic forms over a ring R are equivalent if there exists an isometry between them: a linear equivalence that transforms one quadratic form into the other.

Equations
@[protected, instance]
def quadratic_form.isometry.linear_equiv.has_coe {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] {Q₁ : M₁} {Q₂ : M₂} :
has_coe (Q₁.isometry Q₂) (M₁ ≃ₗ[R] M₂)
Equations
@[simp]
theorem quadratic_form.isometry.to_linear_equiv_eq_coe {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] {Q₁ : M₁} {Q₂ : M₂} (f : Q₁.isometry Q₂) :
@[protected, instance]
def quadratic_form.isometry.has_coe_to_fun {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] {Q₁ : M₁} {Q₂ : M₂} :
has_coe_to_fun (Q₁.isometry Q₂) (λ (_x : Q₁.isometry Q₂), M₁ M₂)
Equations
@[simp]
theorem quadratic_form.isometry.coe_to_linear_equiv {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] {Q₁ : M₁} {Q₂ : M₂} (f : Q₁.isometry Q₂) :
@[simp]
theorem quadratic_form.isometry.map_app {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] {Q₁ : M₁} {Q₂ : M₂} (f : Q₁.isometry Q₂) (m : M₁) :
Q₂ (f m) = Q₁ m
@[refl]
def quadratic_form.isometry.refl {R : Type u_2} {M : Type u_4} [semiring R] [ M] (Q : M) :

The identity isometry from a quadratic form to itself.

Equations
@[symm]
def quadratic_form.isometry.symm {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] {Q₁ : M₁} {Q₂ : M₂} (f : Q₁.isometry Q₂) :
Q₂.isometry Q₁

The inverse isometry of an isometry between two quadratic forms.

Equations
@[trans]
def quadratic_form.isometry.trans {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} [semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M₁] [ M₂] [ M₃] {Q₁ : M₁} {Q₂ : M₂} {Q₃ : M₃} (f : Q₁.isometry Q₂) (g : Q₂.isometry Q₃) :
Q₁.isometry Q₃

The composition of two isometries between quadratic forms.

Equations
@[refl]
theorem quadratic_form.equivalent.refl {R : Type u_2} {M : Type u_4} [semiring R] [ M] (Q : M) :
@[symm]
theorem quadratic_form.equivalent.symm {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] {Q₁ : M₁} {Q₂ : M₂} (h : Q₁.equivalent Q₂) :
Q₂.equivalent Q₁
@[trans]
theorem quadratic_form.equivalent.trans {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} [semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M₁] [ M₂] [ M₃] {Q₁ : M₁} {Q₂ : M₂} {Q₃ : M₃} (h : Q₁.equivalent Q₂) (h' : Q₂.equivalent Q₃) :
Q₁.equivalent Q₃
def quadratic_form.isometry_of_comp_linear_equiv {R : Type u_2} {M : Type u_4} {M₁ : Type u_5} [semiring R] [add_comm_monoid M₁] [ M] [ M₁] (Q : M) (f : M₁ ≃ₗ[R] M) :

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

Equations
noncomputable def quadratic_form.isometry_basis_repr {ι : Type u_1} {R : Type u_2} {M : Type u_4} [semiring R] [ M] [fintype ι] (Q : M) (v : R M) :

A quadratic form is isometric to its bases representations.

Equations
noncomputable def quadratic_form.isometry_weighted_sum_squares {K : Type u_3} {V : Type u_8} [field K] [invertible 2] [ V] (Q : V) (v : basis (fin K V) (hv₁ : v) :
Q.isometry (λ (i : , Q (v i)))

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

Equations
theorem quadratic_form.equivalent_weighted_sum_squares {K : Type u_3} {V : Type u_8} [field K] [invertible 2] [ V] [ V] (Q : V) :
(w : K),
theorem quadratic_form.equivalent_weighted_sum_squares_units_of_nondegenerate' {K : Type u_3} {V : Type u_8} [field K] [invertible 2] [ V] [ V] (Q : V) (hQ : .nondegenerate) :
(w : Kˣ),