Integral lattices in a real vector space

The combinatorics of a toric variety takes place in a real vector space V carrying a distinguished additive map i : N →+ V from an abelian group of integral vectors. For that picture to determine anything, N has to be finite free over ℤ and V has to be the real scalar extension of N along i: the latter is exactly Mathlib's IsBaseChange ℝ condition on the ℤ-linear map underlying i, and TauCeti.Toric.IsIntegralLattice is the name this development gives this interface.

Injectivity of i together with a full real span is strictly weaker and is not enough. The map ℤ² →+ ℝ, (a, b) ↦ a + √2 * b, is injective and its image spans ℝ, yet its image is dense, so its positive image has arbitrarily small elements and a ray has no least positive lattice vector to serve as its "primitive generator". The scalar-extension condition rules this out by forcing the integral and real ranks to agree.

Main declarations

• TauCeti.Toric.IsIntegralLattice: for finite free N, the scalar-extension condition on i : N →+ V, stated as Mathlib's IsBaseChange ℝ for the underlying ℤ-linear map. isIntegralLattice_iff is the equivalent formulation by an ℝ-linear equivalence ℝ ⊗[ℤ] N ≃ₗ[ℝ] V restricting to i.
• TauCeti.Toric.isIntegralLattice_of_basis: an integral basis of N whose image is a real basis of V exhibits an integral lattice.
• TauCeti.Toric.IsIntegralLattice.injective, TauCeti.Toric.IsIntegralLattice.span_range_eq_top and TauCeti.Toric.IsIntegralLattice.finrank_eq: an integral lattice is injective with full real span, and the integral rank of N equals the real dimension of V.
• TauCeti.Toric.linearIndependent_comp_iff_of_liftBaseChange_injective: when the real-linear map ℝ ⊗[ℤ] N →ₗ[ℝ] V induced by i is injective (as it is when i extends scalars from ℤ to ℝ, by IsBaseChange.liftBaseChange_injective), a family of integral vectors is linearly independent over ℤ exactly when its image is linearly independent over ℝ.
• TauCeti.Toric.IsIntegralLattice.linearIndependent_basis: the images of the vectors of an integral basis are linearly independent over the reals.
• TauCeti.Toric.IsIntegralLattice.extend and TauCeti.Toric.IsIntegralLattice.eq_extend: a map of integral vectors extends to a unique real-linear map, so the real-linear map accompanying a map of lattices is determined by it rather than being extra data.
• TauCeti.Toric.IsIntegralLattice.realCharacter and TauCeti.Toric.IsIntegralLattice.eq_realCharacter: an integral character extends to a unique real-linear functional, additively in the character.
• TauCeti.Toric.IsIntegralLattice.exists_realCharacter_apply_eq: every additive real-valued function on the integral characters is evaluation at a point of V.
• TauCeti.Toric.IsIntegralLattice.prod: products of integral lattices are integral lattices for the componentwise lattice map.
• TauCeti.Toric.IsIntegralLattice.isZLattice: in a normed space the image of an integral lattice is discrete, hence a ZLattice in Mathlib's sense.
• TauCeti.Toric.isIntegralLattice_subtype_of_isZLattice: conversely, a full ZLattice in a finite-dimensional space is an integral lattice for its inclusion.

Implementation notes

IsIntegralLattice packages finite freeness of the source with a named specialization of IsBaseChange: it fixes the ring extension ℤ → ℝ, takes the bare additive map i that the ambient cone geometry uses, and is the vocabulary in which toric cones, fans and their morphisms are stated. The IsIntegralLattice.isBaseChange projection is the interface that downstream modules use to reach the whole of Mathlib's base-change API.

References

The mathematics is §1.2 of D. Cox, J. Little and H. Schenck, Toric Varieties, and §1.2 of W. Fulton, Introduction to Toric Varieties.

structure TauCeti.Toric.IsIntegralLattice {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] (i : N →+ V) : Prop

An additive map i : N →+ V from a finite free ℤ-module into a real vector space is an integral lattice when it exhibits V as the extension of scalars of N from ℤ to ℝ.

• free : Module.Free ℤ N

  The module of integral vectors is free.

• finite : Module.Finite ℤ N

  The module of integral vectors is finitely generated.

• isBaseChange : IsBaseChange ℝ i.toIntLinearMap

  Extending scalars from ℤ to ℝ along i gives the ambient real vector space.

theorem TauCeti.Toric.isIntegralLattice_iff {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} : IsIntegralLattice i ↔ Module.Free ℤ N ∧ Module.Finite ℤ N ∧ ∃ (e : TensorProduct ℤ ℝ N ≃ₗ[ℝ] V), ∀ (n : N), e (1 ⊗ₜ[ℤ] n) = i n

An integral lattice, spelled by the scalar-extension equivalence it provides.

