Quadratic forms #
This file defines quadratic forms over a
A quadratic form is a map
Q : M → R such that
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
Q.comp f x = Q (f x).
Main definitions #
quadratic_form.associated: associated bilinear form
quadratic_form.pos_def: positive definite quadratic forms
quadratic_form.anisotropic: anisotropic quadratic forms
quadratic_form.discr: discriminant of a quadratic form
Main statements #
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
bilin_form.exists_orthogonal_basis: There exists an orthogonal basis with respect to any nondegenerate, symmetric bilinear form
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
S is used when
R itself has a
quadratic form, homogeneous polynomial, quadratic polynomial
Up to a factor 2,
Q.polar is the associated bilinear form for a quadratic form
Source of this name: https://en.wikipedia.org/wiki/Quadratic_form#Generalization
- to_fun : M → R
- to_fun_smul : ∀ (a : R) (x : M), self.to_fun (a • x) = a * a * self.to_fun x
- polar_add_left' : ∀ (x x' y : M), quadratic_form.polar self.to_fun (x + x') y = quadratic_form.polar self.to_fun x y + quadratic_form.polar self.to_fun x' y
- polar_smul_left' : ∀ (a : R) (x y : M), quadratic_form.polar self.to_fun (a • x) y = a • quadratic_form.polar self.to_fun x y
- polar_add_right' : ∀ (x y y' : M), quadratic_form.polar self.to_fun x (y + y') = quadratic_form.polar self.to_fun x y + quadratic_form.polar self.to_fun x y'
- polar_smul_right' : ∀ (a : R) (x y : M), quadratic_form.polar self.to_fun x (a • y) = a • quadratic_form.polar self.to_fun x y
A quadratic form over a module.
Helper instance for when there's too many metavariables to apply
Copy of a
quadratic_form with a new
to_fun equal to the old one. Useful to fix definitional
quadratic_form R M inherits the scalar action from any algebra over
R is commutative, this provides an
This API mirrors
Evaluation on a particular element of the module
M is an additive map over quadratic forms.
Compose the quadratic form with a linear function.
Compose a quadratic form with a linear function on the left.
Create a quadratic form in a commutative ring by proving only one side of the bilinearity.
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
A bilinear form gives a quadratic form by applying the argument twice.
associated_hom is the map that sends a quadratic form on a module
R to its
associated symmetric bilinear form. As provided here, this has the structure of an
S is a commutative subring of
Over a commutative ring, use
associated, which gives an
R-linear map. Over a general ring with
no nontrivial distinguished commutative subring, use
associated', which gives an additive
homomorphism (or more precisely a
Symmetric bilinear forms can be lifted to quadratic forms
There exists a non-null vector with respect to any quadratic form
Q whose associated
bilinear form is non-zero, i.e. there exists
x such that
Q x ≠ 0.
The associated bilinear form of an anisotropic quadratic form is nondegenerate.
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.
An isometry between two quadratic spaces
M₁, Q₁ and
M₂, Q₂ over a ring
is a linear equivalence between
M₂ that commutes with the quadratic forms.
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.
The identity isometry from a quadratic form to itself.
The inverse isometry of an isometry between two quadratic forms.
The composition of two isometries between quadratic forms.
There exists a non-null vector with respect to any symmetric, nonzero bilinear form
on a module
M over a ring
R with invertible
2, i.e. there exists some
x : M such that
B x x ≠ 0.
Given a symmetric bilinear form
B on some vector space
V over a field
2 is invertible, there exists an orthogonal basis with respect to
A quadratic form composed with a
linear_equiv is isometric to itself.
Given a quadratic form
Q and a basis,
basis_repr is the basis representation of
A quadratic form is isometric to its bases representations.
The weighted sum of squares with respect to some weight as a quadratic form.
The weights are applied using
•; typically this definition is used either with
S = R₁ or
[algebra S R₁], although this is stated more generally.
On an orthogonal basis, the basis representation of
Q is just a sum of squares.
Given an orthogonal basis, a quadratic form is isometric with a weighted sum of squares.