From 810c740b2ab7337d11f579c8ed8dcc5a99c05875 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Fri, 27 Sep 2024 14:40:41 +0000
Subject: [PATCH] Dimension calculation

---
 LeanCamCombi.lean                             |  6 +++
 .../Mathlib/Algebra/Group/Pointwise/Set.lean  | 14 +++++++
 .../Algebra/GroupWithZero/Pointwise/Set.lean  | 23 +++++++++++
 LeanCamCombi/Mathlib/Data/Set/Card.lean       | 17 ++++++++
 .../AffineSpace/AffineSubspace.lean           | 40 +++++++++++++++++++
 .../LinearAlgebra/Dimension/Construction.lean | 10 +++++
 LeanCamCombi/Mathlib/LinearAlgebra/Span.lean  |  3 ++
 LeanCamCombi/Sight/Sight.lean                 | 30 +++++++++++++-
 8 files changed, 142 insertions(+), 1 deletion(-)
 create mode 100644 LeanCamCombi/Mathlib/Algebra/Group/Pointwise/Set.lean
 create mode 100644 LeanCamCombi/Mathlib/Algebra/GroupWithZero/Pointwise/Set.lean
 create mode 100644 LeanCamCombi/Mathlib/Data/Set/Card.lean
 create mode 100644 LeanCamCombi/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean
 create mode 100644 LeanCamCombi/Mathlib/LinearAlgebra/Dimension/Construction.lean
 create mode 100644 LeanCamCombi/Mathlib/LinearAlgebra/Span.lean

diff --git a/LeanCamCombi.lean b/LeanCamCombi.lean
index 2b95dbb015..3bef727f72 100644
--- a/LeanCamCombi.lean
+++ b/LeanCamCombi.lean
@@ -20,6 +20,8 @@ import LeanCamCombi.Kneser.MulStab
 import LeanCamCombi.LittlewoodOfford
 import LeanCamCombi.Mathlib.Algebra.BigOperators.Finsupp
 import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
+import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set
+import LeanCamCombi.Mathlib.Algebra.GroupWithZero.Pointwise.Set
 import LeanCamCombi.Mathlib.Algebra.Module.BigOperators
 import LeanCamCombi.Mathlib.Algebra.Order.BigOperators.LocallyFinite
 import LeanCamCombi.Mathlib.Algebra.Order.Group.Pi
@@ -44,10 +46,14 @@ import LeanCamCombi.Mathlib.Data.Finsupp.Order
 import LeanCamCombi.Mathlib.Data.List.DropRight
 import LeanCamCombi.Mathlib.Data.Multiset.Basic
 import LeanCamCombi.Mathlib.Data.Nat.Defs
+import LeanCamCombi.Mathlib.Data.Set.Card
 import LeanCamCombi.Mathlib.Data.Set.Finite
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
 import LeanCamCombi.Mathlib.GroupTheory.QuotientGroup
 import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.AffineMap
+import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace
+import LeanCamCombi.Mathlib.LinearAlgebra.Dimension.Construction
+import LeanCamCombi.Mathlib.LinearAlgebra.Span
 import LeanCamCombi.Mathlib.Logic.Basic
 import LeanCamCombi.Mathlib.Order.ConditionallyCompleteLattice.Basic
 import LeanCamCombi.Mathlib.Order.Partition.Finpartition
