Sesquilinear form #
This files provides properties about sesquilinear forms. The maps considered are of the form
M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R, where
I₁ : R₁ →+* R and
I₂ : R₂ →+* R are ring homomorphisms and
M₁ is a module over
M₂ is a module over
Sesquilinear forms are the special case that
M₁ = M₂,
R₁ = R₂ = R, and
I₁ = RingHom.id R.
I₂ = RingHom.id R, then one obtains bilinear forms.
These forms are a special case of the bilinear maps defined in
BilinearMap.lean and all basic
lemmas about construction and elementary calculations are found there.
Main declarations #
IsOrtho: states that two vectors are orthogonal with respect to a sesquilinear form
IsAlt: states that a sesquilinear form is symmetric and alternating, respectively
orthogonalBilin: provides the orthogonal complement with respect to sesquilinear form
Orthogonal vectors #
The proposition that two elements of a sesquilinear form space are orthogonal
A set of vectors
v is orthogonal with respect to some bilinear form
B if and only
if for all
i ≠ j,
B (v i) (v j) = 0. For orthogonality between two elements, use
A set of orthogonal vectors
v with respect to some sesquilinear form
B is linearly
independent if for all
B (v i) (v i) ≠ 0.
Reflexive bilinear forms #
Symmetric bilinear forms #
Alternating bilinear forms #
The orthogonal complement #
The orthogonal complement of a submodule
N with respect to some bilinear form is the set of
x which are orthogonal to all elements of
N; i.e., for all
B x y = 0.
Note that for general (neither symmetric nor antisymmetric) bilinear forms this definition has a
chirality; in addition to this "left" orthogonal complement one could define a "right" orthogonal
complement for which, for all
B y x = 0. This variant definition is not currently
provided in mathlib.
Given a bilinear form
B and some
x such that
B x x ≠ 0, the span of the singleton of
is complement to its orthogonal complement.
Adjoint pairs #
Given a pair of modules equipped with bilinear forms, this is the condition for a pair of maps between them to be mutually adjoint.
Self-adjoint pairs #
The condition for an endomorphism to be "self-adjoint" with respect to a pair of bilinear forms on the underlying module. In the case that these two forms are identical, this is the usual concept of self adjointness. In the case that one of the forms is the negation of the other, this is the usual concept of skew adjointness.
Nondegenerate bilinear forms #
A bilinear form is called left-separating if
the only element that is left-orthogonal to every other element is
for every nonzero
M₁, there exists
B x y ≠ 0.
In a non-trivial module, zero is not non-degenerate.
A bilinear form is called right-separating if
the only element that is right-orthogonal to every other element is
for every nonzero
M₂, there exists
B x y ≠ 0.
A bilinear form is called non-degenerate if it is left-separating and right-separating.
A bilinear form is left-separating if and only if it has a trivial kernel.
A bilinear form is right-separating if and only if its flip has a trivial kernel.
An orthogonal basis with respect to a left-separating bilinear form has no self-orthogonal elements.
An orthogonal basis with respect to a right-separating bilinear form has no self-orthogonal elements.
Given an orthogonal basis with respect to a bilinear form, the bilinear form is left-separating if the basis has no elements which are self-orthogonal.
Given an orthogonal basis with respect to a bilinear form, the bilinear form is right-separating if the basis has no elements which are self-orthogonal.
Given an orthogonal basis with respect to a bilinear form, the bilinear form is nondegenerate if the basis has no elements which are self-orthogonal.