feat(Analysis/Convex/SimplicialComplex): add AbstractSimplicialComplex + constructions

Mathlib.lean

@@ -1751,6 +1751,7 @@ public import Mathlib.Analysis.Convex.Quasiconvex
 public import Mathlib.Analysis.Convex.Radon
 public import Mathlib.Analysis.Convex.Segment
 public import Mathlib.Analysis.Convex.Side
+public import Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
 public import Mathlib.Analysis.Convex.SimplicialComplex.Basic
 public import Mathlib.Analysis.Convex.Slope
 public import Mathlib.Analysis.Convex.SpecificFunctions.Basic

Mathlib/AlgebraicTopology/SimplicialComplex/Basic.lean

@@ -0,0 +1,136 @@
+/-
+Copyright (c) 2025 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+module
+
+public import Mathlib.LinearAlgebra.AffineSpace.Independent
+
+/-!
+# Abstract Simplicial complexes
+
+In this file, we define abstract simplicial complexes.
+An abstract simplicial complex is a downwards-closed collection of nonempty finite sets containing
+every Singleton. These are defined first defining `PreAbstractSimplicialComplex`,
+which does not require the presence of singletons, and then defining `AbstractSimplicialComplex` as
+an extension.
+
+This is related to the geometrical notion of simplicial complexes, which are then defined under the
+name `Geometry.SimplicialComplex` using affine combinations in another file.
+
+## Main declarations
+
+* `PreAbstractSimplicialComplex ι`: An abstract simplicial complex with vertices of type `ι`.
+* `AbstractSimplicialComplex ι`: An abstract simplicial complex with vertices of type `ι` which
+  contains all singletons.
+
+## Notation
+
+`s ∈ K` means that `s` is a face of `K`.
+
+`K ≤ L` means that the faces of `K` are faces of `L`.
+
+-/
+
+@[expose] public section
+
+
+open Finset Set
+
+variable (ι : Type*)
+
+/-- An abstract simplicial complex is a collection of nonempty finite sets of points ("faces")
+which is downwards closed, i.e., any nonempty subset of a face is also a face.
+-/
+@[ext]
+structure PreAbstractSimplicialComplex where
+  /-- the faces of this simplicial complex: currently, given by their spanning vertices -/
+  faces : Set (Finset ι)
+  /-- the empty set is not a face: hence, all faces are non-empty -/
+  empty_notMem : ∅ ∉ faces
+  /-- faces are downward closed: a non-empty subset of its spanning vertices spans another face -/
+  down_closed : ∀ {s t}, s ∈ faces → t ⊆ s → t.Nonempty → t ∈ faces
+
+namespace PreAbstractSimplicialComplex
+
+/-- The complex consisting of only the faces present in both of its arguments. -/
+instance : Min (PreAbstractSimplicialComplex ι) :=
+  ⟨fun K L =>
+    { faces := K.faces ∩ L.faces
+      empty_notMem := fun h => K.empty_notMem (Set.inter_subset_left h)
+      down_closed := fun hs hst ht => ⟨K.down_closed hs.1 hst ht, L.down_closed hs.2 hst ht⟩ }⟩
+
+/-- The complex consisting of all faces present in either of its arguments. -/
+instance : Max (PreAbstractSimplicialComplex ι) :=
+  ⟨fun K L =>
+    { faces := K.faces ∪ L.faces
+      empty_notMem := by
+        simp only [Set.mem_union, not_or]
+        exact ⟨K.empty_notMem, L.empty_notMem⟩
+      down_closed := by
+        sorry }⟩
+
+instance : LE (PreAbstractSimplicialComplex ι) :=
+  ⟨fun K L => K.faces ⊆ L.faces⟩
+
+instance : LT (PreAbstractSimplicialComplex ι) :=
+  ⟨fun K L => K.faces ⊂ L.faces⟩
+
+instance : CompleteLattice (PreAbstractSimplicialComplex ι) where
+  le := (· ≤ ·)
+  lt := (· < ·)
+  le_refl := fun K => Set.Subset.refl K.faces
+  le_trans := fun _ _ _ h1 h2 => Set.Subset.trans h1 h2
+  le_antisymm := fun K L h1 h2 => PreAbstractSimplicialComplex.ext (Set.Subset.antisymm h1 h2)
+  sup := max
+  le_sup_left := fun K L => Set.subset_union_left
+  le_sup_right := fun K L => Set.subset_union_right
+  sup_le := fun K L M h1 h2 => Set.union_subset h1 h2
+  inf := min
+  inf_le_left := fun K L => Set.inter_subset_left
+  inf_le_right := fun K L => Set.inter_subset_right
+  le_inf := fun K L M h1 h2 => Set.subset_inter h1 h2
+  sSup := fun s =>
+    { faces := ⋃ K ∈ s, K.faces
+      empty_notMem := by
+        simp only [Set.mem_iUnion, not_exists]
+        exact fun K hK => K.empty_notMem
+      down_closed := by
+        sorry }
+  le_sSup := fun s K hK => sorry
+  sSup_le := fun s K hK => sorry
+  sInf := fun s =>
+    { faces := ⋂ K ∈ s, K.faces
+      empty_notMem := by
+        simp only [Set.mem_iInter, not_forall]
+        sorry
+      down_closed := by
+        sorry }
+  sInf_le := fun s K hK => sorry
+  le_sInf := fun s K hK => sorry
+  top :=
+    { faces := { s | False }
+      empty_notMem := by simp
+      down_closed := by
+        sorry }
+  le_top := fun K s hs => sorry
+  bot :=
+    { faces := { s | s.Nonempty }
+      empty_notMem := by simp
+      down_closed := by
+        sorry }
+  bot_le := fun K s hs => sorry
+
+
+end PreAbstractSimplicialComplex
+
+@[ext]
+structure AbstractSimplicialComplex extends PreAbstractSimplicialComplex ι where
+  /-- every singleton is a face -/
+  singleton_mem : ∀ v : ι, {v} ∈ faces
+
+-- TODO typeclasses for lattice
+-- TODO API to go from PreAbstractSimplicialComplex to AbstractSimplicialComplex and back
+
+end

Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean

@@ -0,0 +1,134 @@
+/-
+Copyright (c) 2025 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+module
+
+public import Mathlib.Analysis.Convex.Combination
+public import Mathlib.Analysis.Convex.SimplicialComplex.Basic
+public import Mathlib.LinearAlgebra.Finsupp.VectorSpace
+public import Mathlib.Combinatorics.SimpleGraph.Basic
+
+/-!
+# Simplicial complexes from affinely independent points
+
+This file provides constructions for simplicial complexes where the vertices
+are affinely independent.
+
+## Main declarations
+
+* `Geometry.SimplicialComplex.ofAffineIndependent`: Construct a simplicial complex from a
+  downward-closed set of faces whose union of vertices is affinely independent.
+* `Geometry.SimplicialComplex.onFinsupp`: Construct a simplicial complex on `ι →₀ 𝕜` from a
+  downward-closed set of finite subsets of `ι`, using the standard basis vectors.
+* `Geometry.SimplicialComplex.ofSimpleGraph`: Construct a simplicial complex from a simple graph,
+  where vertices of the graph are 0-simplices and edges are 1-simplices.
+-/
+
+@[expose] public section
+
+open Finset Set
+
+namespace Geometry
+
+namespace AbstractSimplicialComplex
+
+/--
+Construct an abstract simplicial complex from a simple graph, where vertices of the graph
+are 0-simplices and edges are 1-simplices.
+-/
+def ofSimpleGraph {ι : Type*} [DecidableEq ι] (G : SimpleGraph ι) :
+    AbstractSimplicialComplex ι where
+  faces := ((fun v => ({v} : Finset ι)) '' (Set.univ (α := ι))) ∪ Sym2.toFinset '' G.edgeSet
+  empty_notMem := by
+    simp only [Set.mem_union, Set.mem_image, Set.mem_univ, true_and, Finset.singleton_ne_empty,
+      exists_false, false_or, not_exists, not_and]
+    exact fun _ _ h => Finset.ne_empty_of_mem (Sym2.mem_toFinset.mpr (Sym2.out_fst_mem _)) h
+  down_closed := by
+    simp only [Set.mem_union, Set.mem_image, Set.mem_univ, true_and]
+    intro s t hs hts ht
+    rcases hs with ⟨v, rfl⟩ | ⟨e, he, rfl⟩
+    · simp only [Finset.subset_singleton_iff] at hts
+      rcases hts with rfl | rfl
+      · exact ht.ne_empty rfl |>.elim
+      · exact Or.inl ⟨v, rfl⟩
+    · by_cases hc : t.card ≤ 1
+      · left
+        obtain ⟨x, hx⟩ := ht
+        exact ⟨x, (Finset.eq_singleton_iff_unique_mem.mpr
+          ⟨hx, fun y hy => Finset.card_le_one.mp hc y hy x hx⟩).symm⟩
+      · right
+        push_neg at hc
+        have hle : e.toFinset.card ≤ t.card := by
+          have := Sym2.card_toFinset e
+          split_ifs at this <;> omega
+        exact ⟨e, he, (Finset.eq_of_subset_of_card_le hts hle).symm⟩
+
+end AbstractSimplicialComplex
+
+namespace SimplicialComplex
+
+/--
+Construct a simplicial complex from a downward-closed set of faces
+with defining points affinely independent.
+-/
+def ofAffineIndependent {𝕜 E}
+    [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [DecidableEq E] [AddCommGroup E] [Module 𝕜 E]
+    (faces : Set (Finset E)) (empty_notMem : ∅ ∉ faces)
+    (down_closed : ∀ {s t}, s ∈ faces → t ⊆ s → t.Nonempty → t ∈ faces)
+    (indep : AffineIndependent 𝕜 (Subtype.val : (⋃ s ∈ faces, (s : Set E)) → E)) :
+    SimplicialComplex 𝕜 E where
+  faces := faces
+  empty_notMem := empty_notMem
+  indep {s} hs := indep.mono (Set.subset_biUnion_of_mem hs)
+  down_closed := down_closed
+  inter_subset_convexHull {s t} hs ht := by
+    apply subset_of_eq
+    rw [AffineIndependent.convexHull_inter (R := 𝕜) (s := s ∪ t)]
+    · apply indep.mono
+      simp only [Finset.coe_union]
+      exact Set.union_subset (Set.subset_biUnion_of_mem hs) (Set.subset_biUnion_of_mem ht)
+    · exact Finset.subset_union_left
+    · exact Finset.subset_union_right
+
+/--
+Construct a simplicial complex from an abstract simplicial complex on a set of points
+over the `𝕜`-module of finitely supported functions on those points.
+-/
+noncomputable def onFinsupp {𝕜 ι : Type*} [DecidableEq ι]
+    [DecidableEq 𝕜] [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
+    (abstract : AbstractSimplicialComplex ι) :
+    SimplicialComplex 𝕜 (ι →₀ 𝕜) :=
+  ofAffineIndependent (𝕜 := 𝕜) (E := ι →₀ 𝕜)
+    (abstract.faces.image (fun x => x.image (fun i => Finsupp.single i (1 : 𝕜))))
+    (by
+      simp only [Set.mem_image, Finset.image_eq_empty]
+      rintro ⟨s, hs, rfl⟩
+      exact abstract.empty_notMem hs)
+    (by
+      simp only [Set.mem_image]
+      rintro _ t ⟨s', hs', rfl⟩ hts ht
+      rw [Finset.subset_image_iff] at hts
+      obtain ⟨t', ht', rfl⟩ := hts
+      exact ⟨t', abstract.down_closed hs' ht' (Finset.image_nonempty.mp ht), rfl⟩)
+    (by
+      refine (Finsupp.linearIndependent_single_one 𝕜 ι).affineIndependent.range.mono fun x hx => ?_
+      simp only [Set.mem_iUnion, Set.mem_image, Finset.mem_coe] at hx
+      obtain ⟨_, ⟨_, _, rfl⟩, hx⟩ := hx
+      exact Finset.mem_image.mp hx |>.choose_spec.2 ▸ Set.mem_range_self _)
+
+/--
+The simplicial complex associated to a simple graph, where vertices of the graph
+are 0-simplices and edges are 1-simplices. The complex is constructed over the
+`𝕜`-module of finitely supported functions on the vertex type.
+-/
+noncomputable def ofSimpleGraph {𝕜 V : Type*} [DecidableEq V] [DecidableEq 𝕜]
+    [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
+    (G : SimpleGraph V) :
+    SimplicialComplex 𝕜 (V →₀ 𝕜) :=
+  onFinsupp (AbstractSimplicialComplex.ofSimpleGraph G)
+
+end SimplicialComplex
+
+end Geometry

Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean

@@ -5,18 +5,19 @@ Authors: Yaël Dillies, Bhavik Mehta
 -/
 module
 
+public import Mathlib.AlgebraicTopology.SimplicialComplex.Basic
 public import Mathlib.Analysis.Convex.Hull
 public import Mathlib.LinearAlgebra.AffineSpace.Independent
 
 /-!
 # Simplicial complexes
 
-In this file, we define simplicial complexes in `𝕜`-modules. A simplicial complex is a collection
-of simplices closed by inclusion (of vertices) and intersection (of underlying sets).
-
-We model them by a downward-closed set of affine independent finite sets whose convex hulls "glue
-nicely", each finite set and its convex hull corresponding respectively to the vertices and the
-underlying set of a simplex.
+In this file, we define simplicial complexes over `𝕜`-modules.
+A (pre-) abstract simplicial complex is a downwards-closed collection of nonempty finite sets,
+and a simplicial complex is such a collection identified with simplices
+closed by inclusion (of vertices) and intersection (of underlying sets)
+whose convex hulls "glue nicely", each finite set and its convex hull corresponding respectively
+to the vertices and the underlying set of a simplex.
 
 ## Main declarations
 
@@ -57,15 +58,9 @@ Note that the textbook meaning of "glue nicely" is given in
 `Geometry.SimplicialComplex.disjoint_or_exists_inter_eq_convexHull`. It is mostly useless, as
 `Geometry.SimplicialComplex.convexHull_inter_convexHull` is enough for all purposes. -/
 @[ext]
-structure SimplicialComplex where
-  /-- the faces of this simplicial complex: currently, given by their spanning vertices -/
-  faces : Set (Finset E)
-  /-- the empty set is not a face: hence, all faces are non-empty -/
-  empty_notMem : ∅ ∉ faces
+structure SimplicialComplex extends PreAbstractSimplicialComplex E where
   /-- the vertices in each face are affine independent: this is an implementation detail -/
   indep : ∀ {s}, s ∈ faces → AffineIndependent 𝕜 ((↑) : s → E)
-  /-- faces are downward closed: a non-empty subset of its spanning vertices spans another face -/
-  down_closed : ∀ {s t}, s ∈ faces → t ⊆ s → t.Nonempty → t ∈ faces
   inter_subset_convexHull : ∀ {s t}, s ∈ faces → t ∈ faces →
     convexHull 𝕜 ↑s ∩ convexHull 𝕜 ↑t ⊆ convexHull 𝕜 (s ∩ t : Set E)
 
@@ -215,7 +210,7 @@ instance : Min (SimplicialComplex 𝕜 E) :=
       inter_subset_convexHull := fun hs ht => K.inter_subset_convexHull hs.1 ht.1 }⟩
 
 instance : SemilatticeInf (SimplicialComplex 𝕜 E) :=
-  { PartialOrder.lift faces (fun _ _ => SimplicialComplex.ext) with
+  { PartialOrder.lift (fun K => K.faces) (fun _ _ => SimplicialComplex.ext) with
     inf := (· ⊓ ·)
     inf_le_left := fun _ _ _ hs => hs.1
     inf_le_right := fun _ _ _ hs => hs.2

Mathlib/LinearAlgebra/AffineSpace/Independent.lean

@@ -237,6 +237,15 @@ theorem affineIndependent_iff_eq_of_fintype_affineCombination_eq [Fintype ι] (p
       Finset.affineCombination_indicator_subset w2 p (Finset.subset_univ s2)] at hweq
     exact h _ _ hw1' hw2' hweq
 
+/-- A linearly independent family of vectors is also affinely independent. -/
+theorem LinearIndependent.affineIndependent
+    {v : ι → V} (hv : LinearIndependent k v) : AffineIndependent k v := by
+  intro s w hw0 hwv i hi
+  rw [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ _ _ hw0 0,
+    Finset.weightedVSubOfPoint_apply] at hwv
+  simp only [vsub_eq_sub, sub_zero] at hwv
+  exact linearIndependent_iff'.mp hv s w hwv i hi
+
 variable {k}
 
 /-- If we single out one member of an affine-independent family of points and affinely transport