diff --git a/LeanCamCombi/Mathlib/Algebra/Group/Pointwise/Set.lean b/LeanCamCombi/Mathlib/Algebra/Group/Pointwise/Set.lean
new file mode 100644
index 0000000000..4ceb725437
--- /dev/null
+++ b/LeanCamCombi/Mathlib/Algebra/Group/Pointwise/Set.lean
@@ -0,0 +1,14 @@
+import Mathlib.Algebra.Group.Pointwise.Set
+
+open scoped Pointwise
+
+namespace Set
+variable {α β : Type*} [SMul α β]
+
+attribute [gcongr] smul_subset_smul vadd_subset_vadd smul_set_mono vadd_set_mono
+
+@[to_additive]
+lemma smul_set_insert (a : α) (b : β) (s : Set β) : a • insert b s = insert (a • b) (a • s) :=
+  image_insert_eq ..
+
+end Set
diff --git a/LeanCamCombi/Mathlib/Algebra/GroupWithZero/Pointwise/Set.lean b/LeanCamCombi/Mathlib/Algebra/GroupWithZero/Pointwise/Set.lean
new file mode 100644
index 0000000000..bf95d4d20f
--- /dev/null
+++ b/LeanCamCombi/Mathlib/Algebra/GroupWithZero/Pointwise/Set.lean
@@ -0,0 +1,23 @@
+import Mathlib.Algebra.Group.Pointwise.Finset.NatCard
+
+open scoped Cardinal Pointwise
+
+variable {G α G₀ M₀ : Type*}
+
+namespace Set
+section Group
+variable [Group G] [MulAction G α]
+
+@[to_additive (attr := simp)]
+lemma card_smul_set' (a : G) (s : Set α) : #↥(a • s) = #s :=
+  Cardinal.mk_image_eq_of_injOn _ _ (MulAction.injective a).injOn
+
+end Group
+
+section GroupWithZero
+variable [GroupWithZero G₀] [Zero M₀] [MulActionWithZero G₀ M₀] {a : G₀}
+
+lemma card_smul_set₀ (ha : a ≠ 0) (s : Set M₀) : Nat.card ↥(a • s) = Nat.card s :=
+  Nat.card_image_of_injective (MulAction.injective₀ ha) _
+
+end GroupWithZero
diff --git a/LeanCamCombi/Mathlib/Data/Set/Card.lean b/LeanCamCombi/Mathlib/Data/Set/Card.lean
new file mode 100644
index 0000000000..73b23deaa6
--- /dev/null
+++ b/LeanCamCombi/Mathlib/Data/Set/Card.lean
@@ -0,0 +1,17 @@
+import Mathlib.Data.Set.Card
+
+/-!
+# TODO
+
+Rename `Set.exists_subset_card_eq` to `Set.exists_subset_ncard_eq`
+-/
+
+open scoped Cardinal
+
+namespace Set
+variable {α : Type*} {s : Set α}
+
+lemma exists_subset_natCard_eq {c : Cardinal} (hc : c ≤ #s) : ∃ t ⊆ s, #t = c :=
+  Cardinal.le_mk_iff_exists_subset.mp hc
+
+end Set
diff --git a/LeanCamCombi/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean b/LeanCamCombi/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean
new file mode 100644
index 0000000000..d34a47b2e4
--- /dev/null
+++ b/LeanCamCombi/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean
@@ -0,0 +1,40 @@
+import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace
+import Mathlib.LinearAlgebra.AffineSpace.Combination
+import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
+
+/-!
+# TODO
+
+Kill `spanPoints`
+-/
+
+open Set
+
+variable {k V P : Type*} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P]
+
+namespace AffineSubspace
+variable {s : AffineSubspace k P} {x y z : P}
+
+lemma mem_of_collinear (h : Collinear k {x, y, z}) (hx : x ∈ s) (hz : z ∈ s) : y ∈ s := sorry
+
+end AffineSubspace
+
+-- TODO: Prove that `SameRay` implies `Collinear`
+
+@[simp] lemma affineSpan_insert_zero (s : Set V) :
+    (affineSpan k (insert 0 s) : Set V) = Submodule.span k s := by
+  refine subset_antisymm ?_ ?_
+  · rw [← Submodule.span_insert_zero]
+    exact affineSpan_subset_span
+  let W : Submodule k V :=
+    { carrier := affineSpan k (insert 0 s)
+      add_mem' := fun {x y} hx hy ↦ by
+        sorry
+      zero_mem' := subset_affineSpan _ _ <| mem_insert ..
+      smul_mem' := fun {a x} hx ↦ by
+        simp only [SetLike.mem_coe]
+        refine AffineSubspace.mem_of_collinear ?_ hx <| subset_affineSpan _ _ <| mem_insert ..
+        sorry
+         }
+  change Submodule.span k s ≤ W
+  exact Submodule.span_le.2 fun x hx ↦ subset_affineSpan _ _ <| subset_insert _ _ hx
diff --git a/LeanCamCombi/Mathlib/LinearAlgebra/Dimension/Construction.lean b/LeanCamCombi/Mathlib/LinearAlgebra/Dimension/Construction.lean
new file mode 100644
index 0000000000..30fee520c7
--- /dev/null
+++ b/LeanCamCombi/Mathlib/LinearAlgebra/Dimension/Construction.lean
@@ -0,0 +1,10 @@
+import Mathlib.LinearAlgebra.Dimension.Constructions
+
+namespace Submodule
+variable {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] {s t : Submodule R M}
+
+-- TODO: Generalise `finrank_mono`
+
+lemma rank_mono (hst : s ≤ t) : Module.rank R s ≤ Module.rank R t := rank_le_of_submodule _ _ hst
+
+end Submodule
diff --git a/LeanCamCombi/Mathlib/LinearAlgebra/Span.lean b/LeanCamCombi/Mathlib/LinearAlgebra/Span.lean
new file mode 100644
index 0000000000..7d822665c6
--- /dev/null
+++ b/LeanCamCombi/Mathlib/LinearAlgebra/Span.lean
@@ -0,0 +1,3 @@
+import Mathlib.LinearAlgebra.Span
+
+attribute [gcongr] Submodule.span_mono
diff --git a/LeanCamCombi/Sight/Sight.lean b/LeanCamCombi/Sight/Sight.lean
index 1d8a85076c..b16b1a85d2 100644
--- a/LeanCamCombi/Sight/Sight.lean
+++ b/LeanCamCombi/Sight/Sight.lean
@@ -1,10 +1,15 @@
 import Mathlib.Analysis.Convex.Between
 import Mathlib.Analysis.Convex.Topology
