mathlib3 documentation

linear_algebra.quadratic_form.isometry

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 #

Main results #

@[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
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
@[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₂} :
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₂] [module R M₁] [module R M₂] {Q₁ : quadratic_form R M₁} {Q₂ : quadratic_form R 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₂] [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₂)
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₂] [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₁) :
Q₂ (f m) = Q₁ 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) :

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₂] [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.

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₃] [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.

Equations
@[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) :
@[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.

Equations
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) :

A quadratic form is isometric to its bases representations.

Equations

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

Equations