Integral and even overlattices via isotropic subgroups

Let L be an integral lattice. This file refines the intermediate-carrier correspondence of TauCeti.LinearAlgebra.IntegralLattice.Overlattice.Basic by the two properties an intermediate carrier L ≤ M ≤ Lᵛ can enjoy: M is integral when it lies in its own dual submodule, so the rational form pairs its vectors integrally, and M is even when the norm of each of its vectors is twice an integer. Evenness implies integrality by polarization, mirroring the classical fact that even lattices are integral.

The characteristic results locate both classes inside the discriminant group, in two stages. For any integral lattice, M is integral exactly when the discriminant pairing vanishes on the subgroup M / L of A_L = Lᵛ / L, and, when L is even, M is even exactly when the discriminant quadratic map vanishes on M / L. When L is moreover nondegenerate — so that the discriminant group packages as a finite bilinear or quadratic module — these become isotropy of M / L, and restricting the intermediate-carrier order isomorphism accordingly packages the two gluing correspondences: integral carriers correspond to bilinear-isotropic subgroups, and even carriers of an even lattice correspond to quadratic-isotropic subgroups.

Main declarations

• TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral: integrality of an intermediate carrier.
• TauCeti.IntegralLattice.IntermediateCarrier.IsEven: evenness of an intermediate carrier.
• TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral.toIntegralLattice: an integral intermediate carrier, as an integral lattice for the same ambient form. It inherits nondegeneracy and positive definiteness from the lattice it lies over; evenness is not inherited, and is instead supplied by IsEven of the carrier itself.
• TauCeti.IntegralLattice.IntermediateCarrier.isIntegral_iff_forall_discriminantPairing_eq_zero: integral carriers are cut out by vanishing of the discriminant pairing.
• TauCeti.IntegralLattice.IntermediateCarrier.isEven_iff_forall_discriminantQuadraticMap_eq_zero: even carriers of an even lattice are cut out by vanishing of the discriminant quadratic map.
• TauCeti.IntegralLattice.IntermediateCarrier.isIntegral_iff_isIsotropic_discriminantSubgroup, TauCeti.IntegralLattice.IntermediateCarrier.isEven_iff_isIsotropic_discriminantSubgroup: the isotropy forms of the two criteria, for a nondegenerate lattice.
• TauCeti.IntegralLattice.integralIntermediateCarrierOrderIsoIsotropicSubgroup: the restriction of the intermediate-carrier order isomorphism to integral carriers.
• TauCeti.IntegralLattice.evenIntermediateCarrierOrderIsoIsotropicSubgroup: the restriction of the intermediate-carrier order isomorphism to even carriers of an even lattice.
• TauCeti.IntegralLattice.ofIsotropicSubgroup: the even overlattice glued along a quadratic-isotropic subgroup of the discriminant group, as an integral lattice. It keeps the ambient form, so it inherits nondegeneracy and positive definiteness, and the isotropy hypothesis makes it even.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.4, Proposition 1.4.1. The quadratic statement here is that proposition in the half-norm ℚ/ℤ convention; the bilinear statement is its elementary intermediate-lattice analogue.
• W. Ebeling, Lattices and Codes, Chapter 1.
• TauCetiRoadmap/IntegralLattices/README.md, Layer 4.
• TauCetiRoadmap/IntegralLattices/Suggested.lean (integralOverlatticeEquivIsotropicSubgroup, evenOverlatticeEquivIsotropicSubgroup).

def TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (M : ↑L.IntermediateCarrier) : Prop

An intermediate carrier is integral when it lies in its own dual submodule, the shape of IntegralLattice.le_dual.

Equations

• TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral M = (↑M ≤ L.form.dualSubmodule ↑M)

