feat: homogenization increases (finite) dimension by one

Polyhedral.lean

@@ -72,8 +72,10 @@ public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Defs
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Dimension
+public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.Basic
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.Set
+public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Independent
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Lattice
 public import Polyhedral.Mathlib.LinearAlgebra.BilinearMap
 public import Polyhedral.Mathlib.LinearAlgebra.Dual.Basis

Polyhedral/Mathlib/Data/SetLike/IsConcrete.lean

@@ -104,6 +104,9 @@ variable {A B : Type*} [setLike : SetLike A B] [EmptyCollection A] [IsConcreteEm
 
 @[simp] lemma coe_empty : (∅ : A) = (∅ : Set B) := IsConcreteEmpty.coe_empty'
 
+@[simp, norm_cast]
+lemma coe_eq_empty {a : A} : (a : Set B) = ∅ ↔ a = ∅ := by rw [← coe_empty (A := A), coe_set_eq]
+
 @[simp, grind =, push]
 theorem mem_empty_iff_false {x : B} : x ∈ (∅ : A) ↔ False := by simp [← mem_coe]
 
@@ -124,7 +127,7 @@ include setLike in
 
 include setLike in
 @[simp, grind =]
-theorem le_empty_iff {a : A} : a ≤ ∅ ↔ a = ∅ := by simp [← coe_set_eq, ← coe_subset_coe]
+theorem le_empty_iff {a : A} : a ≤ ∅ ↔ a = ∅ := by simp [← coe_subset_coe]
 
 include setLike in
 theorem eq_empty_of_le_empty {a : A} : a ≤ ∅ → a = ∅ := le_empty_iff.1

Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Rank.lean

@@ -46,9 +46,17 @@ section Semiring
 variable [Semiring R] [PartialOrder R] [IsOrderedRing R]
 variable [AddCommMonoid M] [Module R M]
 
-noncomputable abbrev rank (C : PointedCone R M) := Module.rank R (span R (C : Set M))
+noncomputable def rank (C : PointedCone R M) := Module.rank R (span R (C : Set M))
 
-noncomputable abbrev finrank (C : PointedCone R M) := Module.finrank R (span R (C : Set M))
+noncomputable def finrank (C : PointedCone R M) := Module.finrank R (span R (C : Set M))
+
+@[simp] protected lemma rank_bot [Nontrivial R] : (⊥ : PointedCone R M).rank = 0 :=
+  have : Subsingleton (span R ((⊥ : PointedCone R M) : Set M)) :=
+    Submodule.subsingleton_iff_eq_bot.mpr (by simp)
+  rank_subsingleton' _ _
+
+@[simp] protected lemma finrank_bot [Nontrivial R] : (⊥ : PointedCone R M).finrank = 0 :=
+  Module.finrank_eq_zero_of_rank_eq_zero PointedCone.rank_bot
 
 -- NOTE: this is not the same as Module.Finite or FG!
 abbrev FinRank (C : PointedCone R M) := (span R (C : Set M)).FG
@@ -81,11 +89,11 @@ theorem affineSpan_ne_bot (C : PointedCone R M) : affineSpan R (C : Set M) ≠ 
 
 theorem dim_affineSpan_eq_rank (C : PointedCone R M) :
     (affineSpan R (C : Set M)).dim = C.rank := by
-  simp [affineSpan_eq_span]
+  simp [rank, affineSpan_eq_span]
 
 theorem finDim_affineSpan_eq_finrank (C : PointedCone R M) :
     (affineSpan R (C : Set M)).finDim = C.finrank := by
-  simp [affineSpan_eq_span]
+  simp [finrank, affineSpan_eq_span]
 
 variable [IsDomain R] [Module.IsTorsionFree R M] {C : PointedCone R M}
 

Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Ray.lean

@@ -32,7 +32,7 @@ lemma rank_one_of_ray {x : M} (hx : x ≠ 0) : (hull R {x}).rank = 1 := by
   simpa using hr
 
 lemma finrank_one_of_ray {x : M} (hx : x ≠ 0) : (hull R {x}).finrank = 1 := by
-  simpa [Module.finrank, Cardinal.toNat_eq_one] using rank_one_of_ray hx
+  simpa [finrank, rank, Module.finrank, Cardinal.toNat_eq_one] using rank_one_of_ray hx
 
 end Ring
 

Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean

@@ -7,6 +7,8 @@ module
 
 public import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Convexity
 public import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Lineal
+public import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Rank
+public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.Basic
 
 import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Lattice
@@ -120,7 +122,7 @@ lemma dehomogenize_bot : dehomogenize A (⊥ : PointedCone R W) = ⊥ := by
 @[simp]
 lemma dehomogenize_top : dehomogenize A (⊤ : PointedCone R W) = ⊤ := by
   ext
-  simp [dehomogenize, SetLike.mem_coe.mp]
+  simp [dehomogenize, ← SetLike.mem_coe]
 
 @[simp]
 lemma dehomogenize_weight_positive : dehomogenize A hom.weight.positive = ⊤ :=
@@ -173,6 +175,35 @@ lemma homogenize_top : homogenize W (⊤ : ConvexSet R A) = hom.weight.positive
   congr! with x
   simp
 
+variable (W) in
+theorem finrank_homogenize
+    (K : ConvexSet R A) [Module.Finite R (vectorSpan R (K : Set A))] :
+    (homogenize W K).finrank = Order.succ (affineSpan R (K : Set A)).finDim := by
+  by_cases hK : K = ∅
+  · simp [hK, ← SetLike.bot_eq_empty]
+  obtain ⟨t, -, ht₂, ht₃, ht₄⟩ := exists_affineIndepOn_of_finiteDimensional R V (K : Set A)
+  rw [← WithBot.succ_eq_succ, ← ht₄, ← finDim_affineSpan_eq_finrank, homogenize,
+    AffineSubspace.finDim_eq_finrank (PointedCone.affineSpan_ne_bot _),
+    affineSpan_hull, ← affineSpan_insert_zero',
+    affineSpan_insert_congr R 0 (t := hom.ofPoint '' t) (by simp [← AffineSubspace.map_span, ht₂])]
+  have ht : t.Finite := by
+    have : affineSpan R (K : Set A) ≠ ⊥ := by simpa
+    exact Set.finite_of_ncard_pos <| by
+      simp [AffineSubspace.finDim_eq_finrank this, ht₄, WithBot.succ_natCast]
+  have hai : AffineIndepOn R id (insert 0 (hom.ofPoint '' t)) := by
+    refine (ht₃.map' _ hom.ofPoint_injective).id_image.insert ?_
+    simp [← AffineSubspace.map_span, hom.ofPoint_ne_zero]
+  rw [direction_affineSpan, hai.finrank_vectorSpan (by simp [ht.image _]) (by simp),
+    Set.ncard_insert_of_notMem (by simp [hom.ofPoint_ne_zero]) (ht.image _),
+    Set.ncard_image_of_injective t hom.ofPoint_injective]
+  norm_cast
+
+variable (W) in
+theorem finDim_affineSpan_eq_pred_finrank_homogenize
+    (K : ConvexSet R A) [Module.Finite R (vectorSpan R (K : Set A))] :
+    (affineSpan R (K : Set A)).finDim = Order.pred ((homogenize W K).finrank : WithBot ℕ) := by
+  simp [finrank_homogenize]
+
 variable [ConvexSpace R W] [IsAffineConvexSpace R V A] [IsModuleConvexSpace R W]
 
 lemma smul_pos_of_mem_homogenize {P : ConvexSet R A} {x} (h : x ∈ homogenize W P) (hx : x ≠ 0) :

Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Defs.lean

@@ -22,6 +22,16 @@ variable {A : Type*} [AddTorsor V A]
 
 lemma spanPoints_empty : spanPoints R (∅ : Set A) = ∅ := by simp [spanPoints]
 
+theorem _root_.affineSpan_insert_congr {s t : Set A} (x : A)
+    (h : affineSpan R s = affineSpan R t) :
+    affineSpan R (insert x s) = affineSpan R (insert x t) := by
+  rw [← affineSpan_insert_affineSpan, h, affineSpan_insert_affineSpan]
+
+theorem _root_.vectorSpan_insert_congr {s t : Set A} (x : A)
+    (h : affineSpan R s = affineSpan R t) :
+    vectorSpan R (insert x s) = vectorSpan R (insert x t) := by
+  rw [← direction_affineSpan, affineSpan_insert_congr R x h, direction_affineSpan]
+
 @[gcongr]
 lemma spanPoints_mono {F G : Set A} (hFG : G ⊆ F) : spanPoints R G ⊆ spanPoints R F :=
   fun _p ⟨p₁, hp₁, v, hv, hp⟩ =>

Polyhedral/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean

@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2026 Vlad Tsyrklevich. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Vlad Tsyrklevich
+-/
+module
+
+public import Mathlib.LinearAlgebra.AffineSpace.Dimension
+public import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
+
+/-! Finite-dimensional affine space lemmas -/
+
+@[expose] public section
+
+open Affine
+
+section AffineSpace'
+
+variable (k : Type*) {V : Type*} {P : Type*}
+
+open AffineSubspace Module
+
+variable [DivisionRing k] [AddCommGroup V] [Module k V] [AffineSpace V P]
+
+variable {k}
+
+theorem AffineIndepOn.ncard_eq_succ_finDim_affineSpan {s : Set P} (hai : AffineIndepOn k id s)
+    [hf : FiniteDimensional k (vectorSpan k s)] : s.ncard = (affineSpan k s).finDim.succ := by
+  rcases Set.eq_empty_or_nonempty s with rfl | hs
+  · simp
+  rw [← Subtype.range_coe (s := s)] at hf
+  have := finiteDimensional_iff_setFinite k hai |>.mp hf
+  have := hai.finrank_vectorSpan this hs
+  rw [finDim_eq_finrank (by simp [Set.nonempty_iff_ne_empty.mp hs]), direction_affineSpan,
+    WithBot.succ_natCast, this]
+  grind only [Set.ncard_eq_zero, Set.not_nonempty_empty]
+
+theorem AffineIndependent.ncard_eq_succ_finDim_affineSpan {s : Set P}
+    (hai : AffineIndependent k ((↑) : s → P)) [hf : FiniteDimensional k (vectorSpan k s)] :
+    s.ncard = (affineSpan k s).finDim.succ :=
+  AffineIndepOn.ncard_eq_succ_finDim_affineSpan ((affineIndependent_subtype_iff _).mp hai)
+
+variable (k)
+
+variable (V) in
+theorem exists_affineIndependent_of_finiteDimensional (s : Set P)
+    [F : FiniteDimensional k (vectorSpan k s)] :
+    ∃ t ⊆ s, affineSpan k t = affineSpan k s ∧ AffineIndependent k ((↑) : t → P) ∧
+      t.ncard = (affineSpan k s).finDim.succ := by
+  obtain ⟨t, ht₁, ht₂, ht₃⟩ := exists_affineIndependent k V s
+  refine ⟨t, ht₁, ht₂, ht₃, ?_⟩
+  rw [← direction_affineSpan, ← ht₂, direction_affineSpan] at F
+  exact ht₂ ▸ ht₃.ncard_eq_succ_finDim_affineSpan
+
+variable (V) in
+theorem exists_affineIndepOn_of_finiteDimensional (s : Set P)
+    [F : FiniteDimensional k (vectorSpan k s)] :
+    ∃ t ⊆ s, affineSpan k t = affineSpan k s ∧ AffineIndepOn k id t ∧
+      t.ncard = (affineSpan k s).finDim.succ :=
+  exists_affineIndependent_of_finiteDimensional k V s
+
+end AffineSpace'

Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Independent.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2026 Vlad Tsyrklevich. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Vlad Tsyrklevich
+-/
+module
+
+public import Mathlib.LinearAlgebra.AffineSpace.Independent
+
+/-! Affine independence lemmas -/
+
+@[expose] public section
+
+open Affine
+
+section DivisionRing
+
+variable (k : Type*) (V : Type*) {P : Type*} [DivisionRing k] [AddCommGroup V] [Module k V]
+variable [AffineSpace V P]
+
+theorem exists_affineIndepOn (s : Set P) :
+    ∃ t ⊆ s, affineSpan k t = affineSpan k s ∧ AffineIndepOn k id t :=
+  exists_affineIndependent k V s
+
+end DivisionRing