Intermediate carriers of integral lattices

Let L be an integral lattice. An intermediate carrier is a ℤ-submodule M of the ambient rational vector space satisfying

L ≤ M ≤ Lᵛ.

This file proves the underlying correspondence in the theory of overlattices: intermediate carriers are order-isomorphic to additive subgroups of the discriminant group A_L = Lᵛ / L. The forward map sends M to its image M / L in A_L, and the inverse sends a subgroup H ≤ A_L to its literal inverse image in Lᵛ, written L_H below. The characteristic membership lemmas state both constructions on representatives. The interval of intermediate carriers is a bounded order, with ⊥ the carrier of L and ⊤ its dual carrier. Every intermediate carrier is also proved to be a full ℤ-lattice in the common rational ambient space when L is nondegenerate. The correspondence and its membership, inverse, and order lemmas do not require nondegeneracy; only this fullness result does, and even it is unconditional for ⊥, which is the carrier of L itself.

Integrality and evenness of an intermediate carrier are deliberately not assumed here; the restrictions of the correspondence they cut out live in TauCeti.LinearAlgebra.IntegralLattice.Overlattice.Isotropic.

Main declarations

• TauCeti.IntegralLattice.IntermediateCarrier: the interval of carriers between L and Lᵛ.
• TauCeti.IntegralLattice.intermediateCarrierOrderIsoDiscriminantSubgroup: the order isomorphism with subgroups of A_L.
• TauCeti.IntegralLattice.discriminantSubgroup: the image M / L of an intermediate carrier in A_L.
• TauCeti.IntegralLattice.intermediateCarrierOfDiscriminantSubgroup: the inverse-image carrier L_H attached to a subgroup H of A_L.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.4.
• W. Ebeling, Lattices and Codes, Chapter 1.
• TauCetiRoadmap/IntegralLattices/README.md, Layer 4.
• TauCetiRoadmap/IntegralLattices/Suggested.lean (intermediateOrderIsoSubgroup).

@[reducible, inline]

abbrev TauCeti.IntegralLattice.IntermediateCarrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Set (Submodule ℤ V)

The type of ℤ-submodules lying between an integral lattice and its dual carrier.

Equations

• L.IntermediateCarrier = Set.Icc L.carrier L.dualCarrier

instance TauCeti.IntegralLattice.instFactCarrierLeDualCarrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Fact (L.carrier ≤ L.dualCarrier)

The endpoints of the intermediate-carrier interval are ordered, so L.IntermediateCarrier is a bounded order with ⊥ the carrier of L and ⊤ its dual carrier.