theorem TauCeti.Toric.isIntegralLattice_of_basis {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {ι : Type u_3} [Finite ι] (b : Module.Basis ι ℤ N) (c : Module.Basis ι ℝ V) (hbc : ∀ (j : ι), i (b j) = c j) : IsIntegralLattice i

An integral basis of N whose image under i is a real basis of V exhibits i as an integral lattice.

theorem TauCeti.Toric.IsIntegralLattice.injective {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (h : IsIntegralLattice i) : Function.Injective ⇑i

An integral lattice is injective.

theorem TauCeti.Toric.linearIndependent_comp_iff_of_liftBaseChange_injective {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (h : Function.Injective ⇑(LinearMap.liftBaseChange ℝ i.toIntLinearMap)) {ι : Type u_3} {v : ι → N} : LinearIndependent ℝ (⇑i ∘ v) ↔ LinearIndependent ℤ v

When the real-linear map ℝ ⊗[ℤ] N →ₗ[ℝ] V induced by i is injective (for instance when i extends scalars from ℤ to ℝ, by IsBaseChange.liftBaseChange_injective), a family of integral vectors is linearly independent over ℤ exactly when its image under i is linearly independent over ℝ: a real linear relation among lattice vectors forces an integral one. The image of i need not span V.

theorem TauCeti.Toric.IsIntegralLattice.span_range_eq_top {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (h : IsIntegralLattice i) : Submodule.span ℝ (Set.range ⇑i) = ⊤

The image of an integral lattice spans the ambient real vector space.

theorem TauCeti.Toric.IsIntegralLattice.finrank_eq {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (h : IsIntegralLattice i) : Module.finrank ℤ N = Module.finrank ℝ V

The integral rank of the lattice equals the real dimension of the ambient space.

theorem TauCeti.Toric.IsIntegralLattice.finiteDimensional {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (h : IsIntegralLattice i) : FiniteDimensional ℝ V

An integral lattice sits in a finite-dimensional real vector space.

theorem TauCeti.Toric.IsIntegralLattice.range_eq_span {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {ι : Type u_3} (h : IsIntegralLattice i) (b : Module.Basis ι ℤ N) : i.toIntLinearMap.range = Submodule.span ℤ (Set.range ⇑(IsBaseChange.basis b ⋯))

The range of an integral lattice is the ℤ-span of the real basis attached to an integral basis of N.

theorem TauCeti.Toric.IsIntegralLattice.linearIndependent_basis {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {ι : Type u_3} (h : IsIntegralLattice i) (b : Module.Basis ι ℤ N) : LinearIndependent ℝ fun (j : ι) => i (b j)

The images of the vectors of an integral basis of an integral lattice are linearly independent over the reals.

Maps of lattices

noncomputable def TauCeti.Toric.IsIntegralLattice.extend {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} (h : IsIntegralLattice i) (i' : N' →+ V') (f : N →+ N') : V →ₗ[ℝ] V'

The real-linear map extending a map f : N →+ N' of integral vectors.

@[simp]

theorem TauCeti.Toric.IsIntegralLattice.extend_apply {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} (h : IsIntegralLattice i) (i' : N' →+ V') (f : N →+ N') (n : N) : (h.extend i' f) (i n) = i' (f n)

theorem TauCeti.Toric.IsIntegralLattice.eq_extend {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} (h : IsIntegralLattice i) {f : N →+ N'} {g : V →ₗ[ℝ] V'} (hg : ∀ (n : N), g (i n) = i' (f n)) : g = h.extend i' f

A real-linear map compatible with a map of integral vectors is the extension of it. This is what makes the real-linear part of a map of lattices determined rather than chosen.

@[simp]

theorem TauCeti.Toric.IsIntegralLattice.extend_id {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (h : IsIntegralLattice i) : h.extend i (AddMonoidHom.id N) = LinearMap.id

@[simp]

theorem TauCeti.Toric.IsIntegralLattice.extend_comp {N : Type u_1} {N' : Type u_2} {N'' : Type u_3} {V : Type u_4} {V' : Type u_5} {V'' : Type u_6} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup N''] [AddCommGroup V] [AddCommGroup V'] [AddCommGroup V''] [Module ℝ V] [Module ℝ V'] [Module ℝ V''] {i : N →+ V} {i' : N' →+ V'} {i'' : N'' →+ V''} (h : IsIntegralLattice i) (h' : IsIntegralLattice i') (f : N →+ N') (f' : N' →+ N'') : h'.extend i'' f' ∘ₗ h.extend i' f = h.extend i'' (f'.comp f)

noncomputable def TauCeti.Toric.IsIntegralLattice.realCharacter {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (h : IsIntegralLattice i) : (N →+ ℤ) →+ Module.Dual ℝ V

The real-linear extension of an integral character. Extension is additive in the character, so this is bundled as an additive homomorphism into the real dual space.

@[simp]

theorem TauCeti.Toric.IsIntegralLattice.realCharacter_apply {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (h : IsIntegralLattice i) (m : N →+ ℤ) (n : N) : (h.realCharacter m) (i n) = ↑(m n)

Extending an integral character and evaluating it on a lattice point recovers the integer value of the character, viewed as a real number.

theorem TauCeti.Toric.IsIntegralLattice.eq_realCharacter {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (h : IsIntegralLattice i) {m : N →+ ℤ} {φ : Module.Dual ℝ V} (hφ : ∀ (n : N), φ (i n) = ↑(m n)) : φ = h.realCharacter m

A real-linear functional agreeing with an integral character on lattice points is the real extension of that character.

theorem TauCeti.Toric.IsIntegralLattice.realCharacter_coord {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {ι : Type u_7} (h : IsIntegralLattice i) (b : Module.Basis ι ℤ N) (j : ι) : h.realCharacter (b.coord j).toAddMonoidHom = (IsBaseChange.basis b ⋯).coord j

The real extension of an integral coordinate character is the corresponding coordinate of the real basis attached to an integral basis.

theorem TauCeti.Toric.IsIntegralLattice.exists_realCharacter_eq_iff {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (h : IsIntegralLattice i) {φ : Module.Dual ℝ V} : (∃ (m : N →+ ℤ), h.realCharacter m = φ) ↔ ∀ (n : N), ∃ (k : ℤ), φ (i n) = ↑k

A real-linear functional is the real extension of an integral character exactly when it takes integer values at every lattice point.

theorem TauCeti.Toric.IsIntegralLattice.realCharacter_injective {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (h : IsIntegralLattice i) : Function.Injective ⇑h.realCharacter

Real extension of integral characters is injective.

theorem TauCeti.Toric.IsIntegralLattice.exists_realCharacter_apply_eq {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (h : IsIntegralLattice i) (f : (N →+ ℤ) →+ ℝ) : ∃ (v : V), ∀ (m : N →+ ℤ), (h.realCharacter m) v = f m

Every additive real-valued function on the integral characters is evaluation at a point of the ambient real space: the real extensions of the characters identify V with the real-valued additive functions on N →+ ℤ.

theorem TauCeti.Toric.IsIntegralLattice.realCharacter_comp {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} (h : IsIntegralLattice i) (h' : IsIntegralLattice i') (f : N →+ N') (g : V →ₗ[ℝ] V') (hfg : ∀ (n : N), g (i n) = i' (f n)) (m : N' →+ ℤ) : h.realCharacter (m.comp f) = h'.realCharacter m ∘ₗ g

Real extension commutes with a compatible map of lattices.

theorem TauCeti.Toric.isIntegralLattice_congr {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} (f : N ≃+ N') (e : V ≃ₗ[ℝ] V') (hfe : ∀ (n : N), e (i n) = i' (f n)) : IsIntegralLattice i ↔ IsIntegralLattice i'

Being an integral lattice transfers along an isomorphism of the integral vectors together with a compatible real-linear equivalence.

theorem TauCeti.Toric.IsIntegralLattice.prod {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} (h : IsIntegralLattice i) (h' : IsIntegralLattice i') : IsIntegralLattice (i.prodMap i')

The product of two integral lattices is an integral lattice for the componentwise map.

@[simp]

theorem TauCeti.Toric.IsIntegralLattice.realCharacter_coprod {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} (h : IsIntegralLattice i) (h' : IsIntegralLattice i') (m : N →+ ℤ) (m' : N' →+ ℤ) : ⋯.realCharacter (m.coprod m') = LinearMap.coprod (h.realCharacter m) (h'.realCharacter m')

Real extension of the sum of characters on the two factors of a product lattice is the sum of their real extensions.

Discreteness

theorem TauCeti.Toric.IsIntegralLattice.discreteTopology {N : Type u_1} {V : Type u_2} [AddCommGroup N] [NormedAddCommGroup V] [NormedSpace ℝ V] {i : N →+ V} (h : IsIntegralLattice i) : DiscreteTopology ↥i.toIntLinearMap.range

The image of an integral lattice is a discrete subgroup of a normed real vector space; this is what fails for an injective map with dense image.

theorem TauCeti.Toric.IsIntegralLattice.isZLattice {N : Type u_1} {V : Type u_2} [AddCommGroup N] [NormedAddCommGroup V] [NormedSpace ℝ V] {i : N →+ V} (h : IsIntegralLattice i) : IsZLattice ℝ i.toIntLinearMap.range

The image of an integral lattice is a ℤ-lattice in Mathlib's sense.

theorem TauCeti.Toric.isIntegralLattice_subtype_of_isZLattice {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (L : Submodule ℤ V) [DiscreteTopology ↥L] [IsZLattice ℝ L] : IsIntegralLattice L.subtype.toAddMonoidHom

Conversely, a full ℤ-lattice in Mathlib's sense, in a finite-dimensional normed real vector space, is an integral lattice for its inclusion: the space is the real scalar extension of the lattice.

The standard lattice

theorem TauCeti.Toric.isIntegralLattice_intCast (n : ℕ) : IsIntegralLattice ((Int.castAddHom ℝ).compLeft (Fin n))

The standard lattice ℤ^n ⊆ ℝ^n given by the coordinatewise integer cast.