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).
quadratic_form.associated: associated bilinear form
quadratic_form.pos_def: positive definite quadratic forms
quadratic_form.discr: discriminant of a quadratic form
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
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
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), 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.
Compose the quadratic form with a linear function.
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 is the linear map that sends a quadratic form to its associated
symmetric bilinear form
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.