def TauCeti.IntegralLattice.intermediateCarrierOrderIsoDiscriminantSubgroup {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : ↑L.IntermediateCarrier ≃o AddSubgroup L.DiscriminantGroup

The intermediate-carrier correspondence. Intermediate carriers L ≤ M ≤ Lᵛ are order-isomorphic to additive subgroups of the discriminant group A_L = Lᵛ / L.

The construction is the composite of Mathlib's correspondence theorem for quotient modules and its order isomorphism between submodules of a subtype and ambient submodules below that subtype: Submodule.comapMkQRelIso, Submodule.mapIic, and AddSubgroup.toIntSubmodule.

Equations

• L.intermediateCarrierOrderIsoDiscriminantSubgroup = (TauCeti.iccOrderIsoQuotientOfMapEq L.carrierInDual ⋯).trans AddSubgroup.toIntSubmodule.symm

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

The subgroup M / L of the discriminant group attached to an intermediate carrier L ≤ M ≤ Lᵛ.

Equations

• L.discriminantSubgroup M = L.intermediateCarrierOrderIsoDiscriminantSubgroup M

@[simp]

theorem TauCeti.IntegralLattice.intermediateCarrierOrderIsoDiscriminantSubgroup_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (M : ↑L.IntermediateCarrier) : L.intermediateCarrierOrderIsoDiscriminantSubgroup M = L.discriminantSubgroup M

Evaluating the intermediate-carrier order isomorphism is the named discriminant-subgroup construction.

@[simp]

theorem TauCeti.IntegralLattice.mk_mem_discriminantSubgroup_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (M : ↑L.IntermediateCarrier) (x : ↥L.dualCarrier) : Submodule.Quotient.mk x ∈ L.discriminantSubgroup M ↔ ↑x ∈ ↑M

A dual-carrier representative belongs to M / L exactly when its underlying ambient vector belongs to M.

def TauCeti.IntegralLattice.intermediateCarrierOfDiscriminantSubgroup {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (H : AddSubgroup L.DiscriminantGroup) : ↑L.IntermediateCarrier

The intermediate carrier L_H obtained as the inverse image in Lᵛ of a subgroup of the discriminant group.

Equations

• L.intermediateCarrierOfDiscriminantSubgroup H = L.intermediateCarrierOrderIsoDiscriminantSubgroup.symm H

@[simp]

theorem TauCeti.IntegralLattice.intermediateCarrierOrderIsoDiscriminantSubgroup_symm_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (H : AddSubgroup L.DiscriminantGroup) : L.intermediateCarrierOrderIsoDiscriminantSubgroup.symm H = L.intermediateCarrierOfDiscriminantSubgroup H

Evaluating the inverse intermediate-carrier order isomorphism is the named inverse-image construction.

@[simp]

theorem TauCeti.IntegralLattice.coe_mem_intermediateCarrierOfDiscriminantSubgroup_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (H : AddSubgroup L.DiscriminantGroup) (x : ↥L.dualCarrier) : ↑x ∈ ↑(L.intermediateCarrierOfDiscriminantSubgroup H) ↔ Submodule.Quotient.mk x ∈ H

A dual-carrier representative belongs to L_H exactly when its class belongs to H.

theorem TauCeti.IntegralLattice.mem_intermediateCarrierOfDiscriminantSubgroup_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (H : AddSubgroup L.DiscriminantGroup) (x : V) : x ∈ ↑(L.intermediateCarrierOfDiscriminantSubgroup H) ↔ ∃ (hx : x ∈ L.dualCarrier), Submodule.Quotient.mk ⟨x, hx⟩ ∈ H

The carrier attached to H ≤ A_L is its literal inverse image in the dual carrier: an ambient vector lies in L_H exactly when it lies in Lᵛ and its class belongs to H.

@[simp]

theorem TauCeti.IntegralLattice.intermediateCarrierOfDiscriminantSubgroup_bot {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.intermediateCarrierOfDiscriminantSubgroup ⊥ = ⊥

The inverse image of the bottom discriminant subgroup is the bottom intermediate carrier.

@[simp]

theorem TauCeti.IntegralLattice.intermediateCarrierOfDiscriminantSubgroup_top {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.intermediateCarrierOfDiscriminantSubgroup ⊤ = ⊤

The inverse image of the top discriminant subgroup is the top intermediate carrier.

theorem TauCeti.IntegralLattice.coe_intermediateCarrierOfDiscriminantSubgroup_bot {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : ↑(L.intermediateCarrierOfDiscriminantSubgroup ⊥) = L.carrier

The inverse image of the bottom discriminant subgroup is the original carrier.

theorem TauCeti.IntegralLattice.coe_intermediateCarrierOfDiscriminantSubgroup_top {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : ↑(L.intermediateCarrierOfDiscriminantSubgroup ⊤) = L.dualCarrier

The inverse image of the top discriminant subgroup is the dual carrier.

@[simp]

theorem TauCeti.IntegralLattice.discriminantSubgroup_intermediateCarrierOfDiscriminantSubgroup {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (H : AddSubgroup L.DiscriminantGroup) : L.discriminantSubgroup (L.intermediateCarrierOfDiscriminantSubgroup H) = H

Passing from a subgroup of A_L to its inverse-image carrier and back recovers the subgroup.

@[simp]

theorem TauCeti.IntegralLattice.intermediateCarrierOfDiscriminantSubgroup_discriminantSubgroup {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (M : ↑L.IntermediateCarrier) : L.intermediateCarrierOfDiscriminantSubgroup (L.discriminantSubgroup M) = M

Passing from an intermediate carrier to its discriminant subgroup and back recovers the carrier.

@[simp]

theorem TauCeti.IntegralLattice.discriminantSubgroup_bot {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.discriminantSubgroup ⊥ = ⊥

The discriminant subgroup of the bottom intermediate carrier, the carrier of L itself, is bottom.

@[simp]

theorem TauCeti.IntegralLattice.discriminantSubgroup_top {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.discriminantSubgroup ⊤ = ⊤

The discriminant subgroup of the top intermediate carrier, the dual carrier, is top.

@[simp]

theorem TauCeti.IntegralLattice.discriminantSubgroup_le_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (M N : ↑L.IntermediateCarrier) : L.discriminantSubgroup M ≤ L.discriminantSubgroup N ↔ M ≤ N

Containment of intermediate carriers is detected by containment of their discriminant subgroups.

@[simp]

theorem TauCeti.IntegralLattice.intermediateCarrierOfDiscriminantSubgroup_le_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (H K : AddSubgroup L.DiscriminantGroup) : L.intermediateCarrierOfDiscriminantSubgroup H ≤ L.intermediateCarrierOfDiscriminantSubgroup K ↔ H ≤ K

Containment of subgroups of the discriminant group is detected by containment of their inverse-image carriers.

instance TauCeti.IntegralLattice.instIsLatticeBotIntermediateCarrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Submodule.IsLattice ℚ ↑⊥

The bottom intermediate carrier is the carrier of L itself, hence a full ℤ-lattice in the ambient rational space. No nondegeneracy is required.

instance TauCeti.IntegralLattice.instIsLatticeIntermediateCarrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (M : ↑L.IntermediateCarrier) : Submodule.IsLattice ℚ ↑M

Every intermediate carrier of a nondegenerate integral lattice is a full ℤ-lattice in the same rational ambient space.