Orthogonal quotients of finite bilinear modules #
Let A be a finite bilinear module and let H be an additive subgroup of it. The pairing of
A restricted to H⊥ kills the vectors of H that lie in H⊥, so it descends to the quotient
H⊥ / (H ∩ H⊥).
For an isotropic H, where H ≤ H⊥, this is the classical orthogonal quotient H⊥ / H. The
construction itself needs no isotropy hypothesis, and is given here without one; isotropy is
assumed exactly in the two places where it is used, namely the squared-order corollary and the
Lagrangian criterion.
The results are the ones the gluing theory of integral lattices asks of this quotient. It is
nondegenerate precisely when H swallows the radical of A, which for nondegenerate A is
automatic. Its order is the index of H ∩ H⊥ in H⊥, so for nondegenerate A and isotropic
H the double-complement cardinality identity |H| |H⊥| = |A| of
TauCeti.LinearAlgebra.FiniteBilinearModule.Orthogonal.Complement turns into
|H⊥ / H| · |H|² = |A|.
The quotient is trivial exactly when H⊥ ≤ H, hence — for isotropic H — exactly when H is
Lagrangian. Read through the discriminant form of an integral lattice, that last statement is
the module-level form of "an overlattice glued along a Lagrangian subgroup is unimodular".
The quadratic refinement TauCeti.FiniteQuadraticModule.orthogonalQuotient of
TauCeti.LinearAlgebra.FiniteBilinearModule.Quadratic carries a quadratic map on the same
quotient group, and its underlying bilinear module is definitionally the construction of this
file; TauCeti.FiniteQuadraticModule.orthogonalQuotient_toFiniteBilinearModule records that
identification.
Main declarations #
TauCeti.FiniteBilinearModule.orthogonalQuotient: the finite bilinear module induced onH⊥ / (H ∩ H⊥).TauCeti.FiniteBilinearModule.orthogonalQuotient_pairing_mk: its pairing, on representatives.TauCeti.FiniteBilinearModule.radical_orthogonalQuotient: its radical, as the image of the restricted radical.TauCeti.FiniteBilinearModule.isNondegenerate_orthogonalQuotient_iff: it is nondegenerate exactly whenrad(A) ≤ H.TauCeti.FiniteBilinearModule.IsNondegenerate.card_orthogonalQuotient_mul_card_sq: the order computation|H⊥ / H| · |H|² = |A|, for a nondegenerate module and an isotropic subgroup.TauCeti.FiniteBilinearModule.card_orthogonalQuotient_eq_one_iff_isLagrangian: the quotient of an isotropic subgroup is trivial exactly when that subgroup is Lagrangian.TauCeti.FiniteBilinearModule.subsingleton_orthogonalQuotient_iff_isLagrangian: the same criterion phrased asSubsingleton.TauCeti.FiniteBilinearModule.Isometry.orthogonalQuotientEquiv: transport of orthogonal quotients along an isometry carrying one subgroup onto another.
References #
- V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.4, Proposition 1.4.1.
- W. Ebeling, Lattices and Codes, Chapter 1.
The induced pairing on H⊥ / (H ∩ H⊥) #
The orthogonal quotient of a finite bilinear module. The pairing of A is restricted to
H⊥ and then divided by the part of H lying in H⊥, which is degenerate for the restricted
pairing by
TauCeti.FiniteBilinearModule.addSubgroupOf_orthogonalComplement_le_radical_restrict.
No isotropy hypothesis is needed: H ∩ H⊥ is always killed by the restricted pairing. When H
is isotropic, so that H ≤ H⊥, this is the classical H⊥ / H.
Exposed for the same reason as quotientOfLeRadical, on which it is built: so that its carrier
reduces to the Submodule quotient and maps out of it are definable with Submodule.liftQ,
Submodule.mapQ and Submodule.Quotient.equiv, and so that this package is definitionally the
underlying bilinear module of TauCeti.FiniteQuadraticModule.orthogonalQuotient.
Equations
- A.orthogonalQuotient H = (A.restrict (A.orthogonalComplement H)).quotientOfLeRadical (H.addSubgroupOf (A.orthogonalComplement H)) ⋯
Instances For
The quotient map from H⊥ onto the orthogonal quotient.
Equations
- A.orthogonalQuotientMk H = (A.restrict (A.orthogonalComplement H)).quotientOfLeRadicalMk (H.addSubgroupOf (A.orthogonalComplement H)) ⋯
Instances For
The orthogonal-quotient map sends an element to its quotient class.
The pairing of the orthogonal quotient is the pairing of A on representatives.
The quotient map onto the orthogonal quotient is surjective.
Every element of the orthogonal quotient is the class of an element of H⊥.
The radical of the orthogonal quotient is the image of the radical of the restricted pairing.
The kernel of the quotient map onto the orthogonal quotient is the part of H that lies
in H⊥.
An element of H⊥ has zero class in the orthogonal quotient exactly when it lies in H.
Two elements of H⊥ have the same class in the orthogonal quotient exactly when they differ
by an element of H.
Equal subgroups induce the same orthogonal quotient, up to the canonical isometry.
Equations
Instances For
The canonical isometry between orthogonal quotients along equal subgroups is the identity on representatives.
Nondegeneracy #
Nondegeneracy of the orthogonal quotient. The quotient H⊥ / (H ∩ H⊥) is
nondegenerate exactly when H contains the radical of A.
Only the radical can survive: an element of H⊥ orthogonal to all of H⊥ lies in H⊥⊥, which
is H enlarged by the radical.
The orthogonal quotient of a nondegenerate finite bilinear module is nondegenerate.
Order #
The order of the orthogonal quotient is the index of H ∩ H⊥ in H⊥.
The general order formula for an orthogonal quotient. In a nondegenerate finite bilinear
module, the orders of H⊥ / (H ∩ H⊥), H ∩ H⊥, and H multiply to the order of the
ambient module.
The order of the orthogonal quotient of an isotropic subgroup. In a nondegenerate finite
bilinear module, |H⊥ / H| · |H|² = |A|.
The Lagrangian criterion #
The orthogonal quotient is trivial exactly when H⊥ is contained in H. No hypothesis on
A or on H is needed.
The Lagrangian criterion. The orthogonal quotient of an isotropic subgroup is trivial exactly when that subgroup is Lagrangian.
The orthogonal quotient of an isotropic subgroup is a subsingleton exactly when that subgroup is Lagrangian.
Transport along isometries #
Transport of an orthogonal quotient along an isometry. An isometry f : A ≅ B carrying
H onto K induces an isometry H⊥ / (H ∩ H⊥) ≅ K⊥ / (K ∩ K⊥).
Equations
Instances For
The representative formula for a transported orthogonal quotient. The transported
isometry sends the class of x ∈ H⊥ to the class of f x ∈ K⊥.
The inverse representative formula for a transported orthogonal quotient. The inverse
transport sends the class of y ∈ K⊥ to the class of f⁻¹ y ∈ H⊥.