Splitting off a regular submodule #
Let (M, q) be a quadratic form over a commutative ring and N ⊆ M a submodule on which the
restriction of q is regular — its polar form is a bijection N ≃ N*. Then N splits off
orthogonally:
M = N ⊕ Nᗮ and q = q|_N ⊥ q|_{Nᗮ},
where Nᗮ is the orthogonal complement of N for the polar form of q (mathlib's
LinearMap.BilinForm.orthogonal).
Why regularity, and not less #
Regularity is used twice and both times essentially. Surjectivity of N → N* produces the
projection: the functional n ↦ q(x, n) on N is realized by an actual element of N, and
subtracting it lands x in Nᗮ. Injectivity gives N ∩ Nᗮ = 0. Neither follows from
non-singularity of q on M, and over a field of characteristic 2 the difference is not cosmetic:
the polar form of a non-singular form of odd rank has a kernel, so its span is a submodule that
does not split off.
Nothing here needs M to be projective, finitely generated, or 2 to be invertible; those enter
only in QuadraticForm.IsGPRNonsingular.comp_polarOrthogonal_subtype, where non-singularity of
the complement is deduced by base change.
Main definitions #
QuadraticForm.polarProj: the projectionM →ₗ[R] Nattached to a regular restriction.QuadraticForm.polarOrthogonal:Nᗮ, a readable spelling of mathlib'sLinearMap.BilinForm.orthogonalapplied to the polar form.QuadraticForm.orthogonalDecomposition: the linear equivalenceN × Nᗮ ≃ₗ[R] Mgiven by addition.
Main results #
QuadraticForm.orthogonalDecompositionIsometryEquiv: the orthogonal splitting packaged as an isometry equivalence.QuadraticForm.comp_orthogonalDecomposition:qpulls back toq|_N ⊥ q|_{Nᗮ}.QuadraticForm.nontrivial_baseChange_polarOrthogonal: the complement is nonzero over every field whereNis strictly smaller thanM. This is how the full-support hypothesis of the representation lemma is met in practice.QuadraticForm.IsGPRNonsingular.comp_polarOrthogonal_subtype: the complement of a regular submodule in a non-singular form is non-singular. This is what feeds the representation lemma (GPR 11.26).QuadraticForm.eq_top_of_isGPRRegular_of_rankAtStalk_eq: a regular submodule of full rank is everything — the complement has rank zero, hence vanishes.
References #
- [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 11.11, 19.16.
- [GN] Gille, Neher, Group schemes over LG-rings and applications to cancellation theorems and Azumaya algebras, European Journal of Mathematics 11 (2025), article 42, C.8.
Nᗮ, the orthogonal complement of N for the polar form of Q.
This is mathlib's LinearMap.BilinForm.orthogonal applied to QuadraticMap.polarBilin Q; the
abbreviation exists only so that statements about it are readable, and is reducible, so mathlib's
LinearMap.BilinForm.mem_orthogonal_iff applies unchanged.
Equations
Instances For
The orthogonal projection onto a regular submodule.
x is sent to the unique element of N representing the functional n ↦ q(x, n) through the
polar form of q|_N. Uniqueness — hence linearity — is exactly regularity of the restriction.
Equations
- QuadraticForm.polarProj hreg = ↑(LinearEquiv.ofBijective (QuadraticMap.comp Q N.subtype).polarBilin hreg).symm ∘ₗ N.subtype.dualMap ∘ₗ QuadraticMap.polarBilin Q
Instances For
The defining property of the projection: it does not change the polar form against N.
Every x decomposes as its projection plus a vector orthogonal to N.
The projection is the identity on N, by injectivity of the restricted polar form.
The projection kills the orthogonal complement.
M = N ⊕ Nᗮ. Addition is a linear equivalence N × Nᗮ ≃ₗ[R] M when the restriction of
q to N is regular.
Equations
Instances For
The orthogonal splitting of the form: q = q|_N ⊥ q|_{Nᗮ}.
The cross term vanishes by the definition of Nᗮ, which is the whole point.
The orthogonal decomposition packaged as an isometry between the orthogonal sum of the two restricted forms and the ambient form.
Equations
- QuadraticForm.orthogonalDecompositionIsometryEquiv hreg = { toLinearEquiv := QuadraticForm.orthogonalDecomposition hreg, map_app' := ⋯ }
Instances For
A regular submodule of a finitely generated module is finitely generated: it is a direct summand, being the image of the projection.
A regular submodule of a projective module is projective.
The complement of a regular submodule is finitely generated when the ambient module is.
The complement of a regular submodule is projective when the ambient module is.
The complement of a regular submodule in a non-singular form is non-singular.
Base change the orthogonal splitting q ≅ q|_N ⊥ q|_{Nᗮ} to a field and read off the right
summand (GN (C.8.3), QuadraticForm.IsGPRNonsingular.of_prod_right). This is the hypothesis the
representation lemma GPR 11.26 consumes.
The complement is visible in the rank. Over a field F ∈ R-alg in which N is strictly
smaller than M, the base change of the complement is nonzero.
Base change is exact on the splitting M = N ⊕ Nᗮ, so the three ranks add up; a vanishing
complement would force the two ranks to agree. This is what supplies Module.HasFullSupport for
the representation lemma GPR 11.26.
A regular submodule of full rank is everything. If the restriction of Q to N is regular
and N has the same constant rank as M at every prime, the orthogonal complement has rank zero,
hence is trivial, hence N = ⊤.
This is the criterion that turns a doubling that has run out of room into a surjection; the
subalgebra form of it is ConicAlgebra.mem_of_isGPRRegular_of_rankAtStalk_eq.