Restricting an integral lattice to a submodule

A submodule S of an integral lattice L need not span the rational ambient space. Its restricted integral form nevertheless defines a full integral lattice in ℚ ⊗[ℤ] S. IntegralLattice.restrict constructs this lattice, and restrictMap embeds its ambient space into that of L, preserving the forms. Its range is exactly the rational span of the embedded submodule, and its integral carrier maps onto that submodule. isEven_restrict_iff characterizes evenness by the original integral norm on the submodule.

When the embedded submodule is full, restrictFull instead keeps the original ambient space. restrictFullIsometry identifies these two constructions through the canonical rational extension of the inclusion. Neither construction assumes nondegeneracy: restrictions to isotropic submodules and to the zero submodule are allowed.

These constructions let orthogonal summands be treated as lattices without imposing an incorrect full-span hypothesis on each summand.

The rationalization uses IntegralLattice.ofIntegralForm and Mathlib's LinearMap.liftBaseChange.

Main declarations

• TauCeti.IntegralLattice.restrict: restriction in the submodule's own rational ambient space.
• TauCeti.IntegralLattice.restrictCarrierEquiv: the canonical integral carrier equivalence.
• TauCeti.IntegralLattice.isEven_restrict_iff: evenness characterized on the chosen submodule.
• TauCeti.IntegralLattice.restrictMap: the rational extension of the inclusion, characterized by restrictMap_injective, range_restrictMap, form_restrictMap, and map_restrictMap_restrict_carrier.
• TauCeti.IntegralLattice.restrictIsometry: restrictMap as an isometric embedding of rational forms; anisotropic_restrict passes anisotropy of the rational norm form to restrictions.
• TauCeti.IntegralLattice.restrictFull: restriction to a full ambient submodule contained in the original carrier, retaining the original rational ambient space; it inherits nondegeneracy and, by isEven_restrictFull, evenness.
• TauCeti.IntegralLattice.inf: the full restriction to the intersection of two carriers on the same rational space, with the form of the first lattice.
• TauCeti.IntegralLattice.restrictFullIsometry: the canonical comparison of the two restrictions when the embedded submodule is full.

References

• W. Ebeling, Lattices and Codes, Chapter 1.

noncomputable def TauCeti.IntegralLattice.restrict {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) : IntegralLattice (TensorProduct ℤ ℚ ↥S)

Restrict a lattice to an arbitrary submodule of its carrier, in that submodule's own rational ambient space. Every such submodule is finite free over ℤ.

@[simp]

theorem TauCeti.IntegralLattice.restrict_form {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) : (L.restrict S).form = LinearMap.BilinForm.baseChange ℚ (L.integralForm.restrict S)

The form of a restricted lattice is the rational extension of the restricted integral form.

theorem TauCeti.IntegralLattice.restrict_carrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) : (L.restrict S).carrier = ((TensorProduct.mk ℤ ℚ ↥S) 1).range

The carrier of a restricted lattice is the range of the unit pure tensor map.

@[simp]

theorem TauCeti.IntegralLattice.mem_restrict_carrier_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) (x : TensorProduct ℤ ℚ ↥S) : x ∈ (L.restrict S).carrier ↔ ∃ (s : ↥S), 1 ⊗ₜ[ℤ] s = x

The carrier of a restricted lattice consists of the unit pure tensors of the submodule.

noncomputable def TauCeti.IntegralLattice.restrictCarrierEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) : ↥S ≃ₗ[ℤ] ↥(L.restrict S).carrier

The original submodule is canonically equivalent to the carrier of the restricted lattice.

@[simp]

theorem TauCeti.IntegralLattice.coe_restrictCarrierEquiv_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) (s : ↥S) : ↑((L.restrictCarrierEquiv S) s) = 1 ⊗ₜ[ℤ] s

The carrier equivalence sends a submodule vector to its unit pure tensor.

@[simp]

theorem TauCeti.IntegralLattice.integralForm_restrictCarrierEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) (s t : ↥S) : ((L.restrict S).integralForm ((L.restrictCarrierEquiv S) s)) ((L.restrictCarrierEquiv S) t) = (L.integralForm ↑s) ↑t

Restriction recovers the original integral form on the chosen submodule.

@[simp]

theorem TauCeti.IntegralLattice.integralNorm_restrictCarrierEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) (s : ↥S) : (L.restrict S).integralNorm ((L.restrictCarrierEquiv S) s) = L.integralNorm ↑s

Restriction recovers the original integral norm on the chosen submodule.

theorem TauCeti.IntegralLattice.scaleIdeal_restrict_le {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) : (L.restrict S).scaleIdeal ≤ L.scaleIdeal

Restriction to any carrier submodule gives containment of scale ideals.

theorem TauCeti.IntegralLattice.normIdeal_restrict_le {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) : (L.restrict S).normIdeal ≤ L.normIdeal

Restriction to any carrier submodule gives containment of norm ideals.

theorem TauCeti.IntegralLattice.isEven_restrict_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) : (L.restrict S).IsEven ↔ ∀ (s : ↥S), Even (L.integralNorm ↑s)

A restricted lattice is even exactly when the original integral norm is even on the submodule. In particular restriction preserves evenness.

def TauCeti.IntegralLattice.restrictMap {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) : TensorProduct ℤ ℚ ↥S →ₗ[ℚ] V

The rational extension of the inclusion of a submodule into the ambient space of a lattice.

@[simp]

