Basic examples of integral lattices

This file supplies the three acceptance examples from Layer 1 of the integral-lattices roadmap. The hyperbolic plane is even, unimodular, and indefinite of signature (1, 0, 1); the negative rank-one root lattice has signature (0, 0, 1); and the affine A₁ lattice is even, positive-semidefinite, and degenerate of signature (1, 1, 0). The last example is not merely identified by its signature: its radical quotient is exhibited isometrically as the positive rank-one A₁ lattice.

All four lattices are constructed with TauCeti.IntegralLattice.ofGramMatrix, so their carriers are genuine full ℤ-lattices in their displayed rational ambient spaces. The quotient identification uses the coordinate difference (x₀ - x₁), whose kernel is exactly the radical of the affine form.

Main definitions

• TauCeti.IntegralLattice.a1: the positive rank-one lattice with Gram matrix [2].
• TauCeti.IntegralLattice.negativeA1: the negative rank-one lattice with Gram matrix [-2].
• TauCeti.IntegralLattice.hyperbolicPlane: the hyperbolic plane with Gram matrix !![0, 1; 1, 0].
• TauCeti.IntegralLattice.affineA1: the affine A₁ lattice with Gram matrix !![2, -2; -2, 2].
• TauCeti.IntegralLattice.affineA1RadicalQuotientIsometry: the isometry from the radical quotient of affineA1 to a1.
• TauCeti.IntegralLattice.infinite_vectorsOfNorm_zero_hyperbolicPlane: the hyperbolic plane has infinitely many vectors of norm zero, so shells of an indefinite lattice need not be finite.

References

• W. Ebeling, Lattices and Codes, Chapter 1.
• TauCetiRoadmap/IntegralLattices/README.md, Layer 1 acceptance criteria.

The four Gram lattices

noncomputable def TauCeti.IntegralLattice.a1 : IntegralLattice ℚ

The positive rank-one root lattice A₁, with Gram matrix [2].

Equations

• TauCeti.IntegralLattice.a1 = TauCeti.IntegralLattice.ofGramMatrix (Module.Basis.singleton (Fin 1) ℚ) TauCeti.IntegralLattice.a1Matrix✝ TauCeti.IntegralLattice.a1._proof_1✝

noncomputable def TauCeti.IntegralLattice.negativeA1 : IntegralLattice ℚ

The negative rank-one root lattice ⟨-2⟩.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.IntegralLattice.hyperbolicPlane : IntegralLattice (Fin 2 → ℚ)

The hyperbolic plane, with Gram matrix !![0, 1; 1, 0].

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.IntegralLattice.affineA1 : IntegralLattice (Fin 2 → ℚ)

The degenerate affine A₁ lattice, with Gram matrix !![2, -2; -2, 2].

Equations

• TauCeti.IntegralLattice.affineA1 = TauCeti.IntegralLattice.ofGramMatrix (Pi.basisFun ℚ (Fin 2)) TauCeti.IntegralLattice.affineA1Matrix✝ TauCeti.IntegralLattice.affineA1._proof_1✝

@[simp]

theorem TauCeti.IntegralLattice.mem_a1_carrier_iff (x : ℚ) : x ∈ a1.carrier ↔ ∃ (z : ℤ), ↑z = x

Membership in the A₁ carrier means being an integer inside ℚ.

@[simp]

theorem TauCeti.IntegralLattice.mem_negativeA1_carrier_iff (x : ℚ) : x ∈ negativeA1.carrier ↔ ∃ (z : ℤ), ↑z = x

Membership in the negative A₁ carrier means being an integer inside ℚ.

@[simp]

theorem TauCeti.IntegralLattice.mem_hyperbolicPlane_carrier_iff (x : Fin 2 → ℚ) : x ∈ hyperbolicPlane.carrier ↔ ∀ (i : Fin 2), ∃ (z : ℤ), ↑z = x i

A vector belongs to the hyperbolic-plane carrier exactly when both coordinates are integers.

@[simp]

theorem TauCeti.IntegralLattice.mem_affineA1_carrier_iff (x : Fin 2 → ℚ) : x ∈ affineA1.carrier ↔ ∀ (i : Fin 2), ∃ (z : ℤ), ↑z = x i

A vector belongs to the affine A₁ carrier exactly when both coordinates are integers.

@[simp]

theorem TauCeti.IntegralLattice.a1_form_apply (x y : ℚ) : (a1.form x) y = 2 * x * y

The A₁ form evaluates as twice the product of its two inputs.

@[simp]

theorem TauCeti.IntegralLattice.negativeA1_form_apply (x y : ℚ) : (negativeA1.form x) y = -2 * x * y

The negative A₁ form evaluates as negative twice the product of its two inputs.

@[simp]

theorem TauCeti.IntegralLattice.hyperbolicPlane_form_apply (x y : Fin 2 → ℚ) : (hyperbolicPlane.form x) y = x 0 * y 1 + x 1 * y 0

The hyperbolic-plane form pairs opposite coordinates.

@[simp]

theorem TauCeti.IntegralLattice.affineA1_form_apply (x y : Fin 2 → ℚ) : (affineA1.form x) y = 2 * (x 0 - x 1) * (y 0 - y 1)

The affine A₁ form is twice the product of the coordinate differences.

Norms and arithmetic invariants

@[simp]

theorem TauCeti.IntegralLattice.a1_norm_apply (x : ℚ) : a1.norm x = 2 * x ^ 2

The norm on the positive rank-one lattice is twice a square.

@[simp]

theorem TauCeti.IntegralLattice.negativeA1_norm_apply (x : ℚ) : negativeA1.norm x = -2 * x ^ 2

