Skip to content

Commit

Permalink
Dimension calculation
Browse files Browse the repository at this point in the history
  • Loading branch information
YaelDillies committed Sep 27, 2024
1 parent 0e9327a commit 810c740
Show file tree
Hide file tree
Showing 8 changed files with 142 additions and 1 deletion.
6 changes: 6 additions & 0 deletions LeanCamCombi.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
14 changes: 14 additions & 0 deletions LeanCamCombi/Mathlib/Algebra/Group/Pointwise/Set.lean
Original file line number Diff line number Diff line change
@@ -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
23 changes: 23 additions & 0 deletions LeanCamCombi/Mathlib/Algebra/GroupWithZero/Pointwise/Set.lean
Original file line number Diff line number Diff line change
@@ -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
17 changes: 17 additions & 0 deletions LeanCamCombi/Mathlib/Data/Set/Card.lean
Original file line number Diff line number Diff line change
@@ -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
40 changes: 40 additions & 0 deletions LeanCamCombi/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean
Original file line number Diff line number Diff line change
@@ -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
10 changes: 10 additions & 0 deletions LeanCamCombi/Mathlib/LinearAlgebra/Dimension/Construction.lean
Original file line number Diff line number Diff line change
@@ -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
3 changes: 3 additions & 0 deletions LeanCamCombi/Mathlib/LinearAlgebra/Span.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
import Mathlib.LinearAlgebra.Span

attribute [gcongr] Submodule.span_mono
30 changes: 29 additions & 1 deletion LeanCamCombi/Sight/Sight.lean
Original file line number Diff line number Diff line change
@@ -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*}

Expand Down Expand Up @@ -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
Expand All @@ -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

0 comments on commit 810c740

Please sign in to comment.