Finite quadratic modules #
A finite quadratic module is a finite abelian group equipped with a quadratic map to ℚ/ℤ.
It extends the finite bilinear module of its symmetric pairing, and the field polar_eq_pairing'
requires that stored pairing to be the polar form of the quadratic map, so the quadratic map
determines it. This file develops restriction, form negation, orthogonal products, morphisms,
isometries, quadratic-isotropic subgroups, and quadratic Lagrangians.
The convention is the half-norm convention used for discriminant forms: for an even integral
lattice the quadratic value of a dual class represented by x is B(x, x) / 2 modulo ℤ, and
the polar pairing is therefore B(x, y) modulo ℤ.
Main definitions #
TauCeti.FiniteQuadraticModule: a finite abelian group with anAddCircle (1 : ℚ)-valued quadratic map.TauCeti.FiniteQuadraticModule.ofQuadraticMap: the finite quadratic module presented by a quadratic map on a finite abelian group.TauCeti.FiniteQuadraticModule.toFiniteBilinearModule: the canonical polar bilinear module.TauCeti.FiniteQuadraticModule.Hom: a quadratic-map-preserving additive homomorphism.TauCeti.FiniteQuadraticModule.Isometry: a quadratic-map isometric equivalence.TauCeti.FiniteQuadraticModule.IsIsotropic: quadratic isotropy of an additive subgroup.TauCeti.FiniteQuadraticModule.isIsotropic_prod_iff: quadratic isotropy of a product subgroup in an orthogonal direct sum is quadratic isotropy of each factor subgroup.TauCeti.FiniteQuadraticModule.IsLagrangian: a quadratic-isotropic subgroup equal to its bilinear orthogonal complement.TauCeti.FiniteQuadraticModule.orthogonalQuotient: the quadratic module induced onH^⊥ / Hby a quadratic-isotropic subgroupH. Its underlying bilinear module isTauCeti.FiniteBilinearModule.orthogonalQuotient, as recorded byTauCeti.FiniteQuadraticModule.orthogonalQuotient_toFiniteBilinearModule.TauCeti.FiniteQuadraticModule.orthogonalQuotientCongr: the canonical isometry between the orthogonal quotients along equal subgroups.TauCeti.FiniteQuadraticModule.Isometry.orthogonalQuotientEquiv: transport of an orthogonal quotient along an isometry carrying one isotropic subgroup onto another.
References #
- V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.1.
- W. Ebeling, Lattices and Codes, Chapter 1.
A finite abelian group equipped with a quadratic map to ℚ/ℤ.
The associated bilinear pairing is required to be the polar form, so the quadratic map determines all pairing values.
- addCommGroup : AddCommGroup self.carrier
- quadratic : QuadraticMap ℤ self.carrier (AddCircle 1)
The
ℚ/ℤ-valued quadratic map. - polar_eq_pairing' (x y : self.carrier) : QuadraticMap.polar (⇑self.quadratic) x y = (self.pairing x) y
The polar form is the stored bilinear pairing.
Instances For
A finite quadratic module coerces to its underlying type.
Equations
- TauCeti.FiniteQuadraticModule.instCoeSortType = { coe := fun (A : TauCeti.FiniteQuadraticModule) => A.carrier }
The finite quadratic module presented by a quadratic map on a finite abelian group. The pairing is the polar form, which is what the structure demands anyway, so no data beyond the quadratic map is needed.
Exposed for the same reason as quotientOfLeQuadraticRadical: so that its carrier reduces to the
given group and maps into or out of it are definable.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The polar of the quadratic map is the pairing of the underlying finite bilinear module.
The quadratic value of an integral combination m • x + n • y, expanded in terms of the
quadratic values of x and y and their pairing.
Twice the order of the underlying group kills every quadratic value.
The bilinear map of the underlying finite bilinear module is exactly the polar bilinear map.
A finite quadratic module is nondegenerate when its polar pairing is nondegenerate.
Equations
Instances For
The quadratic radical of a nondegenerate finite quadratic module is trivial: an element of the radical pairs to zero with everything under the polar pairing.
Morphisms and isometries #
A morphism of finite quadratic modules is an additive homomorphism preserving the quadratic map.
This is Mathlib's QuadraticMap.Isometry applied to the stored quadratic maps.
Instances For
The identity morphism of a finite quadratic module.
Instances For
The composite of two finite quadratic module morphisms.
Equations
- g.comp f = QuadraticMap.Isometry.comp g f
Instances For
Two finite quadratic module morphisms are equal when they agree on every element.
A morphism of finite quadratic modules preserves the canonical polar pairing.
A quadratic-module morphism induces a morphism of the canonical polar bilinear modules.
Equations
- f.toFiniteBilinearModule = { toAddMonoidHom := f.toAddMonoidHom, map_pairing' := ⋯ }
Instances For
Forgetting the identity quadratic morphism gives the identity bilinear morphism.
Forgetting a composite quadratic morphism gives the composite bilinear morphism.
An isometry of finite quadratic modules is Mathlib's isometric equivalence of their quadratic maps.
Equations
- A.Isometry B = A.quadratic.IsometryEquiv B.quadratic
Instances For
Applying a composite quadratic isometry applies its two factors in order.
A quadratic isometry is, after forgetting bijectivity, a morphism.
Equations
Instances For
The additive homomorphism underlying f.toHom is that of the additive equivalence of f.
Forgetting the identity quadratic isometry gives the identity quadratic morphism.
Forgetting a composite quadratic isometry gives the composite quadratic morphism.
The underlying morphism of a quadratic isometry is bijective.
A quadratic isometry induces an isometry of the canonical polar bilinear modules.
Equations
- f.toFiniteBilinearModule = { toAddEquiv := f.toAddEquiv, map_pairing' := ⋯ }
Instances For
The induced bilinear isometry has the same underlying additive equivalence.
Nondegeneracy transfers along a quadratic isometry.
Nondegeneracy is invariant under quadratic isometry.
A bijective morphism of finite quadratic modules is an isometry.
Equations
- f.toIsometry hf = { toLinearEquiv := (AddEquiv.ofBijective f.toAddMonoidHom hf).toIntLinearEquiv, map_app' := ⋯ }
Instances For
Forgetting a bijective morphism after packaging it as an isometry recovers the morphism.
Packaging the underlying morphism of an isometry recovers the isometry.
Canonical constructions #
Restrict a finite quadratic module to an additive subgroup.
No nondegeneracy conclusion is asserted: the polar pairing can become degenerate after restriction.
Equations
Instances For
Taking the polar bilinear module commutes with restriction.
The inclusion of a restricted finite quadratic module into the original module.
Equations
- A.restrictHom H = { toLinearMap := (AddSubgroup.toIntSubmodule H).subtype, map_app' := ⋯ }
Instances For
Forgetting the quadratic structure of a restriction inclusion gives the bilinear restriction inclusion.
Negate the quadratic map of a finite quadratic module.
Equations
Instances For
Taking the polar bilinear module commutes with form negation.
Form negation preserves nondegeneracy.
The orthogonal product of two finite quadratic modules.
Reducible, exactly as TauCeti.FiniteBilinearModule.prod is, so that the carrier of an orthogonal
product reduces to the product of the carriers and a subgroup of that product is a subgroup of the
orthogonal product without further coercion.
Equations
Instances For
Taking the polar bilinear module commutes with orthogonal products.
An orthogonal product is nondegenerate exactly when both factors are nondegenerate.
Quadratic isotropy #
An element of a finite quadratic module is isotropic when its quadratic value vanishes.
Equations
- A.IsIsotropicElem x = (A.quadratic x = 0)
Instances For
Quadratic isotropy of an element, unfolded to its defining property.
Zero is quadratically isotropic.
Negating an element preserves quadratic isotropy.
A morphism of finite quadratic modules preserves and reflects isotropic elements.
A quadratic isometry preserves and reflects isotropic elements.
Form negation preserves quadratic isotropy.
An element of an orthogonal product is quadratically isotropic exactly when the sum of its quadratic values vanishes.
A subgroup is quadratically isotropic when the quadratic map vanishes on it.
Equations
- A.IsIsotropic H = ∀ x ∈ H, A.quadratic x = 0
Instances For
Quadratic isotropy of a subgroup, unfolded to its defining property.
The image of a subgroup under a morphism of finite quadratic modules is quadratically isotropic exactly when the subgroup is.
A quadratic isometry transports quadratic isotropy of a subgroup, stated for the image under its additive equivalence.
An element of a quadratically isotropic subgroup is isotropic.
Quadratic isotropy passes to additive subgroups.
The trivial subgroup is quadratically isotropic.
Quadratic isotropy of a product subgroup is componentwise.
A subgroup is quadratically isotropic exactly when the restricted quadratic map is zero.
Quadratic isotropy implies bilinear isotropy for the polar pairing.
A quadratically isotropic subgroup is contained in its bilinear orthogonal complement.
A quadratic Lagrangian is a quadratically isotropic subgroup which is Lagrangian for the polar bilinear pairing.
Equations
- A.IsLagrangian H = (A.IsIsotropic H ∧ A.IsLagrangian H)
Instances For
The quadratic Lagrangian condition, unfolded to its two defining properties.
A quadratic isometry transports quadratic Lagrangian subgroups.
A quadratic Lagrangian is quadratically isotropic.
A quadratic Lagrangian is Lagrangian for the polar bilinear pairing.
A quadratic Lagrangian equals its orthogonal complement for the polar pairing.
A quadratically isotropic subgroup of a nondegenerate finite quadratic module is Lagrangian when its squared order is the order of the ambient module.
Quotients by isotropic subgroups #
A quadratic-isotropic subgroup contained in the radical of the polar pairing lies in the radical of the quadratic map. This is the exact condition needed to descend the quadratic map to the quotient.
A subgroup contained in the radical of the quadratic map is quadratic-isotropic.
A subgroup contained in the radical of the quadratic map is contained in the radical of the polar pairing.
The finite quadratic module obtained by quotienting by a subgroup contained in the radical of the quadratic map. That radical consists of the isotropic elements of the radical of the polar pairing, so this is exactly the condition making the quadratic map descend.
The underlying bilinear module is the corresponding quotient of the polar pairing, while the
quadratic map is Mathlib's QuadraticMap.lift.
Exposed for the same reason as FiniteBilinearModule.quotientOfLeRadical: so that its carrier
reduces to the Submodule quotient and maps out of it are definable.
Equations
- A.quotientOfLeQuadraticRadical K hK = { toFiniteBilinearModule := A.quotientOfLeRadical K ⋯, quadratic := A.quadratic.lift (AddSubgroup.toIntSubmodule K) hK, polar_eq_pairing' := ⋯ }
Instances For
The quotient map onto a quadratic quotient by a subgroup of the quadratic radical.
Equations
Instances For
The quotient map sends an element to its quotient class.
The quotient quadratic map is represented by the original quadratic map.
The quotient polar pairing is represented by the original pairing.
The quotient map onto a quadratic quotient is surjective.
Every element of a quadratic quotient is the class of a representative.
A representative has zero class in a quadratic quotient exactly when it belongs to the subgroup being divided out.
Two representatives have the same class in a quadratic quotient exactly when they differ by an element of the subgroup being divided out.
Taking the polar bilinear module commutes with quotienting by a subgroup of the quadratic radical.
The quadratic quotient is nondegenerate exactly when the subgroup contains the radical of the polar pairing.
The order of a quadratic quotient is the index of the subgroup being divided out.
The induced quadratic form on H^⊥ / H #
The elements of H lying in H^⊥, viewed as a subgroup of H^⊥. When H ≤ H^⊥, this
intersection is a copy of all of H.
Equations
Instances For
Membership in H ∩ H^⊥, viewed inside H^⊥, is membership of the underlying element in
H.
The copy of a quadratic-isotropic subgroup in its orthogonal complement remains quadratic-isotropic for the restricted form.
The copy of a quadratic-isotropic subgroup in its orthogonal complement lies in the radical of the quadratic map restricted to that complement.
The finite quadratic module induced on H^⊥ / H by a quadratic-isotropic subgroup H.
The form is first restricted to H^⊥; the copy of H there lies in the radical of the restricted
quadratic map, so the restricted form descends to the quotient.
Exposed for the same reason as quotientOfLeQuadraticRadical: so that its carrier reduces to the
Submodule quotient and maps out of it are definable.
Equations
- A.orthogonalQuotient H hH = (A.restrict (A.orthogonalComplement H)).quotientOfLeQuadraticRadical (A.subgroupInOrthogonalComplement H) ⋯
Instances For
The underlying bilinear module of a quadratic orthogonal quotient is the bilinear
orthogonal quotient. Both are the restriction of the form to H^⊥ divided by the copy of H
inside it, so the two constructions agree.
The additive equivalence from a quadratic orthogonal quotient to its underlying bilinear orthogonal quotient.
Equations
- A.orthogonalQuotientUnderlyingEquiv H hH = ⋯.mpr (AddEquiv.refl (A.orthogonalQuotient H).carrier)
Instances For
The quotient map from H^⊥ onto its induced quadratic quotient.
Equations
- A.orthogonalQuotientMk H hH = (A.restrict (A.orthogonalComplement H)).quotientOfLeQuadraticRadicalMk (A.subgroupInOrthogonalComplement H) ⋯
Instances For
The orthogonal-quotient map sends an element of H^⊥ to its quotient class.
The equivalence with the underlying bilinear orthogonal quotient commutes with the quotient maps.
The inverse equivalence from the underlying bilinear orthogonal quotient commutes with the quotient maps.
The quadratic form on H^⊥ / H is represented by the original quadratic form.
The pairing on H^⊥ / H is represented by the original polar pairing.
The quotient map from H^⊥ is surjective.
Every element of H^⊥ / H is the class of an element of H^⊥.
An element of H^⊥ has zero class in H^⊥ / H exactly when it lies in H.
Two elements of H^⊥ have the same class in H^⊥ / H exactly when they differ by an element
of H.
Equal quadratic-isotropic subgroups induce the same orthogonal quotient, up to the canonical isometry.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical isometry between the orthogonal quotients along equal subgroups is the identity on representatives.
Nondegeneracy of the orthogonal quotient. The quadratic module induced on H^⊥ / H is
nondegenerate exactly when H contains the radical of the polar bilinear module of A.
If A is nondegenerate, the quadratic module induced on H^⊥ / H is nondegenerate.
For nondegenerate A, the order of H^⊥ / H multiplied by |H|² is |A|.
Transport of an orthogonal quotient along an isometry #
A quadratic isometry carrying H onto K transports quadratic isotropy from H to K.
Transport of an orthogonal quotient along an isometry. An isometry f : A ≅ B of finite
quadratic modules carrying a quadratic-isotropic subgroup H of A onto K induces an isometry
H⊥ / H ≅ 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.symm y ∈ H⊥.