Metabolic discriminant forms and unimodular overlattices

For an even nondegenerate integral lattice, an intermediate carrier is even precisely when its discriminant subgroup is quadratic-isotropic. It is unimodular precisely when that subgroup equals its orthogonal complement. Together these identify metabolic discriminant forms with lattices admitting an even unimodular overlattice.

See Nikulin, Integral symmetric bilinear forms and some of their applications, §1.4.

theorem TauCeti.IntegralLattice.isMetabolic_discriminantQuadraticModule_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) : (L.discriminantQuadraticModule hL).IsMetabolic ↔ ∃ (M : { M : ↑L.IntermediateCarrier // IntermediateCarrier.IsEven M }), ⋯.toIntegralLattice.IsUnimodular

The discriminant form of an even lattice is metabolic exactly when the lattice has an even unimodular intermediate overlattice.