Quadratic forms #
This file defines quadratic forms over a R
-module M
.
A quadratic form on a ring R
is a map Q : M → R
such that:
QuadraticForm.map_smul
:Q (a • x) = a * a * Q x
QuadraticForm.polar_add_left
,QuadraticForm.polar_add_right
,QuadraticForm.polar_smul_left
,QuadraticForm.polar_smul_right
: the mapQuadraticForm.polar Q := fun x y ↦ Q (x + y) - Q x - Q y
is 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 QuadraticForm.polar Q
.
To build a QuadraticForm
from the polar
axioms, use QuadraticForm.ofPolar
.
Quadratic forms 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 #
QuadraticForm.ofPolar
: a more familiar constructor that works on ringsQuadraticForm.associated
: associated bilinear formQuadraticForm.PosDef
: positive definite quadratic formsQuadraticForm.Anisotropic
: anisotropic quadratic formsQuadraticForm.discr
: discriminant of a quadratic form
Main statements #
QuadraticForm.associated_left_inverse
,QuadraticForm.associated_rightInverse
: in a commutative ring where 2 has an inverse, there is a correspondence between quadratic forms and symmetric bilinear formsBilinForm.exists_orthogonal_basis
: There exists an orthogonal basis with respect to any nondegenerate, symmetric bilinear formB
.
Notation #
In this file, the variable R
is used when a Ring
structure is sufficient and
R₁
is used when specifically a CommRing
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 CommRing
.
The variable S
is used when R
itself has a •
action.
References #
- https://en.wikipedia.org/wiki/Quadratic_form
- https://en.wikipedia.org/wiki/Discriminant#Quadratic_forms
Tags #
quadratic form, homogeneous polynomial, quadratic polynomial
Up to a factor 2, Q.polar
is the associated bilinear form for a quadratic form Q
.
Source of this name: https://en.wikipedia.org/wiki/Quadratic_form#Generalization
Instances For
Auxiliary lemma to express bilinearity of QuadraticForm.polar
without subtraction.
- toFun : M → R
- toFun_smul : ∀ (a : R) (x : M), QuadraticForm.toFun s (a • x) = a * a * QuadraticForm.toFun s x
- exists_companion' : ∃ B, ∀ (x y : M), QuadraticForm.toFun s (x + y) = QuadraticForm.toFun s x + QuadraticForm.toFun s y + BilinForm.bilin B x y
A quadratic form over a module.
For a more familiar constructor when R
is a ring, see QuadraticForm.ofPolar
.
Instances For
Helper instance for when there's too many metavariables to apply
FunLike.hasCoeToFun
directly.
The simp
normal form for a quadratic form is FunLike.coe
, not toFun
.
Copy of a QuadraticForm
with a new toFun
equal to the old one. Useful to fix definitional
equalities.
Instances For
QuadraticForm.polar
as a bilinear form
Instances For
An alternative constructor to QuadraticForm.mk
, for rings where polar
can be used.
Instances For
In a ring the companion bilinear form is unique and equal to QuadraticForm.polar
.
QuadraticForm R M
inherits the scalar action from any algebra over R
.
When R
is commutative, this provides an R
-action via Algebra.id
.
@CoeFn (QuadraticForm R M)
as an AddMonoidHom
.
This API mirrors AddMonoidHom.coeFn
.
Instances For
Evaluation on a particular element of the module M
is an additive map over quadratic forms.
Instances For
Compose the quadratic form with a linear function.
Instances For
Compose a quadratic form with a linear function on the left.
Instances For
The product of linear forms is a quadratic form.
Instances For
sq
is the quadratic form mapping the vector x : R₁
to x * x
Instances For
proj i j
is the quadratic form mapping the vector x : n → R₁
to x i * x j
Instances For
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.
A bilinear form gives a quadratic form by applying the argument twice.
Instances For
BilinForm.toQuadraticForm
as an additive homomorphism
Instances For
BilinForm.toQuadraticForm
as a linear map
Instances For
associatedHom
is the map that sends a quadratic form on a module M
over R
to its
associated symmetric bilinear form. As provided here, this has the structure of an S
-linear map
where S
is a commutative subring of R
.
Over a commutative ring, use QuadraticForm.associated
, which gives an R
-linear map. Over a
general ring with no nontrivial distinguished commutative subring, use QuadraticForm.associated'
,
which gives an additive homomorphism (or more precisely a ℤ
-linear map.)
Instances For
associated'
is the ℤ
-linear map that sends a quadratic form on a module M
over R
to its
associated symmetric bilinear form.
Instances For
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.
Instances For
An anisotropic quadratic form is zero only on zero vectors.
Instances For
The associated bilinear form of an anisotropic quadratic form is nondegenerate.
A positive definite quadratic form is positive on nonzero vectors.
Instances For
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.
M.toQuadraticForm'
is the map fun x ↦ col x * M * row x
as a quadratic form.
Instances For
A matrix representation of the quadratic form.
Instances For
The discriminant of a quadratic form generalizes the discriminant of a quadratic polynomial.
Instances For
A bilinear form is nondegenerate if the quadratic form it is associated with is anisotropic.
There exists a non-null vector with respect to any symmetric, nonzero bilinear form B
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 K
in which 2
is invertible, there exists an orthogonal basis with respect to B
.
Given a quadratic form Q
and a basis, basisRepr
is the basis representation of Q
.
Instances For
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.
Instances For
On an orthogonal basis, the basis representation of Q
is just a sum of squares.