theorem TauCeti.IntegralLattice.IntermediateCarrier.isIntegral_def {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {M : ↑L.IntermediateCarrier} : IsIntegral M ↔ ∀ x ∈ ↑M, ∀ y ∈ ↑M, (L.form x) y ∈ 1

Integrality of an intermediate carrier, unfolded to elementwise integrality of the form.

def TauCeti.IntegralLattice.IntermediateCarrier.IsEven {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (M : ↑L.IntermediateCarrier) : Prop

An intermediate carrier is even when every norm of its vectors is twice an integer, the normal form of IntegralLattice.isEven_iff_forall_norm.

Equations

• TauCeti.IntegralLattice.IntermediateCarrier.IsEven M = ∀ x ∈ ↑M, ∃ (n : ℤ), L.norm x = 2 * ↑n

theorem TauCeti.IntegralLattice.IntermediateCarrier.isEven_def {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {M : ↑L.IntermediateCarrier} : IsEven M ↔ ∀ x ∈ ↑M, ∃ (n : ℤ), L.norm x = 2 * ↑n

Evenness of an intermediate carrier, unfolded to its defining property.

@[simp]

theorem TauCeti.IntegralLattice.IntermediateCarrier.isIntegral_bot {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} : IsIntegral ⊥

The bottom intermediate carrier, the lattice itself, is integral.

@[simp]

theorem TauCeti.IntegralLattice.IntermediateCarrier.isEven_bot_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} : IsEven ⊥ ↔ L.IsEven

The bottom intermediate carrier is even exactly when the lattice itself is even.

theorem TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral.mono {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {M N : ↑L.IntermediateCarrier} (hN : IsIntegral N) (h : M ≤ N) : IsIntegral M

Integrality descends along containment of intermediate carriers.

theorem TauCeti.IntegralLattice.IntermediateCarrier.IsEven.mono {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {M N : ↑L.IntermediateCarrier} (hN : IsEven N) (h : M ≤ N) : IsEven M

Evenness descends along containment of intermediate carriers.

theorem TauCeti.IntegralLattice.IntermediateCarrier.IsEven.isIntegral {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {M : ↑L.IntermediateCarrier} (hM : IsEven M) : IsIntegral M

Evenness of an intermediate carrier implies its integrality, by polarization.

def TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral.toIntegralLattice {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {M : ↑L.IntermediateCarrier} [Submodule.IsLattice ℚ ↑M] (hM : IsIntegral M) : IntegralLattice V

An integral intermediate carrier which is itself a full ℤ-lattice is an integral lattice, for the same ambient rational form. Over a nondegenerate lattice every intermediate carrier is such a lattice, by TauCeti.IntegralLattice.instIsLatticeIntermediateCarrier.

Equations

• hM.toIntegralLattice = TauCeti.IntegralLattice.ofSubmodule (↑M) L.form ⋯ ⋯

@[simp]

theorem TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral.toIntegralLattice_carrier {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {M : ↑L.IntermediateCarrier} [Submodule.IsLattice ℚ ↑M] (hM : IsIntegral M) : hM.toIntegralLattice.carrier = ↑M

The carrier of the integral lattice attached to an integral intermediate carrier.

@[simp]

theorem TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral.toIntegralLattice_form {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {M : ↑L.IntermediateCarrier} [Submodule.IsLattice ℚ ↑M] (hM : IsIntegral M) : hM.toIntegralLattice.form = L.form

The integral lattice attached to an integral intermediate carrier keeps the ambient form.

@[simp]

theorem TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral.toIntegralLattice_bot {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hM : IsIntegral ⊥) : hM.toIntegralLattice = L

Regarding the lattice itself as an intermediate carrier returns the lattice.

theorem TauCeti.IntegralLattice.IntermediateCarrier.IsEven.isEven_toIntegralLattice {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {M : ↑L.IntermediateCarrier} [Submodule.IsLattice ℚ ↑M] (hM : IsEven M) : ⋯.toIntegralLattice.IsEven

An even intermediate carrier is an even integral lattice.

theorem TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral.isPosDef_toIntegralLattice_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {M : ↑L.IntermediateCarrier} [Submodule.IsLattice ℚ ↑M] (hM : IsIntegral M) : hM.toIntegralLattice.IsPosDef ↔ L.IsPosDef

An integral overlattice is positive definite exactly when the lattice it lies over is: the two carry the same ambient form.

instance TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral.instIsNondegenerate {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {M : ↑L.IntermediateCarrier} (hM : IsIntegral M) : hM.toIntegralLattice.IsNondegenerate

An overlattice of a nondegenerate integral lattice is nondegenerate: it carries the same ambient form.

theorem TauCeti.IntegralLattice.IntermediateCarrier.isIntegral_iff_forall_discriminantPairing_eq_zero {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (M : ↑L.IntermediateCarrier) : IsIntegral M ↔ ∀ x ∈ L.discriminantSubgroup M, ∀ y ∈ L.discriminantSubgroup M, (L.discriminantPairing x) y = 0

Integrality is vanishing of the discriminant pairing. An intermediate carrier is integral exactly when the discriminant pairing vanishes on its subgroup of the discriminant group. No nondegeneracy is required.

theorem TauCeti.IntegralLattice.IntermediateCarrier.isEven_iff_forall_discriminantQuadraticMap_eq_zero {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsEven) (M : ↑L.IntermediateCarrier) : IsEven M ↔ ∀ x ∈ L.discriminantSubgroup M, (L.discriminantQuadraticMap hL) x = 0

Evenness is vanishing of the discriminant quadratic map. For an even lattice, an intermediate carrier is even exactly when the discriminant quadratic map vanishes on its subgroup of the discriminant group. No nondegeneracy is required.

theorem TauCeti.IntegralLattice.IntermediateCarrier.isIntegral_iff_isIsotropic_discriminantSubgroup {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] (M : ↑L.IntermediateCarrier) : IsIntegral M ↔ L.discriminantBilinearModule.IsIsotropic (L.discriminantSubgroup M)

Integrality is bilinear isotropy. For a nondegenerate lattice, an intermediate carrier is integral exactly when its subgroup of the discriminant group is isotropic in the discriminant bilinear module.

theorem TauCeti.IntegralLattice.IntermediateCarrier.isEven_iff_isIsotropic_discriminantSubgroup {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] (hL : L.IsEven) (M : ↑L.IntermediateCarrier) : IsEven M ↔ (L.discriminantQuadraticModule hL).IsIsotropic (L.discriminantSubgroup M)

Evenness is quadratic isotropy. For an even nondegenerate lattice, an intermediate carrier is even exactly when its subgroup of the discriminant group is isotropic in the discriminant quadratic module.

@[simp]

theorem TauCeti.IntegralLattice.isIntegral_intermediateCarrierOfDiscriminantSubgroup_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (H : AddSubgroup L.DiscriminantGroup) : IntermediateCarrier.IsIntegral (L.intermediateCarrierOfDiscriminantSubgroup H) ↔ L.discriminantBilinearModule.IsIsotropic H

The inverse-image carrier of a subgroup is integral exactly when the subgroup is bilinear-isotropic.

theorem TauCeti.IntegralLattice.isEven_intermediateCarrierOfDiscriminantSubgroup_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) (H : AddSubgroup L.DiscriminantGroup) : IntermediateCarrier.IsEven (L.intermediateCarrierOfDiscriminantSubgroup H) ↔ (L.discriminantQuadraticModule hL).IsIsotropic H

For an even lattice, the inverse-image carrier of a subgroup is even exactly when the subgroup is quadratic-isotropic.

def TauCeti.IntegralLattice.integralIntermediateCarrierOrderIsoIsotropicSubgroup {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] : { M : ↑L.IntermediateCarrier // IntermediateCarrier.IsIntegral M } ≃o { H : AddSubgroup L.DiscriminantGroup // L.discriminantBilinearModule.IsIsotropic H }

Integral overlattices correspond to bilinear-isotropic subgroups. The intermediate-carrier order isomorphism restricts to the integral carriers on one side and the bilinear-isotropic subgroups of the discriminant group on the other.

Equations

• L.integralIntermediateCarrierOrderIsoIsotropicSubgroup = TauCeti.IntegralLattice.restrictOrderIso✝ L ⋯

@[simp]

theorem TauCeti.IntegralLattice.integralIntermediateCarrierOrderIsoIsotropicSubgroup_apply_coe {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (M : { M : ↑L.IntermediateCarrier // IntermediateCarrier.IsIntegral M }) : ↑(L.integralIntermediateCarrierOrderIsoIsotropicSubgroup M) = L.discriminantSubgroup ↑M

The restricted integral-carrier order isomorphism acts by the discriminant-subgroup construction.

@[simp]

theorem TauCeti.IntegralLattice.integralIntermediateCarrierOrderIsoIsotropicSubgroup_symm_apply_coe {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (H : { H : AddSubgroup L.DiscriminantGroup // L.discriminantBilinearModule.IsIsotropic H }) : ↑(L.integralIntermediateCarrierOrderIsoIsotropicSubgroup.symm H) = L.intermediateCarrierOfDiscriminantSubgroup ↑H

The inverse of the restricted integral-carrier order isomorphism acts by the inverse-image construction.

def TauCeti.IntegralLattice.evenIntermediateCarrierOrderIsoIsotropicSubgroup {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) : { M : ↑L.IntermediateCarrier // IntermediateCarrier.IsEven M } ≃o { H : AddSubgroup L.DiscriminantGroup // (L.discriminantQuadraticModule hL).IsIsotropic H }

Even overlattices correspond to quadratic-isotropic subgroups. For an even lattice, the intermediate-carrier order isomorphism restricts to the even carriers on one side and the quadratic-isotropic subgroups of the discriminant group on the other.

Equations

• L.evenIntermediateCarrierOrderIsoIsotropicSubgroup hL = TauCeti.IntegralLattice.restrictOrderIso✝ L ⋯

@[simp]

theorem TauCeti.IntegralLattice.evenIntermediateCarrierOrderIsoIsotropicSubgroup_apply_coe {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) (M : { M : ↑L.IntermediateCarrier // IntermediateCarrier.IsEven M }) : ↑((L.evenIntermediateCarrierOrderIsoIsotropicSubgroup hL) M) = L.discriminantSubgroup ↑M

The restricted even-carrier order isomorphism acts by the discriminant-subgroup construction.

@[simp]

theorem TauCeti.IntegralLattice.evenIntermediateCarrierOrderIsoIsotropicSubgroup_symm_apply_coe {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) (H : { H : AddSubgroup L.DiscriminantGroup // (L.discriminantQuadraticModule hL).IsIsotropic H }) : ↑((L.evenIntermediateCarrierOrderIsoIsotropicSubgroup hL).symm H) = L.intermediateCarrierOfDiscriminantSubgroup ↑H

The inverse of the restricted even-carrier order isomorphism acts by the inverse-image construction.

noncomputable def TauCeti.IntegralLattice.ofIsotropicSubgroup {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) (H : AddSubgroup L.DiscriminantGroup) (hH : (L.discriminantQuadraticModule hL).IsIsotropic H) : IntegralLattice V

The even overlattice glued along a quadratic-isotropic subgroup of the discriminant group. This names the composite the gluing correspondence produces: the inverse-image carrier of H, which is even because H is quadratic-isotropic, regarded as an integral lattice for the same ambient form. It is the gluing operation in the form its consumers use, where the datum in hand is the subgroup rather than the carrier.

Equations

• L.ofIsotropicSubgroup hL H hH = ⋯.toIntegralLattice

@[simp]

theorem TauCeti.IntegralLattice.ofIsotropicSubgroup_carrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) (H : AddSubgroup L.DiscriminantGroup) (hH : (L.discriminantQuadraticModule hL).IsIsotropic H) : (L.ofIsotropicSubgroup hL H hH).carrier = ↑(L.intermediateCarrierOfDiscriminantSubgroup H)

The glued lattice is carried by the inverse image of H in the dual.

@[simp]

theorem TauCeti.IntegralLattice.ofIsotropicSubgroup_form {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) (H : AddSubgroup L.DiscriminantGroup) (hH : (L.discriminantQuadraticModule hL).IsIsotropic H) : (L.ofIsotropicSubgroup hL H hH).form = L.form

Gluing keeps the ambient rational form.

theorem TauCeti.IntegralLattice.isEven_ofIsotropicSubgroup {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) (H : AddSubgroup L.DiscriminantGroup) (hH : (L.discriminantQuadraticModule hL).IsIsotropic H) : (L.ofIsotropicSubgroup hL H hH).IsEven

The glued lattice is even, which is what the quadratic-isotropy hypothesis buys.

instance TauCeti.IntegralLattice.instIsNondegenerateOfIsotropicSubgroup {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) (H : AddSubgroup L.DiscriminantGroup) (hH : (L.discriminantQuadraticModule hL).IsIsotropic H) : (L.ofIsotropicSubgroup hL H hH).IsNondegenerate

A lattice glued over a nondegenerate lattice is nondegenerate: it carries the same ambient form. Stated for ofIsotropicSubgroup itself, since instance search does not unfold it.

theorem TauCeti.IntegralLattice.isPosDef_ofIsotropicSubgroup_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) (H : AddSubgroup L.DiscriminantGroup) (hH : (L.discriminantQuadraticModule hL).IsIsotropic H) : (L.ofIsotropicSubgroup hL H hH).IsPosDef ↔ L.IsPosDef

A glued lattice is positive definite exactly when the lattice it lies over is.

@[simp]

theorem TauCeti.IntegralLattice.ofIsotropicSubgroup_bot {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) : L.ofIsotropicSubgroup hL ⊥ ⋯ = L

Gluing along the trivial subgroup returns the lattice. The isotropy hypothesis is supplied here rather than asked of the caller, since the trivial subgroup is unconditionally isotropic.

theorem TauCeti.IntegralLattice.ofIsotropicSubgroup_eq_toIntegralLattice {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) (H : { H : AddSubgroup L.DiscriminantGroup // (L.discriminantQuadraticModule hL).IsIsotropic H }) : L.ofIsotropicSubgroup hL ↑H ⋯ = ⋯.toIntegralLattice

Gluing agrees with the even gluing correspondence: ofIsotropicSubgroup is the lattice carried by the correspondence's inverse image.