Documentation

TauCeti.LinearAlgebra.FiniteBilinearModule.Metabolic

Metabolic finite quadratic modules #

A finite quadratic module is metabolic when it has a quadratic Lagrangian: a subgroup on which the quadratic form vanishes and which equals its orthogonal complement for the polar pairing. This is the condition that arises when an even lattice is glued to an even unimodular overlattice. Bilinear isotropy alone does not suffice.

The terminology follows Nikulin, Integral symmetric bilinear forms and some of their applications, §1.4.

source
def TauCeti.FiniteQuadraticModule.IsMetabolic (A : FiniteQuadraticModule) :
Prop

A finite quadratic module is metabolic if it admits a quadratic Lagrangian.

Instances For
    source
    @[simp]
    theorem TauCeti.FiniteQuadraticModule.isMetabolic_def (A : FiniteQuadraticModule) :
    A.IsMetabolic ↔ ∃ (H : AddSubgroup A.carrier), A.IsLagrangian H

    Metabolicity means that a quadratic Lagrangian exists.

    source
    theorem TauCeti.FiniteQuadraticModule.IsMetabolic.isSquare_natCard {A : FiniteQuadraticModule} (h : A.IsMetabolic) (hA : A.IsNondegenerate) :
    IsSquare (Nat.card A.carrier)

    A nondegenerate metabolic finite quadratic module has square order: a quadratic Lagrangian has order whose square is the order of the ambient group.

    source
    theorem TauCeti.FiniteQuadraticModule.Isometry.isMetabolic_iff {A : FiniteQuadraticModule} {B : FiniteQuadraticModule} (f : A.Isometry B) :
    A.IsMetabolic ↔ B.IsMetabolic

    An isometry preserves the existence of a quadratic Lagrangian. The isometry must be supplied explicitly: it occurs in neither side of the equivalence.