Quadratic forms #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines quadratic forms over a
A quadratic form on a ring
R is a map
Q : M → R such that:
Q (a • x) = a * a * Q x
quadratic_form.polar_smul_right: the map
quadratic_form.polar Q := λ x y, Q (x + y) - Q x - Q yis bilinear.
This notion generalizes to semirings using the approach in [izhakian2016] which requires that
there be a (possibly non-unique) companion bilinear form
B such that
∀ x y, Q (x + y) = Q x + Q y + B x y. Over a ring, this
B is precisely
Quadratic forms 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.of_polar: a more familiar constructor that works on rings
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
Auxiliary lemma to express bilinearity of
quadratic_form.polar without subtraction.
- to_fun : M → R
- to_fun_smul : ∀ (a : R) (x : M), self.to_fun (a • x) = a * a * self.to_fun x
- exists_companion' : ∃ (B : bilin_form R M), ∀ (x y : M), self.to_fun (x + y) = self.to_fun x + self.to_fun y + ⇑B x y
A quadratic form over a module.
For a more familiar constructor when
R is a ring, see
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.polar as a bilinear form
An alternative constructor to
quadratic_form.mk, for rings where
polar can be used.
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.
- quadratic_form.add_comm_group = function.injective.add_comm_group coe_fn quadratic_form.add_comm_group._proof_3 quadratic_form.add_comm_group._proof_4 quadratic_form.add_comm_group._proof_5 quadratic_form.coe_fn_neg quadratic_form.coe_fn_sub quadratic_form.add_comm_group._proof_6 quadratic_form.add_comm_group._proof_7
Compose the quadratic form with a linear function.
Compose a quadratic form with a linear function on the left.
The product of linear forms is a quadratic form.
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.
bilin_form.to_quadratic_form as an additive homomorphism
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.
associated is the linear map that sends a quadratic form over a commutative ring to its
associated symmetric bilinear form.
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.
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
Given a quadratic form
Q and a basis,
basis_repr is the basis representation of
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.