theorem TauCeti.IntegralLattice.restrictMap_tmul {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) (q : ℚ) (s : ↥S) : (L.restrictMap S) (q ⊗ₜ[ℤ] s) = q • ↑↑s

The rational inclusion sends a pure tensor to the scalar multiple of the embedded vector.

theorem TauCeti.IntegralLattice.restrictMap_injective {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) : Function.Injective ⇑(L.restrictMap S)

Rational extension of the inclusion remains injective. No nondegeneracy hypothesis on the form is needed.

theorem TauCeti.IntegralLattice.range_restrictMap {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) : (L.restrictMap S).range = Submodule.span ℚ ↑(Submodule.map L.carrier.subtype S)

The range of the rational inclusion is exactly the rational span of the embedded submodule.

@[simp]

theorem TauCeti.IntegralLattice.form_restrictMap {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) (x y : TensorProduct ℤ ℚ ↥S) : (L.form ((L.restrictMap S) x)) ((L.restrictMap S) y) = ((L.restrict S).form x) y

The rational inclusion preserves the forms, even if the restricted form is degenerate.

def TauCeti.IntegralLattice.restrictIsometry {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) : (L.restrict S).form →bᵢ L.form

The rational extension of the inclusion, as an isometric embedding of rational forms.

@[simp]

theorem TauCeti.IntegralLattice.restrictIsometry_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) (z : TensorProduct ℤ ℚ ↥S) : (L.restrictIsometry S) z = (L.restrictMap S) z

theorem TauCeti.IntegralLattice.anisotropic_restrict {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (h : QuadraticMap.Anisotropic L.norm) (S : Submodule ℤ ↥L.carrier) : QuadraticMap.Anisotropic (L.restrict S).norm

The restriction of a lattice with anisotropic rational norm form is anisotropic.

theorem TauCeti.IntegralLattice.map_restrictMap_restrict_carrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) : Submodule.map (↑ℤ (L.restrictMap S)) (L.restrict S).carrier = Submodule.map L.carrier.subtype S

The restricted integral carrier maps onto the embedded submodule, not merely onto its rational span.

def TauCeti.IntegralLattice.restrictFull {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (N : Submodule ℤ V) (hN : N ≤ L.carrier) [Submodule.IsLattice ℚ N] : IntegralLattice V

Restriction to a full ambient submodule contained in the carrier, retaining the original rational ambient space. Fullness is supplied as an IsLattice ℚ instance. The constructor restrict needs no span condition because it builds its own rational ambient space.

@[simp]

theorem TauCeti.IntegralLattice.restrictFull_carrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (N : Submodule ℤ V) (hN : N ≤ L.carrier) [Submodule.IsLattice ℚ N] : (L.restrictFull N hN).carrier = N

The carrier of the full restriction is the chosen ambient submodule.

@[simp]

theorem TauCeti.IntegralLattice.restrictFull_form {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (N : Submodule ℤ V) (hN : N ≤ L.carrier) [Submodule.IsLattice ℚ N] : (L.restrictFull N hN).form = L.form

Full restriction retains the original rational form.

instance TauCeti.IntegralLattice.instIsNondegenerateRestrictFull {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (N : Submodule ℤ V) (hN : N ≤ L.carrier) [Submodule.IsLattice ℚ N] : (L.restrictFull N hN).IsNondegenerate

Full restriction of a nondegenerate lattice is nondegenerate, since the form is unchanged.

theorem TauCeti.IntegralLattice.isEven_restrictFull {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsEven) (N : Submodule ℤ V) (hN : N ≤ L.carrier) [Submodule.IsLattice ℚ N] : (L.restrictFull N hN).IsEven

Full restriction of an even lattice is even.

instance TauCeti.IntegralLattice.isLattice_carrier_inf {V : Type u} [AddCommGroup V] [Module ℚ V] (L M : IntegralLattice V) : Submodule.IsLattice ℚ (L.carrier ⊓ M.carrier)

The intersection of the carriers of two integral lattices on the same rational space is a full lattice.

noncomputable def TauCeti.IntegralLattice.inf {V : Type u} [AddCommGroup V] [Module ℚ V] (L M : IntegralLattice V) : IntegralLattice V

The integral lattice on the intersection of the carriers of L and M, with the form of L.

@[simp]

theorem TauCeti.IntegralLattice.inf_carrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L M : IntegralLattice V) : (L.inf M).carrier = L.carrier ⊓ M.carrier

The carrier of L.inf M is the intersection of the two carriers.

@[simp]

theorem TauCeti.IntegralLattice.inf_form {V : Type u} [AddCommGroup V] [Module ℚ V] (L M : IntegralLattice V) : (L.inf M).form = L.form

The lattice L.inf M carries the form of L.

noncomputable def TauCeti.IntegralLattice.restrictFullIsometry {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) [Submodule.IsLattice ℚ (Submodule.map L.carrier.subtype S)] : (L.restrict S).Isometry (L.restrictFull (Submodule.map L.carrier.subtype S) ⋯)

For a full submodule, restriction in its own rationalization is canonically isometric to restriction in the original ambient space. The underlying map is the rational extension of the inclusion, so this identifies both the carriers and the forms.

@[simp]

theorem TauCeti.IntegralLattice.restrictFullIsometry_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) [Submodule.IsLattice ℚ (Submodule.map L.carrier.subtype S)] (x : TensorProduct ℤ ℚ ↥S) : (L.restrictFullIsometry S) x = (L.restrictMap S) x

The canonical comparison applies the rational extension of the inclusion.