The norm on the negative rank-one lattice is negative twice a square.

@[simp]

theorem TauCeti.IntegralLattice.hyperbolicPlane_norm_apply (x : Fin 2 → ℚ) : hyperbolicPlane.norm x = 2 * x 0 * x 1

The norm on the hyperbolic plane is twice the product of its coordinates.

@[simp]

theorem TauCeti.IntegralLattice.affineA1_norm_apply (x : Fin 2 → ℚ) : affineA1.norm x = 2 * (x 0 - x 1) ^ 2

The norm on the affine A₁ lattice is twice the square of the coordinate difference.

theorem TauCeti.IntegralLattice.isEven_a1 : a1.IsEven

The positive rank-one lattice is even.

theorem TauCeti.IntegralLattice.isEven_negativeA1 : negativeA1.IsEven

The negative rank-one lattice is even.

theorem TauCeti.IntegralLattice.isEven_hyperbolicPlane : hyperbolicPlane.IsEven

The hyperbolic plane is even.

theorem TauCeti.IntegralLattice.isEven_affineA1 : affineA1.IsEven

The affine A₁ lattice is even.

@[simp]

theorem TauCeti.IntegralLattice.hyperbolicPlane_determinant : hyperbolicPlane.determinant = -1

The signed determinant of the hyperbolic plane is -1.

@[simp]

theorem TauCeti.IntegralLattice.hyperbolicPlane_discriminant : hyperbolicPlane.discriminant = 1

The hyperbolic plane has discriminant one, the determinant form of unimodularity.

@[simp]

theorem TauCeti.IntegralLattice.affineA1_determinant : affineA1.determinant = 0

The signed determinant of the affine A₁ lattice vanishes.

Definiteness and signatures

theorem TauCeti.IntegralLattice.isIndefinite_hyperbolicPlane : hyperbolicPlane.IsIndefinite

The hyperbolic plane is indefinite.

theorem TauCeti.IntegralLattice.infinite_vectorsOfNorm_zero_hyperbolicPlane : (hyperbolicPlane.vectorsOfNorm 0).Infinite

The hyperbolic plane has an infinite shell of norm zero. It is nondegenerate, but every integer multiple of the first coordinate vector is isotropic, so the finiteness of shells of a positive definite lattice cannot be weakened to nondegeneracy.

@[simp]

theorem TauCeti.IntegralLattice.hyperbolicPlane_signature : hyperbolicPlane.signature = (1, 0, 1)

The hyperbolic plane has signature (1, 0, 1).

theorem TauCeti.IntegralLattice.isNegDef_negativeA1 : negativeA1.IsNegDef

The negative rank-one root lattice is negative-definite.

@[simp]

theorem TauCeti.IntegralLattice.negativeA1_signature : negativeA1.signature = (0, 0, 1)

The negative rank-one root lattice has signature (0, 0, 1).

theorem TauCeti.IntegralLattice.isPosSemidef_affineA1 : affineA1.IsPosSemidef

The affine A₁ lattice is positive-semidefinite.

theorem TauCeti.IntegralLattice.isDegenerate_affineA1 : affineA1.IsDegenerate

The affine A₁ lattice is degenerate.

@[simp]

theorem TauCeti.IntegralLattice.affineA1_signature : affineA1.signature = (1, 1, 0)

The affine A₁ lattice has signature (1, 1, 0).

The affine radical quotient

def TauCeti.IntegralLattice.affineA1Difference : (Fin 2 → ℚ) →ₗ[ℚ] ℚ

The coordinate difference map used to identify the affine A₁ quotient.

Equations

• TauCeti.IntegralLattice.affineA1Difference = LinearMap.proj 0 - LinearMap.proj 1

@[simp]

theorem TauCeti.IntegralLattice.affineA1Difference_apply (x : Fin 2 → ℚ) : affineA1Difference x = x 0 - x 1

The affine coordinate difference map sends x to x₀ - x₁.

theorem TauCeti.IntegralLattice.affineA1_radical_eq_ker : affineA1.radical = affineA1Difference.ker

The radical of affine A₁ is the kernel of the coordinate difference.

theorem TauCeti.IntegralLattice.affineA1Difference_surjective : Function.Surjective ⇑affineA1Difference

The coordinate difference map is onto.

noncomputable def TauCeti.IntegralLattice.affineA1QuotientEquiv : ((Fin 2 → ℚ) ⧸ affineA1.radical) ≃ₗ[ℚ] ℚ

The rational radical quotient of affine A₁, expressed by coordinate difference.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.IntegralLattice.affineA1QuotientEquiv_mk (x : Fin 2 → ℚ) : affineA1QuotientEquiv (Submodule.Quotient.mk x) = x 0 - x 1

The quotient equivalence acts on representatives by coordinate difference.

noncomputable def TauCeti.IntegralLattice.affineA1RadicalQuotientIsometry : affineA1.radicalQuotient.Isometry a1

The radical quotient of affine A₁ is isometric, as an integral lattice, to A₁.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.IntegralLattice.affineA1RadicalQuotientIsometry_mk (x : Fin 2 → ℚ) : affineA1RadicalQuotientIsometry (Submodule.Quotient.mk x) = x 0 - x 1

The affine radical-quotient isometry acts on representatives by coordinate difference.

@[simp]

theorem TauCeti.IntegralLattice.affineA1RadicalQuotientIsometry_symm_apply (y : ℚ) : affineA1RadicalQuotientIsometry.symm y = Submodule.Quotient.mk ![y, 0]

The inverse affine radical-quotient isometry sends y to the class of ![y, 0].