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 formsquadratic_form.equvialent: propositional version of the above
Main results #
equivalent_weighted_sum_squares: in finite dimensions, any quadratic form is equivalent to a parametrization ofquadratic_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₂]
[module R M₁]
[module R M₂]
(Q₁ : quadratic_form R M₁)
(Q₂ : quadratic_form R 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
- quadratic_form.isometry.has_sizeof_inst
- quadratic_form.isometry.linear_equiv.has_coe
- quadratic_form.isometry.has_coe_to_fun
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₂]
[module R M₁]
[module R M₂]
(Q₁ : quadratic_form R M₁)
(Q₂ : quadratic_form R 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
- Q₁.equivalent Q₂ = nonempty (Q₁.isometry Q₂)
@[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₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂} :
@[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₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
(f : Q₁.isometry Q₂) :
f.to_linear_equiv = ↑f
@[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₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂} :
has_coe_to_fun (Q₁.isometry Q₂) (λ (_x : Q₁.isometry Q₂), M₁ → M₂)
@[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₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R 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₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
(f : Q₁.isometry Q₂)
(m : M₁) :
@[refl]
def
quadratic_form.isometry.refl
{R : Type u_2}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
(Q : quadratic_form R M) :
Q.isometry Q
The identity isometry from a quadratic form to itself.
Equations
- quadratic_form.isometry.refl Q = {to_linear_equiv := {to_fun := (linear_equiv.refl R M).to_fun, map_add' := _, map_smul' := _, inv_fun := (linear_equiv.refl R M).inv_fun, left_inv := _, right_inv := _}, map_app' := _}
@[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₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
(f : Q₁.isometry Q₂) :
Q₂.isometry Q₁
The inverse isometry of an isometry between two quadratic forms.
@[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₃]
[module R M₁]
[module R M₂]
[module R M₃]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
{Q₃ : quadratic_form R M₃}
(f : Q₁.isometry Q₂)
(g : Q₂.isometry Q₃) :
Q₁.isometry Q₃
The composition of two isometries between quadratic forms.
@[refl]
theorem
quadratic_form.equivalent.refl
{R : Type u_2}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
(Q : quadratic_form R M) :
Q.equivalent Q
@[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₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R 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₃]
[module R M₁]
[module R M₂]
[module R M₃]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
{Q₃ : quadratic_form R 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]
[add_comm_monoid M₁]
[module R M]
[module R M₁]
(Q : quadratic_form R M)
(f : M₁ ≃ₗ[R] M) :
A quadratic form composed with a linear_equiv is isometric to itself.
noncomputable
def
quadratic_form.isometry_basis_repr
{ι : Type u_1}
{R : Type u_2}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
[fintype ι]
(Q : quadratic_form R M)
(v : basis ι R M) :
Q.isometry (Q.basis_repr v)
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]
[add_comm_group V]
[module K V]
(Q : quadratic_form K V)
(v : basis (fin (finite_dimensional.finrank K V)) K V)
(hv₁ : (⇑quadratic_form.associated Q).is_Ortho ⇑v) :
Q.isometry (quadratic_form.weighted_sum_squares K (λ (i : fin (finite_dimensional.finrank K V)), ⇑Q (⇑v i)))
Given an orthogonal basis, a quadratic form is isometric with a weighted sum of squares.
Equations
- Q.isometry_weighted_sum_squares v hv₁ = let iso : Q.isometry (Q.basis_repr v) := Q.isometry_basis_repr v in {to_linear_equiv := ↑iso, map_app' := _}
theorem
quadratic_form.equivalent_weighted_sum_squares
{K : Type u_3}
{V : Type u_8}
[field K]
[invertible 2]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(Q : quadratic_form K V) :
∃ (w : fin (finite_dimensional.finrank K V) → K), Q.equivalent (quadratic_form.weighted_sum_squares K w)
theorem
quadratic_form.equivalent_weighted_sum_squares_units_of_nondegenerate'
{K : Type u_3}
{V : Type u_8}
[field K]
[invertible 2]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(Q : quadratic_form K V)
(hQ : (⇑quadratic_form.associated Q).nondegenerate) :
∃ (w : fin (finite_dimensional.finrank K V) → Kˣ), Q.equivalent (quadratic_form.weighted_sum_squares K w)