feat: Gordan's lemma

Polyhedral.lean

@@ -2,6 +2,7 @@ module  -- shake: keep-all --deprecated_module: ignore
 
 public import Polyhedral.Mathlib.Algebra.Group.Pointwise.SetLike.Basic
 public import Polyhedral.Mathlib.Algebra.Group.Pointwise.SetLike.Scalar
+public import Polyhedral.Mathlib.Algebra.Module.Lattice.Basic
 public import Polyhedral.Mathlib.Algebra.Module.LinearMap
 public import Polyhedral.Mathlib.Algebra.Module.Submodule.Basic
 public import Polyhedral.Mathlib.Algebra.Module.Submodule.Dual.Basic
@@ -35,6 +36,7 @@ public import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Finite.Face.Grade
 public import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Finite.Face.KreinMilman
 public import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Finite.Face.Rank
 public import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Finite.MinkowskiWeyl
+public import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Gordan
 public import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Lineal
 public import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.LinearMap
 public import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Rank

Polyhedral/Mathlib/Algebra/Module/Lattice/Basic.lean

@@ -0,0 +1,172 @@
+/-
+Copyright (c) 2026 Anouk Brose, Justus Springer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anouk Brose, Justus Springer
+-/
+module
+
+public import Mathlib.LinearAlgebra.Dimension.Localization
+public import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
+public import Mathlib.LinearAlgebra.FreeModule.PID
+public import Mathlib.Algebra.Module.Torsion.Free
+public import Mathlib.Algebra.Module.Lattice
+
+/-!
+# Lattices
+
+A generalization of mathlib's `Submodule.IsLattice` to make it useful for Polyhedral.
+This definition is used in the proof of Gordan's lemma, see
+`Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Gordan.lean`.
+
+We (The Ehrhart group from the workshop) will work on upstreaming this into mathlib,
+to replace the existing definition. See Zulip discussion:
+
+https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Definitions.20of.20lattices/with/620077176
+
+-/
+
+@[expose] public section
+
+open Module
+open scoped Pointwise
+
+universe v w
+
+variable {R : Type*} [CommRing R]
+
+namespace Submodule
+
+/-- Let `K` be a `R`-algebra and `V` a `K`-module.
+A lattice is a `R`-submodule `M ≤ V` that is finitely generated such that every `R`-independent
+subset of `M` is `K`-linearly independent. Equivalently, the `R`-rank of `M` equals the
+`K`-dimension of its `K`-span, see `Submodule.isLattice'_iff_fg_and_finrank_eq`. -/
+class IsLattice' (A : outParam Type*) [CommRing A] [Algebra R A] {V : Type v} [AddCommMonoid V]
+    [Module R V] [Module A V] [IsScalarTower R A V] (M : Submodule R V) : Prop where
+  fg : M.FG
+  linearIndepOn : ∀ s ⊆ (M : Set V), LinearIndepOn R id s → LinearIndepOn A id s
+
+namespace IsLattice'
+
+section CommRing
+
+variable (A : Type*) [CommRing A] [Algebra R A]
+variable {V : Type v} [AddCommGroup V] [Module R V] [Module A V] [IsScalarTower R A V]
+variable (M : Submodule R V)
+
+/-- Any `R`-independent family of vectors in a lattice is `K`-linearly independent. -/
+theorem linearIndependent [IsLattice' A M] {ι : Type*} {v : ι → V}
+    (hv : ∀ i, v i ∈ M) (h : LinearIndependent R v) : LinearIndependent A v := by
+  cases subsingleton_or_nontrivial R
+  · have := (algebraMap R A).codomain_trivial
+    exact linearIndependent_of_subsingleton
+  exact (linearIndepOn_id_range_iff h.injective).mp <|
+    IsLattice'.linearIndepOn _ (Set.range_subset_iff.mpr hv) h.linearIndepOn_id
+
+/-- Any basis of an `R`-lattice in `V` is `K`-linearly independent. -/
+theorem basis_linearIndependent {I : Type w} {M : Submodule R V}
+    [IsLattice' A M] (b : Basis I R M) : LinearIndependent A (fun i ↦ (b i).val) :=
+  IsLattice'.linearIndependent A M (fun i ↦ (b i).2)
+    (b.linearIndependent.map' M.subtype (Submodule.ker_subtype _))
+
+/-- Any `R`-lattice is finite. -/
+instance finite [IsLattice' A M] : Module.Finite R M := by
+  rw [Module.Finite.iff_fg]
+  exact IsLattice'.fg
+
+theorem mono_of_fg {M N : Submodule R V} (hle : M ≤ N) (hfg : M.FG) [IsLattice' A N] :
+    IsLattice' A M where
+  fg := hfg
+  linearIndepOn s hs hli := linearIndepOn s (hs.trans hle) hli
+
+/-- Over a Noetherian ring, any submodule of a lattice is a lattice. -/
+theorem mono [IsNoetherianRing R] {M N : Submodule R V} (hle : M ≤ N) [IsLattice' A N] :
+    IsLattice' A M :=
+  mono_of_fg A hle (isNoetherian_submodule.mp inferInstance M hle)
+
+/-- Over a Noetherian ring, the intersection of two lattices is a lattice. -/
+instance inf [IsNoetherianRing R] (M N : Submodule R V) [IsLattice' A M] [IsLattice' A N] :
+    IsLattice' A (M ⊓ N) :=
+  mono A inf_le_left
+
+end CommRing
+
+section Field
+
+variable (K : Type*) [Field K] [Algebra R K] [FaithfulSMul R K]
+variable {V : Type v} [AddCommGroup V] [Module R V] [Module K V] [IsScalarTower R K V]
+variable (M : Submodule R V)
+
+-- This has been merged into mathlib: #43297
+theorem rank_span_le_rank : Module.rank K (span K (M : Set V)) ≤ Module.rank R M := by
+  have : Nontrivial R := (algebraMap R K).domain_nontrivial
+  obtain ⟨b, hbM, hbspan, hbli⟩ := exists_linearIndependent K (M : Set V)
+  rw [← hbspan, rank_span_set hbli]
+  have hb : LinearIndependent R (fun x : b ↦ (⟨x.1, hbM x.2⟩ : M)) :=
+    LinearIndependent.of_comp M.subtype (hbli.restrict_scalars' R)
+  exact hb.cardinal_le_rank
+
+/-- The `R`-rank of a lattice equals the `K`-dimension of its `K`-span. -/
+theorem rank_eq_rank_span [IsLattice' K M] :
+    Module.rank R M = Module.rank K (span K (M : Set V)) := by
+  -- AI slop, needs refactor
+  refine le_antisymm ?_ (rank_span_le_rank K M)
+  rw [Module.rank]
+  apply ciSup_le'
+  intro ⟨s, hs⟩
+  have hR : LinearIndependent R (fun x : s ↦ ((x : M) : V)) :=
+    hs.map' M.subtype (Submodule.ker_subtype _)
+  have hK : LinearIndependent K (fun x : s ↦ ((x : M) : V)) :=
+    IsLattice'.linearIndependent K M (fun x ↦ (x : M).2) hR
+  have hmem : ∀ x : s, ((x : M) : V) ∈ span K (M : Set V) := fun x ↦ subset_span (x : M).2
+  have hW : LinearIndependent K
+      (fun x : s ↦ (⟨((x : M) : V), hmem x⟩ : span K (M : Set V))) :=
+    LinearIndependent.of_comp (span K (M : Set V)).subtype hK
+  exact hW.cardinal_le_rank
+
+/-- The `R`-rank of a lattice equals the `K`-dimension of its `K`-span. -/
+theorem finrank_eq_finrank_span [IsLattice' K M] :
+    finrank R M = finrank K (span K (M : Set V)) :=
+  congrArg Cardinal.toNat (rank_eq_rank_span K M)
+
+theorem _root_.Submodule.isLattice'_iff_fg_and_finrank_eq :
+    IsLattice' K M ↔ M.FG ∧ finrank R M = finrank K (span K (M : Set V)) := by
+  -- Steinitz argument?
+  sorry
+
+section IsPrincipalIdealRing
+
+variable [IsDomain R] [IsPrincipalIdealRing R]
+
+/-- Any lattice over a PID is a free `R`-module. -/
+instance free (M : Submodule R V) [IsLattice' K M] : Module.Free R M := by
+  have := Module.IsTorsionFree.trans_faithfulSMul R K V
+  -- any torsion free finite module over a PID is free
+  infer_instance
+
+/-- A lattice over a PID has a basis that's `K`-linearly independent. -/
+theorem exists_basis_linearIndependent (M : Submodule R V) [IsLattice' K M] :
+    ∃ (I : Type v) (b : Basis I R M), LinearIndependent K (fun i ↦ (b i).val) := by
+  obtain ⟨I, b⟩ := Module.Free.exists_basis R M
+  exact ⟨I, b, basis_linearIndependent K b⟩
+
+end IsPrincipalIdealRing
+
+section IsFractionRing
+
+variable (K : Type*) [Field K] [Algebra R K] [IsFractionRing R K]
+variable {V : Type*} [AddCommGroup V] [Module R V] [Module K V] [IsScalarTower R K V]
+
+/-- If `K` is the field of fractions of `R`, any finitely generated `R`-submodule of `V`
+is a lattice. -/
+theorem of_fg {M : Submodule R V} (hM : M.FG) : IsLattice' K M where
+  fg := hM
+  linearIndepOn v hvM hv := by
+    sorry
+
+end IsFractionRing
+
+end Field
+
+end IsLattice'
+
+end Submodule

Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Ehrhart/Gordan.lean

@@ -0,0 +1,180 @@
+/-
+Copyright (c) 2026 Justus Springer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anouk Brose, Mei Han, Noah Gießing, Jesus de Loera, Justus Springer, Santiago Morales
+-/
+module
+
+public import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Basic
+public import Polyhedral.Mathlib.Algebra.Module.Lattice.Basic
+public import Mathlib.Algebra.Order.Floor.Ring
+public import Mathlib.Algebra.EuclideanDomain.Int
+public import Mathlib.Data.Int.Interval
+
+/-!
+# Gordan's lemma
+
+For a lattice `Λ` in a `K`-vector space `V` and a finite family `r : ι → Λ`, the monoid of lattice
+points of the cone spanned by `r` is generated by `r` together with the lattice points of the
+half-open parallelepiped spanned by `r`. If `r` is `K`-linearly independent, the decomposition is
+unique.
+
+-/
+
+@[expose] public section
+
+variable (K : Type*) [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K]
+variable {V : Type*} [AddCommGroup V] [Module K V]
+
+/-- The monoid of lattice points of a pointed cone in a lattice. -/
+abbrev PointedCone.latticePoints (C : PointedCone K V) (Λ : Submodule ℤ V) : AddSubmonoid V :=
+  C.toAddSubmonoid ⊓ Λ.toAddSubmonoid
+
+namespace Gordan
+
+open Module
+
+variable {ι : Type*} [Fintype ι]
+variable (Λ : Submodule ℤ V) (r : ι → Λ)
+
+/-- The cone spanned by the lattice vectors `r`. -/
+abbrev cone : PointedCone K V := PointedCone.hull K (Set.range (Subtype.val ∘ r))
+
+/-- The half-open parallelepiped spanned by the rays `r`. -/
+def parallelepiped : Set V :=
+  { x | ∃ μ : ι → K, (∀ i, μ i ∈ Set.Ico (0 : K) 1) ∧ x = ∑ i, μ i • (r i : V) }
+
+omit [IsStrictOrderedRing K] [FloorRing K] in
+lemma mem_parallelepiped_iff {x : V} :
+    x ∈ parallelepiped K Λ r ↔
+      ∃ μ : ι → K, (∀ i, μ i ∈ Set.Ico (0 : K) 1) ∧ x = ∑ i, μ i • (r i : V) :=
+  Iff.rfl
+
+omit [FloorRing K] in
+lemma parallelepiped_subset_cone : parallelepiped K Λ r ⊆ (cone K Λ r : Set V) := by
+  rintro x ⟨μ, hμ, rfl⟩
+  refine Submodule.sum_mem _ fun i _ ↦ ?_
+  have h : μ i • (r i : V) = (⟨μ i, (hμ i).1⟩ : {c : K // 0 ≤ c}) • (r i : V) := rfl
+  rw [h]
+  exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨i, rfl⟩)
+
+omit [FloorRing K] in
+/-- Finiteness of the parallelepiped intersected with the lattice. -/
+theorem parallelepiped_inter_lattice_finite [Λ.IsLattice' K] :
+    (parallelepiped K Λ r ∩ (Λ : Set V)).Finite := by
+  -- Proof starts here
+  obtain ⟨I, v, hv⟩ := Submodule.IsLattice'.exists_basis_linearIndependent K Λ
+  have : Finite I := Module.Finite.finite_basis v
+  have := Fintype.ofFinite I
+  let box : Set V := (fun c ↦ ∑ j, c j • v j) ''
+      {c : I → ℤ | ∀ j, c j ∈ Set.Icc (-∑ i, |v.repr (r i) j|) (∑ i, |v.repr (r i) j|)}
+  apply Set.Finite.subset (s := box) ((Set.Finite.pi' fun j ↦ Set.finite_Icc _ _).image _)
+  rintro x ⟨⟨μ, hμ, hx⟩, hxΛ⟩
+  let c (i : I) := v.repr ⟨x, hxΛ⟩ i
+  have key (y : Λ) : y.1 = ∑ j, v.repr y j • (v j : V) := by
+    simp_rw [← Submodule.coe_smul, ← Submodule.coe_sum, v.sum_repr]
+  have hxc : x = ∑ j, c j • (v j).1 := key ⟨x, hxΛ⟩
+  have hr (i : ι) : r i = ∑ j, v.repr (r i) j • (v j).1 := key (r i)
+  have hcμ : ∀ j, c j = ∑ i, μ i * v.repr (r i) j := Fintype.linearIndependent_iffₛ.mp hv _ _ <| by
+    simpa only [Int.cast_smul_eq_zsmul, ← hxc, hx, hr, Finset.smul_sum,
+      Finset.sum_smul, mul_smul] using Finset.sum_comm
+  refine ⟨c, fun j ↦ abs_le.mp ?_, hxc.symm⟩
+  grw [← Int.cast_le (R := K), Int.cast_abs, hcμ, Finset.abs_sum_le_sum_abs]
+  push_cast [abs_mul, abs_of_nonneg (hμ _).1]
+  exact Finset.sum_le_sum fun i _ ↦ mul_le_of_le_one_left (abs_nonneg _) (hμ i).2.le
+
+/-- Every lattice point of the cone is the sum of a lattice point of the half-open parallelepiped
+and an `ℕ`-combination of the rays. Split the coefficients into integer and fractional parts. -/
+theorem exists_decomp (γ : V) (hγ : γ ∈ (cone K Λ r).latticePoints K Λ) :
+    ∃ pn : ↥(parallelepiped K Λ r ∩ (Λ : Set V)) × (ι → ℕ),
+      γ = (pn.1 : V) + ∑ i, pn.2 i • (r i : V) := by
+  obtain ⟨c, hc⟩ : ∃ c : ι → Nonneg K, ∑ i, (c i : K) • (r i : V) = γ :=
+    (Submodule.mem_span_range_iff_exists_fun _).mp hγ.1
+  set n : ι → ℕ := fun i ↦ ⌊(c i : K)⌋₊ with hn_def
+  set μ : ι → K := fun i ↦ Int.fract (c i : K) with hμ_def
+  have hsplit (i : ι) : (c i : K) = μ i + (n i : K) := by
+    rw [hn_def, hμ_def, natCast_floor_eq_intCast_floor (c i).2]
+    exact (Int.fract_add_floor (c i : K)).symm
+  simp only [hsplit, add_smul, Nat.cast_smul_eq_nsmul, Finset.sum_add_distrib] at hc
+  refine ⟨(⟨ ∑ i, μ i • (r i : V), ?_, ?_, ⟩, n), hc.symm⟩
+  · exact ⟨μ, fun i ↦ ⟨Int.fract_nonneg _, Int.fract_lt_one _⟩, rfl⟩
+  · rw [eq_sub_of_add_eq hc]
+    exact Λ.sub_mem hγ.2 (Submodule.sum_mem _ fun i _ ↦ nsmul_mem (r i).2 _)
+
+omit [FloorRing K] in
+/-- Uniqueness of `Gordan.exists_decomp`. Needs `K`-linear independence of the rays. -/
+theorem decomp_unique (hr : LinearIndependent K (Subtype.val ∘ r))
+    {pn qm : ↥(parallelepiped K Λ r ∩ (Λ : Set V)) × (ι → ℕ)}
+    (h : (pn.1 : V) + ∑ i, pn.2 i • (r i : V) = (qm.1 : V) + ∑ i, qm.2 i • (r i : V)) :
+    pn = qm := by
+  obtain ⟨⟨p, ⟨a, ha, rfl⟩, hpΛ⟩, n⟩ := pn
+  obtain ⟨⟨q, ⟨b, hb, rfl⟩, hqΛ⟩, m⟩ := qm
+  simp only [← Nat.cast_smul_eq_nsmul K, ← Finset.sum_add_distrib, ← add_smul] at h
+  have hcoeff (i : ι) : a i - b i = (((m i : ℤ) - (n i : ℤ) : ℤ) : K) := by
+    push_cast; linarith [Fintype.linearIndependent_iffₛ.mp hr _ _ h i]
+  have h (i : ι) : |(((m i : ℤ) - (n i : ℤ) : ℤ) : K)| < 1 := by
+    rw [← hcoeff, abs_lt]
+    exact ⟨by linarith [(ha i).1, (hb i).2], by linarith [(ha i).2, (hb i).1]⟩
+  rw [← Int.cast_one] at h
+  simp only [← Int.cast_abs, Int.cast_lt, Int.abs_lt_one_iff] at h
+  simp only [h, Int.cast_zero, sub_eq_zero] at hcoeff
+  simp only [sub_eq_zero, Nat.cast_inj, ← funext_iff] at h
+  simp only [hcoeff, h]
+
+/-- `Gordan.exists_decomp` and `Gordan.decomp_unique` combined. -/
+theorem existsUnique_decomp (hr : LinearIndependent K (Subtype.val ∘ r)) (γ : V)
+    (hγ : γ ∈ (cone K Λ r).latticePoints K Λ) :
+    ∃! pn : ↥(parallelepiped K Λ r ∩ (Λ : Set V)) × (ι → ℕ),
+      γ = (pn.1 : V) + ∑ i, pn.2 i • (r i : V) := by
+  obtain ⟨pn, hpn⟩ := exists_decomp K Λ r γ hγ
+  exact ⟨pn, hpn, fun _ hqm ↦ decomp_unique K Λ r hr (hqm.symm.trans hpn)⟩
+
+omit [FloorRing K] in
+/-- A decomposition is a lattice point of the cone. -/
+lemma decomp_mem (pn : ↥(parallelepiped K Λ r ∩ (Λ : Set V)) × (ι → ℕ)) :
+    (pn.1 : V) + ∑ i, pn.2 i • (r i : V) ∈ (cone K Λ r).latticePoints K Λ := by
+  have hc : ∀ i, (r i : V) ∈ cone K Λ r := fun i ↦ Submodule.subset_span ⟨i, rfl⟩
+  exact ⟨add_mem (parallelepiped_subset_cone K Λ r pn.1.2.1)
+      (Submodule.sum_mem _ fun i _ ↦ nsmul_mem (hc i) _),
+    add_mem pn.1.2.2 (Submodule.sum_mem _ fun i _ ↦ nsmul_mem (r i).2 _)⟩
+
+
+/-- `Gordan.existsUnique_decomp`, packaged as a bijection. -/
+noncomputable def decompEquiv (hr : LinearIndependent K (Subtype.val ∘ r)) :
+    (↥(parallelepiped K Λ r ∩ (Λ : Set V)) × (ι → ℕ)) ≃ ↥((cone K Λ r).latticePoints K Λ) :=
+  Equiv.ofBijective (fun pn ↦ ⟨_, decomp_mem K Λ r pn⟩)
+    ⟨fun _ _ h ↦ decomp_unique K Λ r hr (congrArg Subtype.val h),
+      fun γ ↦ (exists_decomp K Λ r γ γ.2).imp fun _ h ↦ Subtype.ext h.symm⟩
+
+/-- The proposed set of generators. -/
+def generators : Set V :=
+  (parallelepiped K Λ r ∩ (Λ : Set V)) ∪ Set.range (Subtype.val ∘ r)
+
+omit [FloorRing K] in
+theorem generators_finite [Λ.IsLattice' K] : (generators K Λ r).Finite :=
+  (parallelepiped_inter_lattice_finite K Λ r).union (Set.finite_range _)
+
+/-- **Gordan's lemma**: the monoid of lattice points of the cone is generated by
+`Gordan.generators`. -/
+theorem gordan :
+    AddSubmonoid.closure (generators K Λ r) = (cone K Λ r).latticePoints K Λ := by
+  -- AI slop, need to understand and refactor
+  refine le_antisymm (AddSubmonoid.closure_le.mpr ?_) fun γ hγ ↦ ?_
+  · rintro x (⟨hxP, hxΛ⟩ | ⟨i, rfl⟩)
+    · exact ⟨parallelepiped_subset_cone K Λ r hxP, hxΛ⟩
+    · exact ⟨Submodule.subset_span ⟨i, rfl⟩, (r i).2⟩
+  · obtain ⟨⟨p, n⟩, hpn⟩ := exists_decomp K Λ r γ hγ
+    rw [hpn]
+    refine add_mem (AddSubmonoid.subset_closure (Set.mem_union_left _ p.2))
+      (AddSubmonoid.sum_mem _ fun i _ ↦ ?_)
+    have hri : (r i : V) ∈ generators K Λ r := Or.inr ⟨i, rfl⟩
+    exact nsmul_mem (AddSubmonoid.subset_closure hri) _
+
+/-- **Gordan's lemma**, classical form: the monoid of lattice points is finitely generated. -/
+theorem latticePoints_fg {ι : Type*} [Finite ι] (Λ : Submodule ℤ V) (r : ι → Λ)
+    [Λ.IsLattice' K] : ((cone K Λ r).latticePoints K Λ).FG := by
+  cases nonempty_fintype ι
+  exact ⟨(generators_finite K Λ r).toFinset, by
+    rw [Set.Finite.coe_toFinset]; exact gordan K Λ r⟩
+
+end Gordan