Quadratic forms
This file defines quadratic forms over a R-module M.
A quadratic form is a map Q : M → R such that
(to_fun_smul) Q (a • x) = a * a * Q x
(polar_...) The map polar Q := λ x y, Q (x + y) - Q x - Q y is bilinear.
They come with a scalar multiplication, (a • Q) x = Q (a • x) = a * a * Q x,
and composition with linear maps f, Q.comp f x = Q (f x).
Main definitions
quadratic_form.associated: associated bilinear formquadratic_form.pos_def: positive definite quadratic formsquadratic_form.discr: discriminant of a quadratic form
Main statements
quadratic_form.associated_left_inverse,quadratic_form.associated_right_inverse: in a commutative ring where 2 has an inverse, there is a correspondence between quadratic forms and symmetric bilinear forms
Notation
In this file, the variable R is used when a ring structure is sufficient and
R₁ is used when specifically a comm_ring is required. This allows us to keep
[module R M] and [module R₁ M] assumptions in the variables without
confusion between * from ring and * from comm_ring.
References
- https://en.wikipedia.org/wiki/Quadratic_form
- https://en.wikipedia.org/wiki/Discriminant#Quadratic_forms
Tags
quadratic form, homogeneous polynomial, quadratic polynomial
def
quadratic_form.polar
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R] :
(M → R) → M → M → R
Up to a factor 2, Q.polar is the associated bilinear form for a quadratic form Q.d
Source of this name: https://en.wikipedia.org/wiki/Quadratic_form#Generalization
Equations
- quadratic_form.polar f x y = f (x + y) - f x - f y
theorem
quadratic_form.polar_add
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
(f g : M → R)
(x y : M) :
quadratic_form.polar (f + g) x y = quadratic_form.polar f x y + quadratic_form.polar g x y
theorem
quadratic_form.polar_neg
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
(f : M → R)
(x y : M) :
quadratic_form.polar (-f) x y = -quadratic_form.polar f x y
theorem
quadratic_form.polar_smul
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
(f : M → R)
(s : R)
(x y : M) :
quadratic_form.polar (s • f) x y = s * quadratic_form.polar f x y
theorem
quadratic_form.polar_comm
{M : Type v}
[add_comm_group M]
{R₁ : Type u}
[comm_ring R₁]
(f : M → R₁)
(x y : M) :
quadratic_form.polar f x y = quadratic_form.polar f y x
structure
quadratic_form
(R : Type u)
(M : Type v)
[ring R]
[add_comm_group M]
[module R M] :
Type (max u v)
- to_fun : M → R
- to_fun_smul : ∀ (a : R) (x : M), c.to_fun (a • x) = a * a * c.to_fun x
- polar_add_left' : ∀ (x x' y : M), quadratic_form.polar c.to_fun (x + x') y = quadratic_form.polar c.to_fun x y + quadratic_form.polar c.to_fun x' y
- polar_smul_left' : ∀ (a : R) (x y : M), quadratic_form.polar c.to_fun (a • x) y = a • quadratic_form.polar c.to_fun x y
- polar_add_right' : ∀ (x y y' : M), quadratic_form.polar c.to_fun x (y + y') = quadratic_form.polar c.to_fun x y + quadratic_form.polar c.to_fun x y'
- polar_smul_right' : ∀ (a : R) (x y : M), quadratic_form.polar c.to_fun x (a • y) = a • quadratic_form.polar c.to_fun x y
A quadratic form over a module.
@[instance]
def
quadratic_form.has_coe_to_fun
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M] :
has_coe_to_fun (quadratic_form R M)
Equations
- quadratic_form.has_coe_to_fun = {F := λ (B : quadratic_form R M), M → R, coe := λ (B : quadratic_form R M), B.to_fun}
@[simp]
theorem
quadratic_form.to_fun_eq_apply
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
{Q : quadratic_form R M} :
The simp normal form for a quadratic form is coe_fn, not to_fun.
@[simp]
theorem
quadratic_form.polar_add_left
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
{Q : quadratic_form R M}
(x x' y : M) :
quadratic_form.polar ⇑Q (x + x') y = quadratic_form.polar ⇑Q x y + quadratic_form.polar ⇑Q x' y
@[simp]
theorem
quadratic_form.polar_smul_left
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
{Q : quadratic_form R M}
(a : R)
(x y : M) :
quadratic_form.polar ⇑Q (a • x) y = a * quadratic_form.polar ⇑Q x y
@[simp]
theorem
quadratic_form.polar_add_right
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
{Q : quadratic_form R M}
(x y y' : M) :
quadratic_form.polar ⇑Q x (y + y') = quadratic_form.polar ⇑Q x y + quadratic_form.polar ⇑Q x y'
@[simp]
theorem
quadratic_form.polar_smul_right
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
{Q : quadratic_form R M}
(a : R)
(x y : M) :
quadratic_form.polar ⇑Q x (a • y) = a * quadratic_form.polar ⇑Q x y
theorem
quadratic_form.map_smul
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
{Q : quadratic_form R M}
(a : R)
(x : M) :
theorem
quadratic_form.map_add_self
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
{Q : quadratic_form R M}
(x : M) :
theorem
quadratic_form.map_zero
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
{Q : quadratic_form R M} :
theorem
quadratic_form.map_neg
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
{Q : quadratic_form R M}
(x : M) :
theorem
quadratic_form.map_sub
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
{Q : quadratic_form R M}
(x y : M) :
@[ext]
theorem
quadratic_form.ext
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
{Q Q' : quadratic_form R M} :
@[instance]
def
quadratic_form.has_zero
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M] :
has_zero (quadratic_form R M)
Equations
- quadratic_form.has_zero = {zero := {to_fun := λ (x : M), 0, to_fun_smul := _, polar_add_left' := _, polar_smul_left' := _, polar_add_right' := _, polar_smul_right' := _}}
@[simp]
theorem
quadratic_form.zero_apply
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
(x : M) :
@[instance]
def
quadratic_form.inhabited
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M] :
inhabited (quadratic_form R M)
Equations
@[instance]
def
quadratic_form.has_add
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M] :
has_add (quadratic_form R M)
Equations
- quadratic_form.has_add = {add := λ (Q Q' : quadratic_form R M), {to_fun := ⇑Q + ⇑Q', to_fun_smul := _, polar_add_left' := _, polar_smul_left' := _, polar_add_right' := _, polar_smul_right' := _}}
@[simp]
theorem
quadratic_form.coe_fn_add
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
(Q Q' : quadratic_form R M) :
@[simp]
theorem
quadratic_form.add_apply
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
(Q Q' : quadratic_form R M)
(x : M) :
@[instance]
def
quadratic_form.has_neg
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M] :
has_neg (quadratic_form R M)
Equations
- quadratic_form.has_neg = {neg := λ (Q : quadratic_form R M), {to_fun := -⇑Q, to_fun_smul := _, polar_add_left' := _, polar_smul_left' := _, polar_add_right' := _, polar_smul_right' := _}}
@[simp]
theorem
quadratic_form.coe_fn_neg
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
(Q : quadratic_form R M) :
@[simp]
theorem
quadratic_form.neg_apply
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
(Q : quadratic_form R M)
(x : M) :
@[instance]
def
quadratic_form.has_scalar
{M : Type v}
[add_comm_group M]
{R₁ : Type u}
[comm_ring R₁]
[module R₁ M] :
has_scalar R₁ (quadratic_form R₁ M)
Equations
- quadratic_form.has_scalar = {smul := λ (a : R₁) (Q : quadratic_form R₁ M), {to_fun := a • ⇑Q, to_fun_smul := _, polar_add_left' := _, polar_smul_left' := _, polar_add_right' := _, polar_smul_right' := _}}
@[simp]
theorem
quadratic_form.coe_fn_smul
{M : Type v}
[add_comm_group M]
{R₁ : Type u}
[comm_ring R₁]
[module R₁ M]
(a : R₁)
(Q : quadratic_form R₁ M) :
@[simp]
theorem
quadratic_form.smul_apply
{M : Type v}
[add_comm_group M]
{R₁ : Type u}
[comm_ring R₁]
[module R₁ M]
(a : R₁)
(Q : quadratic_form R₁ M)
(x : M) :
@[instance]
def
quadratic_form.add_comm_group
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M] :
add_comm_group (quadratic_form R M)
Equations
- quadratic_form.add_comm_group = {add := has_add.add quadratic_form.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, neg := has_neg.neg quadratic_form.has_neg, add_left_neg := _, add_comm := _}
@[instance]
def
quadratic_form.module
{M : Type v}
[add_comm_group M]
{R₁ : Type u}
[comm_ring R₁]
[module R₁ M] :
module R₁ (quadratic_form R₁ M)
Equations
- quadratic_form.module = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := quadratic_form.has_scalar _inst_5, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
def
quadratic_form.comp
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
{N : Type v}
[add_comm_group N]
[module R N] :
quadratic_form R N → (M →ₗ[R] N) → quadratic_form R M
Compose the quadratic form with a linear function.
Equations
- Q.comp f = {to_fun := λ (x : M), ⇑Q (⇑f x), to_fun_smul := _, polar_add_left' := _, polar_smul_left' := _, polar_add_right' := _, polar_smul_right' := _}
@[simp]
theorem
quadratic_form.comp_apply
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
{N : Type v}
[add_comm_group N]
[module R N]
(Q : quadratic_form R N)
(f : M →ₗ[R] N)
(x : M) :
def
quadratic_form.mk_left
{M : Type v}
[add_comm_group M]
{R₁ : Type u}
[comm_ring R₁]
[module R₁ M]
(f : M → R₁) :
(∀ (a : R₁) (x : M), f (a • x) = a * a * f x) → (∀ (x x' y : M), quadratic_form.polar f (x + x') y = quadratic_form.polar f x y + quadratic_form.polar f x' y) → (∀ (a : R₁) (x y : M), quadratic_form.polar f (a • x) y = a * quadratic_form.polar f x y) → quadratic_form R₁ M
Create a quadratic form in a commutative ring by proving only one side of the bilinearity.
Equations
- quadratic_form.mk_left f to_fun_smul polar_add_left polar_smul_left = {to_fun := f, to_fun_smul := to_fun_smul, polar_add_left' := polar_add_left, polar_smul_left' := polar_smul_left, polar_add_right' := _, polar_smul_right' := _}
def
quadratic_form.lin_mul_lin
{M : Type v}
[add_comm_group M]
{R₁ : Type u}
[comm_ring R₁]
[module R₁ M] :
(M →ₗ[R₁] R₁) → (M →ₗ[R₁] R₁) → quadratic_form R₁ M
The product of linear forms is a quadratic form.
Equations
- quadratic_form.lin_mul_lin f g = quadratic_form.mk_left (⇑f * ⇑g) _ _ _
@[simp]
theorem
quadratic_form.lin_mul_lin_apply
{M : Type v}
[add_comm_group M]
{R₁ : Type u}
[comm_ring R₁]
[module R₁ M]
(f g : M →ₗ[R₁] R₁)
(x : M) :
@[simp]
theorem
quadratic_form.add_lin_mul_lin
{M : Type v}
[add_comm_group M]
{R₁ : Type u}
[comm_ring R₁]
[module R₁ M]
(f g h : M →ₗ[R₁] R₁) :
quadratic_form.lin_mul_lin (f + g) h = quadratic_form.lin_mul_lin f h + quadratic_form.lin_mul_lin g h
@[simp]
theorem
quadratic_form.lin_mul_lin_add
{M : Type v}
[add_comm_group M]
{R₁ : Type u}
[comm_ring R₁]
[module R₁ M]
(f g h : M →ₗ[R₁] R₁) :
quadratic_form.lin_mul_lin f (g + h) = quadratic_form.lin_mul_lin f g + quadratic_form.lin_mul_lin f h
@[simp]
theorem
quadratic_form.lin_mul_lin_comp
{M : Type v}
[add_comm_group M]
{R₁ : Type u}
[comm_ring R₁]
[module R₁ M]
{N : Type v}
[add_comm_group N]
[module R₁ N]
(f g : M →ₗ[R₁] R₁)
(h : N →ₗ[R₁] M) :
(quadratic_form.lin_mul_lin f g).comp h = quadratic_form.lin_mul_lin (f.comp h) (g.comp h)
def
quadratic_form.proj
{R₁ : Type u}
[comm_ring R₁]
{n : Type u_1} :
n → n → quadratic_form R₁ (n → R₁)
proj i j is the quadratic form mapping the vector x : n → R₁ to x i * x j
Equations
@[simp]
theorem
quadratic_form.proj_apply
{R₁ : Type u}
[comm_ring R₁]
{n : Type u_1}
(i j : n)
(x : n → R₁) :
⇑(quadratic_form.proj i j) x = x i * x j
Associated bilinear forms
Over a commutative ring with an inverse of 2, the theory of quadratic forms is
basically identical to that of symmetric bilinear forms. The map from quadratic
forms to bilinear forms giving this identification is called the associated
quadratic form.
theorem
bilin_form.polar_to_quadratic_form
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
{B : bilin_form R M}
(x y : M) :
def
bilin_form.to_quadratic_form
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M] :
bilin_form R M → quadratic_form R M
A bilinear form gives a quadratic form by applying the argument twice.
Equations
- B.to_quadratic_form = {to_fun := λ (x : M), ⇑B x x, to_fun_smul := _, polar_add_left' := _, polar_smul_left' := _, polar_add_right' := _, polar_smul_right' := _}
@[simp]
theorem
bilin_form.to_quadratic_form_apply
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
(B : bilin_form R M)
(x : M) :
⇑(B.to_quadratic_form) x = ⇑B x x
def
quadratic_form.associated
{M : Type v}
[add_comm_group M]
{R₁ : Type u}
[comm_ring R₁]
[module R₁ M]
[invertible 2] :
quadratic_form R₁ M →ₗ[R₁] bilin_form R₁ M
associated is the linear map that sends a quadratic form to its associated
symmetric bilinear form
Equations
- quadratic_form.associated = {to_fun := λ (Q : quadratic_form R₁ M), {bilin := λ (x y : M), ⅟ 2 * quadratic_form.polar ⇑Q x y, bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}, map_add' := _, map_smul' := _}
@[simp]
theorem
quadratic_form.associated_apply
{M : Type v}
[add_comm_group M]
{R₁ : Type u}
[comm_ring R₁]
[module R₁ M]
[invertible 2]
{Q : quadratic_form R₁ M}
(x y : M) :
theorem
quadratic_form.associated_is_sym
{M : Type v}
[add_comm_group M]
{R₁ : Type u}
[comm_ring R₁]
[module R₁ M]
[invertible 2]
{Q : quadratic_form R₁ M} :
@[simp]
theorem
quadratic_form.associated_comp
{M : Type v}
[add_comm_group M]
{R₁ : Type u}
[comm_ring R₁]
[module R₁ M]
[invertible 2]
{Q : quadratic_form R₁ M}
{N : Type v}
[add_comm_group N]
[module R₁ N]
(f : N →ₗ[R₁] M) :
⇑quadratic_form.associated (Q.comp f) = (⇑quadratic_form.associated Q).comp f f
@[simp]
theorem
quadratic_form.associated_lin_mul_lin
{M : Type v}
[add_comm_group M]
{R₁ : Type u}
[comm_ring R₁]
[module R₁ M]
[invertible 2]
(f g : M →ₗ[R₁] R₁) :
⇑quadratic_form.associated (quadratic_form.lin_mul_lin f g) = ⅟ 2 • (bilin_form.lin_mul_lin f g + bilin_form.lin_mul_lin g f)
theorem
quadratic_form.associated_to_quadratic_form
{M : Type v}
[add_comm_group M]
{R₁ : Type u}
[comm_ring R₁]
[module R₁ M]
[invertible 2]
(B : bilin_form R₁ M)
(x y : M) :
⇑(⇑quadratic_form.associated B.to_quadratic_form) x y = ⅟ 2 * (⇑B x y + ⇑B y x)
theorem
quadratic_form.associated_left_inverse
{M : Type v}
[add_comm_group M]
{R₁ : Type u}
[comm_ring R₁]
[module R₁ M]
[invertible 2]
{B₁ : bilin_form R₁ M} :
theorem
quadratic_form.associated_right_inverse
{M : Type v}
[add_comm_group M]
{R₁ : Type u}
[comm_ring R₁]
[module R₁ M]
[invertible 2]
{Q : quadratic_form R₁ M} :
def
quadratic_form.pos_def
{M : Type v}
[add_comm_group M]
{R₂ : Type u}
[ordered_ring R₂]
[module R₂ M] :
quadratic_form R₂ M → Prop
A positive definite quadratic form is positive on nonzero vectors.
theorem
quadratic_form.pos_def.smul
{M : Type v}
[add_comm_group M]
{R : Type u_1}
[linear_ordered_comm_ring R]
[module R M]
{Q : quadratic_form R M}
(h : Q.pos_def)
{a : R} :
theorem
quadratic_form.pos_def.add
{M : Type v}
[add_comm_group M]
{R₂ : Type u}
[ordered_ring R₂]
[module R₂ M]
(Q Q' : quadratic_form R₂ M) :
theorem
quadratic_form.lin_mul_lin_self_pos_def
{M : Type v}
[add_comm_group M]
{R : Type u_1}
[linear_ordered_comm_ring R]
[module R M]
(f : M →ₗ[R] R) :
f.ker = ⊥ → (quadratic_form.lin_mul_lin f f).pos_def
Quadratic forms and matrices
Connect quadratic forms and matrices, in order to explicitly compute with them. The convention is twos out, so there might be a factor 2⁻¹ in the entries of the matrix. The determinant of the matrix is the discriminant of the quadratic form.
def
matrix.to_quadratic_form
{R₁ : Type u}
[comm_ring R₁]
{n : Type w}
[fintype n] :
matrix n n R₁ → quadratic_form R₁ (n → R₁)
M.to_quadratic_form is the map λ x, col x ⬝ M ⬝ row x as a quadratic form.
Equations
def
quadratic_form.to_matrix
{R₁ : Type u}
[comm_ring R₁]
{n : Type w}
[fintype n]
[decidable_eq n]
[invertible 2] :
quadratic_form R₁ (n → R₁) → matrix n n R₁
A matrix representation of the quadratic form.
Equations
theorem
quadratic_form.to_matrix_smul
{R₁ : Type u}
[comm_ring R₁]
{n : Type w}
[fintype n]
[decidable_eq n]
[invertible 2]
(a : R₁)
(Q : quadratic_form R₁ (n → R₁)) :
@[simp]
theorem
quadratic_form.to_matrix_comp
{R₁ : Type u}
[comm_ring R₁]
{n : Type w}
[fintype n]
[decidable_eq n]
[invertible 2]
{m : Type w}
[decidable_eq m]
[fintype m]
(Q : quadratic_form R₁ (m → R₁))
(f : (n → R₁) →ₗ[R₁] m → R₁) :
def
quadratic_form.discr
{R₁ : Type u}
[comm_ring R₁]
{n : Type w}
[fintype n]
[decidable_eq n]
[invertible 2] :
quadratic_form R₁ (n → R₁) → R₁
The discriminant of a quadratic form generalizes the discriminant of a quadratic polynomial.
theorem
quadratic_form.discr_smul
{R₁ : Type u}
[comm_ring R₁]
{n : Type w}
[fintype n]
[decidable_eq n]
[invertible 2]
{Q : quadratic_form R₁ (n → R₁)}
(a : R₁) :
theorem
quadratic_form.discr_comp
{R₁ : Type u}
[comm_ring R₁]
{n : Type w}
[fintype n]
[decidable_eq n]
[invertible 2]
{Q : quadratic_form R₁ (n → R₁)}
(f : (n → R₁) →ₗ[R₁] n → R₁) :
@[nolint]
structure
quadratic_form.isometry
{R : Type u}
[ring R]
{M₁ : Type u_1}
{M₂ : Type u_2}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂] :
quadratic_form R M₁ → quadratic_form R M₂ → Type (max u_1 u_2)
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.
def
quadratic_form.equivalent
{R : Type u}
[ring R]
{M₁ : Type u_1}
{M₂ : Type u_2}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂] :
quadratic_form R M₁ → 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₂)
@[instance]
def
quadratic_form.isometry.has_coe
{R : Type u}
[ring R]
{M₁ : Type u_1}
{M₂ : Type u_2}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂} :
Equations
@[instance]
def
quadratic_form.isometry.has_coe_to_fun
{R : Type u}
[ring R]
{M₁ : Type u_1}
{M₂ : Type u_2}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂} :
has_coe_to_fun (Q₁.isometry Q₂)
@[simp]
theorem
quadratic_form.isometry.map_app
{R : Type u}
[ring R]
{M₁ : Type u_1}
{M₂ : Type u_2}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
(f : Q₁.isometry Q₂)
(m : M₁) :
def
quadratic_form.isometry.refl
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[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' := _}
def
quadratic_form.isometry.symm
{R : Type u}
[ring R]
{M₁ : Type u_1}
{M₂ : Type u_2}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂} :
The inverse isometry of an isometry between two quadratic forms.
def
quadratic_form.isometry.trans
{R : Type u}
[ring R]
{M₁ : Type u_1}
{M₂ : Type u_2}
{M₃ : Type u_3}
[add_comm_group M₁]
[add_comm_group M₂]
[add_comm_group 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₃} :
The composition of two isometries between quadratic forms.
theorem
quadratic_form.equivalent.refl
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
(Q : quadratic_form R M) :
Q.equivalent Q
theorem
quadratic_form.equivalent.symm
{R : Type u}
[ring R]
{M₁ : Type u_1}
{M₂ : Type u_2}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂} :
Q₁.equivalent Q₂ → Q₂.equivalent Q₁
theorem
quadratic_form.equivalent.trans
{R : Type u}
[ring R]
{M₁ : Type u_1}
{M₂ : Type u_2}
{M₃ : Type u_3}
[add_comm_group M₁]
[add_comm_group M₂]
[add_comm_group 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₃} :
Q₁.equivalent Q₂ → Q₂.equivalent Q₃ → Q₁.equivalent Q₃