mathlib documentation

linear_algebra.quadratic_form

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

Main statements

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

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
theorem quadratic_form.polar_add {R : Type u} {M : Type v} [add_comm_group M] [ring R] (f g : M → R) (x y : M) :

theorem quadratic_form.polar_neg {R : Type u} {M : Type v} [add_comm_group M] [ring R] (f : M → R) (x y : M) :

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

theorem quadratic_form.polar_comm {M : Type v} [add_comm_group M] {R₁ : Type u} [comm_ring R₁] (f : M → R₁) (x y : M) :

structure quadratic_form (R : Type u) (M : Type v) [ring R] [add_comm_group M] [module R M] :
Type (max u v)

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] :

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

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

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

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

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) :
Q (a x) = (a * a) * Q x

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) :
Q (x + x) = 4 * Q x

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} :
Q 0 = 0

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) :
Q (-x) = Q x

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) :
Q (x - y) = Q (y - x)

@[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} :
(∀ (x : M), Q x = Q' x)Q = Q'

@[instance]
def quadratic_form.has_zero {R : Type u} {M : Type v} [add_comm_group M] [ring R] [module R M] :

Equations
@[simp]
theorem quadratic_form.zero_apply {R : Type u} {M : Type v} [add_comm_group M] [ring R] [module R M] (x : M) :
0 x = 0

@[instance]
def quadratic_form.inhabited {R : Type u} {M : Type v} [add_comm_group M] [ring R] [module R M] :

Equations
@[instance]
def quadratic_form.has_add {R : Type u} {M : Type v} [add_comm_group M] [ring R] [module R M] :

Equations
@[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) :
(Q + Q') = Q + Q'

@[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) :
(Q + Q') x = Q x + Q' x

@[instance]
def quadratic_form.has_neg {R : Type u} {M : Type v} [add_comm_group M] [ring R] [module R M] :

Equations
@[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) :
(-Q) x = -Q x

@[instance]
def quadratic_form.has_scalar {M : Type v} [add_comm_group M] {R₁ : Type u} [comm_ring R₁] [module R₁ M] :

Equations
@[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) :
(a Q) = a Q

@[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) :
(a Q) x = a * Q x

@[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
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
@[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) :
(Q.comp f) x = Q (f x)

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

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

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

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) :
quadratic_form.polar (λ (x : M), B x x) x y = B x y + B y x

def bilin_form.to_quadratic_form {R : Type u} {M : Type v} [add_comm_group M] [ring R] [module R M] :

A bilinear form gives a quadratic form by applying the argument twice.

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

def quadratic_form.associated {M : Type v} [add_comm_group M] {R₁ : Type u} [comm_ring R₁] [module R₁ M] [invertible 2] :

associated is the linear map that sends a quadratic form to its associated symmetric bilinear form

Equations
@[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) :
(quadratic_form.associated Q) x y = ( 2) * (Q (x + y) - Q x - Q y)

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

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

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} :

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.

Equations
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} :
0 < a(a Q).pos_def

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) :
Q.pos_defQ'.pos_def(Q + Q').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.

Equations
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₁) :
(a Q).discr = (a ^ fintype.card n) * Q.discr

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
@[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₂} :
has_coe (Q₁.isometry Q₂) (M₁ ≃ₗ[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₂} :

Equations
@[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₁) :
Q₂ (f m) = Q₁ 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) :

The identity isometry from a quadratic form to itself.

Equations
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₂} :
Q₁.isometry Q₂Q₂.isometry Q₁

The inverse isometry of an isometry between two quadratic forms.

Equations
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₃} :
Q₁.isometry Q₂Q₂.isometry Q₃Q₁.isometry Q₃

The composition of two isometries between quadratic forms.

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

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₃