+import Mathlib.Data.Set.Card
 import Mathlib.Tactic.Module
+import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set
+import LeanCamCombi.Mathlib.Algebra.GroupWithZero.Pointwise.Set
 import LeanCamCombi.Mathlib.Analysis.Convex.Between
+import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace
+import LeanCamCombi.Mathlib.LinearAlgebra.Span
 
 open AffineMap Filter Finset Set
-open scoped Topology
+open scoped Cardinal Pointwise Topology
 
 variable {𝕜 V P : Type*}
 
@@ -127,6 +132,8 @@ lemma IsClosed.exists_wbtw_isInSight (hs : IsClosed s) (hy : y ∈ s) (x : V) :
   rw [lineMap_lineMap_right] at hε
   exact (csInf_le ht ⟨mul_nonneg hε₀ hδ₀.le, hε⟩).not_lt <| mul_lt_of_lt_one_left hδ₀ hε₁
 
+-- TODO: Once we have cone hulls, the RHS can be strengthened to
+-- `coneHull ℝ x {y ∈ s | IsInSight ℝ (convexHull ℝ s) x y}`
 lemma IsClosed.convexHull_subset_affineSpan_isInSight (hs : IsClosed (convexHull ℝ s))
     (hx : x ∉ convexHull ℝ s) :
     convexHull ℝ s ⊆ affineSpan ℝ ({x} ∪ {y ∈ s | IsInSight ℝ (convexHull ℝ s) x y}) := by
@@ -137,4 +144,25 @@ lemma IsClosed.convexHull_subset_affineSpan_isInSight (hs : IsClosed (convexHull
     (affineSpan_mono _ subset_union_right <| convexHull_subset_affineSpan _ <|
       hxz.mem_convexHull_isInSight hx hz) (ne_of_mem_of_not_mem hz hx).symm
 
+open Submodule in
+lemma rank_le_card_isInSight (hs : IsClosed (convexHull ℝ s)) (hx : x ∉ convexHull ℝ s) :
+    Module.rank ℝ (span ℝ (-x +ᵥ s)) ≤ #{y ∈ s | IsInSight ℝ (convexHull ℝ s) x y} := by
+  calc
+    Module.rank ℝ (span ℝ (-x +ᵥ s)) ≤
+      Module.rank ℝ (span ℝ
+        (-x +ᵥ affineSpan ℝ ({x} ∪ {y ∈ s | IsInSight ℝ (convexHull ℝ s) x y}) : Set V)) := by
+      push_cast
+      refine rank_le_of_submodule _ _ ?_
+      gcongr
+      exact (subset_convexHull ..).trans <| hs.convexHull_subset_affineSpan_isInSight hx
+    _ = Module.rank ℝ (span ℝ (-x +ᵥ {y ∈ s | IsInSight ℝ (convexHull ℝ s) x y})) := by
+      suffices h :
+        -x +ᵥ (affineSpan ℝ ({x} ∪ {y ∈ s | IsInSight ℝ (convexHull ℝ s) x y}) : Set V) =
+          span ℝ (-x +ᵥ {y ∈ s | IsInSight ℝ (convexHull ℝ s) x y}) by
+        rw [AffineSubspace.coe_pointwise_vadd, h, span_span]
+      simp [← AffineSubspace.coe_pointwise_vadd, AffineSubspace.pointwise_vadd_span,
+        vadd_set_insert, -coe_affineSpan]
+    _ ≤ #(-x +ᵥ {y ∈ s | IsInSight ℝ (convexHull ℝ s) x y}) := rank_span_le _
+    _ = #{y ∈ s | IsInSight ℝ (convexHull ℝ s) x y} := by simp
+
 end Real