From 10772299242d28704c1abe52cd5dcaea5b7c01bf Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sun, 28 Dec 2025 16:47:52 -0800
Subject: [PATCH 01/22] feat(Analysis/Convex/SimplicialComplex): add
 constructions when union is affinely independent

---
 .../Convex/SimplicialComplex/Basic.lean       | 88 ++++++++++++++++++-
 1 file changed, 84 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
index be5b1e6cf42b21..acbf16325daad4 100644
--- a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
+++ b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
@@ -5,8 +5,10 @@ Authors: Yaël Dillies, Bhavik Mehta
 -/
 module
 
+public import Mathlib.Analysis.Convex.Combination
 public import Mathlib.Analysis.Convex.Hull
 public import Mathlib.LinearAlgebra.AffineSpace.Independent
+import Mathlib.LinearAlgebra.Finsupp.VectorSpace
 
 /-!
 # Simplicial complexes
@@ -47,8 +49,6 @@ Simplicial complexes can be generalized to affine spaces once `ConvexHull` has b
 
 open Finset Set
 
-variable (𝕜 E : Type*) [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E]
-
 namespace Geometry
 
 -- TODO: update to new binder order? not sure what binder order is correct for `down_closed`.
@@ -57,7 +57,8 @@ 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
+structure SimplicialComplex (𝕜 E : Type*)
+    [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] 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 -/
@@ -74,7 +75,9 @@ namespace SimplicialComplex
 @[deprecated (since := "2025-05-23")]
 alias not_empty_mem := empty_notMem
 
-variable {𝕜 E}
+section
+
+variable {𝕜 E : Type*} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E]
 variable {K : SimplicialComplex 𝕜 E} {s t : Finset E} {x : E}
 
 /-- A `Finset` belongs to a `SimplicialComplex` if it's a face of it. -/
@@ -140,6 +143,9 @@ def ofSubcomplex (K : SimplicialComplex 𝕜 E) (faces : Set (Finset E)) (subset
     down_closed := fun hs hts _ => down_closed hs hts
     inter_subset_convexHull := fun hs ht => K.inter_subset_convexHull (subset hs) (subset ht) }
 
+
+
+
 /-! ### Vertices -/
 
 
@@ -247,6 +253,80 @@ theorem space_bot : (⊥ : SimplicialComplex 𝕜 E).space = ∅ :=
 theorem facets_bot : (⊥ : SimplicialComplex 𝕜 E).facets = ∅ :=
   eq_empty_of_subset_empty facets_subset
 
+end
+
+section AffineIndependent
+
+open Classical in
+/-- Construct a simplicial complex from a downward-closed set of faces whose union is affinely
+independent. This is a common way to construct simplicial complexes: if you have a set of
+vertices that is affinely independent, then any downward-closed family of nonempty subsets
+forms a simplicial complex. -/
+def ofAffineIndependent {𝕜 E}
+    [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [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
+
+open Classical in
+/--
+Construct a simplicial complex from a downward-closed set of points
+over the `𝕜`-module of finitely supported functions on those points.
+-/
+def onFinsupp {𝕜 ι : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
+    (faces : Set (Finset ι))
+    (empty_notMem : ∅ ∉ faces)
+    (down_closed : ∀ {s t}, s ∈ faces → t ⊆ s → t.Nonempty → t ∈ faces) :
+    SimplicialComplex 𝕜 (ι →₀ 𝕜) :=
+  ofAffineIndependent (𝕜 := 𝕜) (E := ι →₀ 𝕜)
+    (faces.image (fun x => x.image (fun i => Finsupp.single i (1 : 𝕜))))
+    (empty_notMem := by
+      simp only [Set.mem_image, Finset.image_eq_empty]
+      rintro ⟨s, hs, rfl⟩
+      exact empty_notMem hs)
+    (down_closed := by
+      intro s t hs hts ht
+      simp only [Set.mem_image] at hs ⊢
+      obtain ⟨s', hs', rfl⟩ := hs
+      have hinj : Function.Injective (fun i : ι => Finsupp.single i (1 : 𝕜)) :=
+        Finsupp.single_left_injective one_ne_zero
+      rw [Finset.subset_image_iff] at hts
+      obtain ⟨t', ht', rfl⟩ := hts
+      refine ⟨t', down_closed hs' ht' (Finset.image_nonempty.mp ht), rfl⟩)
+    (indep := by
+      have hunion : ⋃ s ∈ (fun x => Finset.image (fun i => Finsupp.single i (1 : 𝕜)) x) '' faces,
+          (s : Set (ι →₀ 𝕜)) ⊆ Set.range (fun i : ι => Finsupp.single i (1 : 𝕜)) := by
+        intro x hx
+        simp only [Set.mem_iUnion, Set.mem_image, Finset.mem_coe] at hx
+        obtain ⟨s, ⟨t, ht, rfl⟩, hx⟩ := hx
+        obtain ⟨i, hi, rfl⟩ := Finset.mem_image.mp hx
+        exact Set.mem_range_self i
+      apply AffineIndependent.mono _ hunion
+      have hind : AffineIndependent 𝕜 (fun i : ι => Finsupp.single i (1 : 𝕜)) := 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
+        have hli := Finsupp.linearIndependent_single_one 𝕜 ι
+        rw [linearIndependent_iff'] at hli
+        exact hli s w hwv i hi
+      exact hind.range)
+
+end AffineIndependent
+
 end SimplicialComplex
 
 end Geometry

From 4fdbb5b74bb80b5e80fe8c073143bafd813053e1 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sun, 28 Dec 2025 16:50:00 -0800
Subject: [PATCH 02/22] public import

---
 Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
index acbf16325daad4..d15d699abab373 100644
--- a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
+++ b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
@@ -8,7 +8,7 @@ module
 public import Mathlib.Analysis.Convex.Combination
 public import Mathlib.Analysis.Convex.Hull
 public import Mathlib.LinearAlgebra.AffineSpace.Independent
-import Mathlib.LinearAlgebra.Finsupp.VectorSpace
+public import Mathlib.LinearAlgebra.Finsupp.VectorSpace
 
 /-!
 # Simplicial complexes

From bdfe400dba509083faf8ff4a55fcfd6e0986965d Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sun, 28 Dec 2025 16:51:48 -0800
Subject: [PATCH 03/22] remove extraneous LLM generation

---
 .../Analysis/Convex/SimplicialComplex/Basic.lean   | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
index d15d699abab373..18cc41e087fbea 100644
--- a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
+++ b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
@@ -258,10 +258,10 @@ end
 section AffineIndependent
 
 open Classical in
-/-- Construct a simplicial complex from a downward-closed set of faces whose union is affinely
-independent. This is a common way to construct simplicial complexes: if you have a set of
-vertices that is affinely independent, then any downward-closed family of nonempty subsets
-forms a simplicial complex. -/
+/--
+Construct a simplicial complex from a downward-closed set of faces
+with defining points affinely independent.
+-/
 def ofAffineIndependent {𝕜 E}
     [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E]
     (faces : Set (Finset E)) (empty_notMem : ∅ ∉ faces)
@@ -293,11 +293,11 @@ def onFinsupp {𝕜 ι : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrdered
     SimplicialComplex 𝕜 (ι →₀ 𝕜) :=
   ofAffineIndependent (𝕜 := 𝕜) (E := ι →₀ 𝕜)
     (faces.image (fun x => x.image (fun i => Finsupp.single i (1 : 𝕜))))
-    (empty_notMem := by
+    (by
       simp only [Set.mem_image, Finset.image_eq_empty]
       rintro ⟨s, hs, rfl⟩
       exact empty_notMem hs)
-    (down_closed := by
+    (by
       intro s t hs hts ht
       simp only [Set.mem_image] at hs ⊢
       obtain ⟨s', hs', rfl⟩ := hs
@@ -306,7 +306,7 @@ def onFinsupp {𝕜 ι : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrdered
       rw [Finset.subset_image_iff] at hts
       obtain ⟨t', ht', rfl⟩ := hts
       refine ⟨t', down_closed hs' ht' (Finset.image_nonempty.mp ht), rfl⟩)
-    (indep := by
+    (by
       have hunion : ⋃ s ∈ (fun x => Finset.image (fun i => Finsupp.single i (1 : 𝕜)) x) '' faces,
           (s : Set (ι →₀ 𝕜)) ⊆ Set.range (fun i : ι => Finsupp.single i (1 : 𝕜)) := by
         intro x hx

From 007d58074b99a26bae9262320039fe8bccb46352 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sun, 28 Dec 2025 16:54:46 -0800
Subject: [PATCH 04/22] golf proof

---
 .../Convex/SimplicialComplex/Basic.lean       | 28 ++++++-------------
 1 file changed, 9 insertions(+), 19 deletions(-)

diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
index 18cc41e087fbea..a99586b75802ce 100644
--- a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
+++ b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
@@ -298,32 +298,22 @@ def onFinsupp {𝕜 ι : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrdered
       rintro ⟨s, hs, rfl⟩
       exact empty_notMem hs)
     (by
-      intro s t hs hts ht
-      simp only [Set.mem_image] at hs ⊢
-      obtain ⟨s', hs', rfl⟩ := hs
-      have hinj : Function.Injective (fun i : ι => Finsupp.single i (1 : 𝕜)) :=
-        Finsupp.single_left_injective one_ne_zero
+      simp only [Set.mem_image]
+      rintro _ t ⟨s', hs', rfl⟩ hts ht
       rw [Finset.subset_image_iff] at hts
       obtain ⟨t', ht', rfl⟩ := hts
-      refine ⟨t', down_closed hs' ht' (Finset.image_nonempty.mp ht), rfl⟩)
+      exact ⟨t', down_closed hs' ht' (Finset.image_nonempty.mp ht), rfl⟩)
     (by
-      have hunion : ⋃ s ∈ (fun x => Finset.image (fun i => Finsupp.single i (1 : 𝕜)) x) '' faces,
-          (s : Set (ι →₀ 𝕜)) ⊆ Set.range (fun i : ι => Finsupp.single i (1 : 𝕜)) := by
-        intro x hx
-        simp only [Set.mem_iUnion, Set.mem_image, Finset.mem_coe] at hx
-        obtain ⟨s, ⟨t, ht, rfl⟩, hx⟩ := hx
-        obtain ⟨i, hi, rfl⟩ := Finset.mem_image.mp hx
-        exact Set.mem_range_self i
-      apply AffineIndependent.mono _ hunion
       have hind : AffineIndependent 𝕜 (fun i : ι => Finsupp.single i (1 : 𝕜)) := by
         intro s w hw0 hwv i hi
         rw [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ _ _ hw0 0,
-            Finset.weightedVSubOfPoint_apply] at hwv
+          Finset.weightedVSubOfPoint_apply] at hwv
         simp only [vsub_eq_sub, sub_zero] at hwv
-        have hli := Finsupp.linearIndependent_single_one 𝕜 ι
-        rw [linearIndependent_iff'] at hli
-        exact hli s w hwv i hi
-      exact hind.range)
+        exact (linearIndependent_iff'.mp (Finsupp.linearIndependent_single_one 𝕜 ι)) s w hwv i hi
+      refine hind.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 _)
 
 end AffineIndependent
 

From 8fbe2694eadd19f7c9b4543076abb60ed82fe919 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sun, 28 Dec 2025 16:59:02 -0800
Subject: [PATCH 05/22] refactor to new file

---
 .../AffineIndependentUnion.lean               | 94 +++++++++++++++++++
 .../Convex/SimplicialComplex/Basic.lean       | 64 -------------
 2 files changed, 94 insertions(+), 64 deletions(-)
 create mode 100644 Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean

diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean b/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
new file mode 100644
index 00000000000000..d8eba5760dd7f1
--- /dev/null
+++ b/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
@@ -0,0 +1,94 @@
+/-
+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
+
+/-!
+# 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.
+-/
+
+@[expose] public section
+
+open Finset Set
+
+namespace Geometry
+
+namespace SimplicialComplex
+
+open Classical in
+/--
+Construct a simplicial complex from a downward-closed set of faces
+with defining points affinely independent.
+-/
+def ofAffineIndependent {𝕜 E}
+    [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [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
+
+open Classical in
+/--
+Construct a simplicial complex from a downward-closed set of points
+over the `𝕜`-module of finitely supported functions on those points.
+-/
+def onFinsupp {𝕜 ι : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
+    (faces : Set (Finset ι))
+    (empty_notMem : ∅ ∉ faces)
+    (down_closed : ∀ {s t}, s ∈ faces → t ⊆ s → t.Nonempty → t ∈ faces) :
+    SimplicialComplex 𝕜 (ι →₀ 𝕜) :=
+  ofAffineIndependent (𝕜 := 𝕜) (E := ι →₀ 𝕜)
+    (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 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', down_closed hs' ht' (Finset.image_nonempty.mp ht), rfl⟩)
+    (by
+      have hind : AffineIndependent 𝕜 (fun i : ι => Finsupp.single i (1 : 𝕜)) := 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 (Finsupp.linearIndependent_single_one 𝕜 ι)) s w hwv i hi
+      refine hind.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 _)
+
+end SimplicialComplex
+
+end Geometry
diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
index a99586b75802ce..0db3c84176e37a 100644
--- a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
+++ b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
@@ -5,10 +5,8 @@ Authors: Yaël Dillies, Bhavik Mehta
 -/
 module
 
-public import Mathlib.Analysis.Convex.Combination
 public import Mathlib.Analysis.Convex.Hull
 public import Mathlib.LinearAlgebra.AffineSpace.Independent
-public import Mathlib.LinearAlgebra.Finsupp.VectorSpace
 
 /-!
 # Simplicial complexes
@@ -255,68 +253,6 @@ theorem facets_bot : (⊥ : SimplicialComplex 𝕜 E).facets = ∅ :=
 
 end
 
-section AffineIndependent
-
-open Classical in
-/--
-Construct a simplicial complex from a downward-closed set of faces
-with defining points affinely independent.
--/
-def ofAffineIndependent {𝕜 E}
-    [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [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
-
-open Classical in
-/--
-Construct a simplicial complex from a downward-closed set of points
-over the `𝕜`-module of finitely supported functions on those points.
--/
-def onFinsupp {𝕜 ι : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
-    (faces : Set (Finset ι))
-    (empty_notMem : ∅ ∉ faces)
-    (down_closed : ∀ {s t}, s ∈ faces → t ⊆ s → t.Nonempty → t ∈ faces) :
-    SimplicialComplex 𝕜 (ι →₀ 𝕜) :=
-  ofAffineIndependent (𝕜 := 𝕜) (E := ι →₀ 𝕜)
-    (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 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', down_closed hs' ht' (Finset.image_nonempty.mp ht), rfl⟩)
-    (by
-      have hind : AffineIndependent 𝕜 (fun i : ι => Finsupp.single i (1 : 𝕜)) := 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 (Finsupp.linearIndependent_single_one 𝕜 ι)) s w hwv i hi
-      refine hind.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 _)
-
-end AffineIndependent
-
 end SimplicialComplex
 
 end Geometry

From 9520eb318509f7a34e7a47aec87a3de34a83d069 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sun, 28 Dec 2025 17:00:45 -0800
Subject: [PATCH 06/22] revert other file

---
 .../Analysis/Convex/SimplicialComplex/Basic.lean   | 14 ++++----------
 1 file changed, 4 insertions(+), 10 deletions(-)

diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
index 0db3c84176e37a..be5b1e6cf42b21 100644
--- a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
+++ b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
@@ -47,6 +47,8 @@ Simplicial complexes can be generalized to affine spaces once `ConvexHull` has b
 
 open Finset Set
 
+variable (𝕜 E : Type*) [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E]
+
 namespace Geometry
 
 -- TODO: update to new binder order? not sure what binder order is correct for `down_closed`.
@@ -55,8 +57,7 @@ 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 (𝕜 E : Type*)
-    [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] where
+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 -/
@@ -73,9 +74,7 @@ namespace SimplicialComplex
 @[deprecated (since := "2025-05-23")]
 alias not_empty_mem := empty_notMem
 
-section
-
-variable {𝕜 E : Type*} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E]
+variable {𝕜 E}
 variable {K : SimplicialComplex 𝕜 E} {s t : Finset E} {x : E}
 
 /-- A `Finset` belongs to a `SimplicialComplex` if it's a face of it. -/
@@ -141,9 +140,6 @@ def ofSubcomplex (K : SimplicialComplex 𝕜 E) (faces : Set (Finset E)) (subset
     down_closed := fun hs hts _ => down_closed hs hts
     inter_subset_convexHull := fun hs ht => K.inter_subset_convexHull (subset hs) (subset ht) }
 
-
-
-
 /-! ### Vertices -/
 
 
@@ -251,8 +247,6 @@ theorem space_bot : (⊥ : SimplicialComplex 𝕜 E).space = ∅ :=
 theorem facets_bot : (⊥ : SimplicialComplex 𝕜 E).facets = ∅ :=
   eq_empty_of_subset_empty facets_subset
 
-end
-
 end SimplicialComplex
 
 end Geometry

From 27a08c53e941fc1cd930228f98319bfe63180295 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sun, 28 Dec 2025 17:01:25 -0800
Subject: [PATCH 07/22] mk_all

---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 120eeb50f23185..14976001c0703f 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1748,6 +1748,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

From 7ab5e4a2d0d2c5dc9d1c1ba34e38352ba1869c91 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sun, 28 Dec 2025 17:14:46 -0800
Subject: [PATCH 08/22] refactor

---
 .../AffineIndependentUnion.lean                 | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean b/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
index d8eba5760dd7f1..771ebc93d9608e 100644
--- a/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
+++ b/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
@@ -27,6 +27,17 @@ are affinely independent.
 
 open Finset Set
 
+-- TODO find home
+open Classical in
+theorem AffineIndependent.Finsupp {𝕜 ι : Type*} [inst : Ring 𝕜] :
+    AffineIndependent 𝕜 (V := ι →₀ 𝕜) (P := ι →₀ 𝕜) fun i ↦ Finsupp.single i 1 := 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 (Finsupp.linearIndependent_single_one 𝕜 ι)) s w hwv i hi
+
+
 namespace Geometry
 
 namespace SimplicialComplex
@@ -79,11 +90,7 @@ def onFinsupp {𝕜 ι : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrdered
       exact ⟨t', down_closed hs' ht' (Finset.image_nonempty.mp ht), rfl⟩)
     (by
       have hind : AffineIndependent 𝕜 (fun i : ι => Finsupp.single i (1 : 𝕜)) := 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 (Finsupp.linearIndependent_single_one 𝕜 ι)) s w hwv i hi
+        exact AffineIndependent.Finsupp
       refine hind.range.mono fun x hx => ?_
       simp only [Set.mem_iUnion, Set.mem_image, Finset.mem_coe] at hx
       obtain ⟨_, ⟨_, _, rfl⟩, hx⟩ := hx

From 3d46ab03ad3d232b528e0611aad67e895e285f2c Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sun, 28 Dec 2025 17:15:39 -0800
Subject: [PATCH 09/22] golf

---
 .../Convex/SimplicialComplex/AffineIndependentUnion.lean      | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean b/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
index 771ebc93d9608e..eed6ebe46d4854 100644
--- a/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
+++ b/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
@@ -89,9 +89,7 @@ def onFinsupp {𝕜 ι : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrdered
       obtain ⟨t', ht', rfl⟩ := hts
       exact ⟨t', down_closed hs' ht' (Finset.image_nonempty.mp ht), rfl⟩)
     (by
-      have hind : AffineIndependent 𝕜 (fun i : ι => Finsupp.single i (1 : 𝕜)) := by
-        exact AffineIndependent.Finsupp
-      refine hind.range.mono fun x hx => ?_
+      refine AffineIndependent.Finsupp.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 _)

From 661d0af03a003675164f911eaaaa1cdf4dcffaf0 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sun, 28 Dec 2025 17:40:49 -0800
Subject: [PATCH 10/22] rehome

---
 .../SimplicialComplex/AffineIndependentUnion.lean   | 13 +------------
 Mathlib/LinearAlgebra/AffineSpace/Independent.lean  | 10 ++++++++++
 2 files changed, 11 insertions(+), 12 deletions(-)

diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean b/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
index eed6ebe46d4854..c6b6f4ad1cf370 100644
--- a/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
+++ b/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
@@ -27,17 +27,6 @@ are affinely independent.
 
 open Finset Set
 
--- TODO find home
-open Classical in
-theorem AffineIndependent.Finsupp {𝕜 ι : Type*} [inst : Ring 𝕜] :
-    AffineIndependent 𝕜 (V := ι →₀ 𝕜) (P := ι →₀ 𝕜) fun i ↦ Finsupp.single i 1 := 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 (Finsupp.linearIndependent_single_one 𝕜 ι)) s w hwv i hi
-
-
 namespace Geometry
 
 namespace SimplicialComplex
@@ -89,7 +78,7 @@ def onFinsupp {𝕜 ι : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrdered
       obtain ⟨t', ht', rfl⟩ := hts
       exact ⟨t', down_closed hs' ht' (Finset.image_nonempty.mp ht), rfl⟩)
     (by
-      refine AffineIndependent.Finsupp.range.mono fun x hx => ?_
+      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 _)
diff --git a/Mathlib/LinearAlgebra/AffineSpace/Independent.lean b/Mathlib/LinearAlgebra/AffineSpace/Independent.lean
index a6ae3e85e0d626..bc75bbdb6bedf2 100644
--- a/Mathlib/LinearAlgebra/AffineSpace/Independent.lean
+++ b/Mathlib/LinearAlgebra/AffineSpace/Independent.lean
@@ -237,6 +237,16 @@ 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 affinely independent when viewed as points
+in the vector space (as an affine space over itself). -/
+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

From bad86879579e6a172028a35830be18061278e2a1 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sun, 28 Dec 2025 17:41:47 -0800
Subject: [PATCH 11/22] deslop

---
 Mathlib/LinearAlgebra/AffineSpace/Independent.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/LinearAlgebra/AffineSpace/Independent.lean b/Mathlib/LinearAlgebra/AffineSpace/Independent.lean
index bc75bbdb6bedf2..d6a671d22ed395 100644
--- a/Mathlib/LinearAlgebra/AffineSpace/Independent.lean
+++ b/Mathlib/LinearAlgebra/AffineSpace/Independent.lean
@@ -237,8 +237,7 @@ 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 affinely independent when viewed as points
-in the vector space (as an affine space over itself). -/
+/-- 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

From 9bf509442736b6d0223a01092e51db308082cb53 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sun, 28 Dec 2025 17:46:20 -0800
Subject: [PATCH 12/22] replace classical with decidableeq

---
 .../Convex/SimplicialComplex/AffineIndependentUnion.lean   | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean b/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
index c6b6f4ad1cf370..d7b3c7c96f2ea2 100644
--- a/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
+++ b/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
@@ -31,13 +31,12 @@ namespace Geometry
 
 namespace SimplicialComplex
 
-open Classical in
 /--
 Construct a simplicial complex from a downward-closed set of faces
 with defining points affinely independent.
 -/
 def ofAffineIndependent {𝕜 E}
-    [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 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)) :
@@ -55,12 +54,12 @@ def ofAffineIndependent {𝕜 E}
     · exact Finset.subset_union_left
     · exact Finset.subset_union_right
 
-open Classical in
 /--
 Construct a simplicial complex from a downward-closed set of points
 over the `𝕜`-module of finitely supported functions on those points.
 -/
-def onFinsupp {𝕜 ι : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
+noncomputable def onFinsupp {𝕜 ι : Type*} [DecidableEq ι]
+    [DecidableEq 𝕜] [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
     (faces : Set (Finset ι))
     (empty_notMem : ∅ ∉ faces)
     (down_closed : ∀ {s t}, s ∈ faces → t ⊆ s → t.Nonempty → t ∈ faces) :

From 6fb6ddfa3d7c2b31e93a8e71e8c0c2782e2106d1 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Mon, 29 Dec 2025 15:12:26 -0800
Subject: [PATCH 13/22] add SimpleGraph complex

---
 .../AffineIndependentUnion.lean               | 36 +++++++++++++++++++
 1 file changed, 36 insertions(+)

diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean b/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
index d7b3c7c96f2ea2..63aadea0965b33 100644
--- a/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
+++ b/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
@@ -8,6 +8,7 @@ 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
@@ -82,6 +83,41 @@ noncomputable def onFinsupp {𝕜 ι : Type*} [DecidableEq ι]
       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
+    (faces := ((fun v => ({v} : Finset V)) '' (Set.univ (α := V))) ∪ 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 SimplicialComplex
 
 end Geometry

From 237d9205f70e370eaddaa79bb6ad4fb76f308138 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Mon, 29 Dec 2025 15:46:31 -0800
Subject: [PATCH 14/22] introduce definition of abstract simplical complex

---
 .../AffineIndependentUnion.lean               | 73 +++++++++++--------
 .../Convex/SimplicialComplex/Basic.lean       | 57 ++++++++++++---
 2 files changed, 86 insertions(+), 44 deletions(-)

diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean b/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
index 63aadea0965b33..1c0e2bb291ed95 100644
--- a/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
+++ b/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
@@ -30,6 +30,41 @@ 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
 
 /--
@@ -56,27 +91,25 @@ def ofAffineIndependent {𝕜 E}
     · exact Finset.subset_union_right
 
 /--
-Construct a simplicial complex from a downward-closed set of points
+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 𝕜]
-    (faces : Set (Finset ι))
-    (empty_notMem : ∅ ∉ faces)
-    (down_closed : ∀ {s t}, s ∈ faces → t ⊆ s → t.Nonempty → t ∈ faces) :
+    (abstract : AbstractSimplicialComplex ι) :
     SimplicialComplex 𝕜 (ι →₀ 𝕜) :=
   ofAffineIndependent (𝕜 := 𝕜) (E := ι →₀ 𝕜)
-    (faces.image (fun x => x.image (fun i => Finsupp.single i (1 : 𝕜))))
+    (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 empty_notMem hs)
+      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', down_closed hs' ht' (Finset.image_nonempty.mp ht), rfl⟩)
+      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
@@ -92,31 +125,7 @@ noncomputable def ofSimpleGraph {𝕜 V : Type*} [DecidableEq V] [DecidableEq 
     [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
     (G : SimpleGraph V) :
     SimplicialComplex 𝕜 (V →₀ 𝕜) :=
-  onFinsupp
-    (faces := ((fun v => ({v} : Finset V)) '' (Set.univ (α := V))) ∪ 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⟩)
+  onFinsupp (AbstractSimplicialComplex.ofSimpleGraph G)
 
 end SimplicialComplex
 
diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
index be5b1e6cf42b21..9ecf0f4613dd24 100644
--- a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
+++ b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
@@ -47,7 +47,41 @@ Simplicial complexes can be generalized to affine spaces once `ConvexHull` has b
 
 open Finset Set
 
-variable (𝕜 E : Type*) [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E]
+section Abstract
+
+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 AbstractSimplicialComplex 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 AbstractSimplicialComplex
+
+/-- The complex consisting of only the faces present in both of its arguments. -/
+instance : Min (AbstractSimplicialComplex ι) :=
+  ⟨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⟩ }⟩
+
+instance : SemilatticeInf (AbstractSimplicialComplex ι) :=
+  { PartialOrder.lift faces (fun _ _ => AbstractSimplicialComplex.ext) with
+    inf := (· ⊓ ·)
+    inf_le_left := fun _ _ _ hs => hs.1
+    inf_le_right := fun _ _ _ hs => hs.2
+    le_inf := fun _ _ _ hKL hKM _ hs => ⟨hKL hs, hKM hs⟩ }
+
+end AbstractSimplicialComplex
+
+end Abstract
 
 namespace Geometry
 
@@ -57,26 +91,25 @@ 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 (𝕜 E : Type*) [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E]
+    extends AbstractSimplicialComplex 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)
 
-namespace SimplicialComplex
+variable (𝕜 E : Type*) [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E]
 
-@[deprecated (since := "2025-05-23")]
-alias not_empty_mem := empty_notMem
+namespace SimplicialComplex
 
 variable {𝕜 E}
 variable {K : SimplicialComplex 𝕜 E} {s t : Finset E} {x : E}
 
+def toAbstract (K : SimplicialComplex 𝕜 E) : AbstractSimplicialComplex E :=
+  { faces := K.faces
+    empty_notMem := K.empty_notMem
+    down_closed := K.down_closed }
+
 /-- A `Finset` belongs to a `SimplicialComplex` if it's a face of it. -/
 instance : Membership (Finset E) (SimplicialComplex 𝕜 E) :=
   ⟨fun K s => s ∈ K.faces⟩
@@ -218,7 +251,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

From dec25aa774c94225c72cb1f6992bd5b6ce7f85e0 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Mon, 29 Dec 2025 23:33:13 -0800
Subject: [PATCH 15/22] update docs

---
 .../SimplicialComplex/AffineIndependentUnion.lean   |  2 ++
 .../Analysis/Convex/SimplicialComplex/Basic.lean    | 13 +++++++------
 2 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean b/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
index 1c0e2bb291ed95..276886022bd283 100644
--- a/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
+++ b/Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
@@ -22,6 +22,8 @@ are affinely independent.
   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
diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
index 9ecf0f4613dd24..3c3ba4616ecef1 100644
--- a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
+++ b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
@@ -11,15 +11,16 @@ 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, both abstractly and in `𝕜`-modules.
+An abstract simplicial complex is a downwards-closed collection of nonempty finte 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
 
+* `AbstractSimplicialComplex ι`: An abstract simplicial complex with vertices of type `ι`.
 * `SimplicialComplex 𝕜 E`: A simplicial complex in the `𝕜`-module `E`.
 * `SimplicialComplex.vertices`: The zero-dimensional faces of a simplicial complex.
 * `SimplicialComplex.facets`: The maximal faces of a simplicial complex.

From 763a321655ee18e7b5c6ba77603a966877469182 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Tue, 30 Dec 2025 09:50:48 -0800
Subject: [PATCH 16/22] document toAbstract

---
 Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
index 3c3ba4616ecef1..cd4aac5f6f3b2b 100644
--- a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
+++ b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
@@ -106,6 +106,9 @@ namespace SimplicialComplex
 variable {𝕜 E}
 variable {K : SimplicialComplex 𝕜 E} {s t : Finset E} {x : E}
 
+/--
+Forget the geometric structure of a simplicial complex, yielding an abstract simplicial complex.
+-/
 def toAbstract (K : SimplicialComplex 𝕜 E) : AbstractSimplicialComplex E :=
   { faces := K.faces
     empty_notMem := K.empty_notMem

From 1ef350696a05abc0220bf9e9e2db7592a5ee8871 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Tue, 30 Dec 2025 10:19:50 -0800
Subject: [PATCH 17/22] remove unneeded to

---
 Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean | 8 --------
 1 file changed, 8 deletions(-)

diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
index cd4aac5f6f3b2b..75f10b43c60887 100644
--- a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
+++ b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
@@ -106,14 +106,6 @@ namespace SimplicialComplex
 variable {𝕜 E}
 variable {K : SimplicialComplex 𝕜 E} {s t : Finset E} {x : E}
 
-/--
-Forget the geometric structure of a simplicial complex, yielding an abstract simplicial complex.
--/
-def toAbstract (K : SimplicialComplex 𝕜 E) : AbstractSimplicialComplex E :=
-  { faces := K.faces
-    empty_notMem := K.empty_notMem
-    down_closed := K.down_closed }
-
 /-- A `Finset` belongs to a `SimplicialComplex` if it's a face of it. -/
 instance : Membership (Finset E) (SimplicialComplex 𝕜 E) :=
   ⟨fun K s => s ∈ K.faces⟩

From 26005028120f9368ecebc9bff4464271d1148138 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Tue, 30 Dec 2025 10:29:12 -0800
Subject: [PATCH 18/22] restore variable use

---
 Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
index 75f10b43c60887..6d6d8009ef8d08 100644
--- a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
+++ b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
@@ -84,6 +84,8 @@ end AbstractSimplicialComplex
 
 end Abstract
 
+variable (𝕜 E : Type*) [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E]
+
 namespace Geometry
 
 -- TODO: update to new binder order? not sure what binder order is correct for `down_closed`.
@@ -92,15 +94,13 @@ 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 (𝕜 E : Type*) [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E]
+structure SimplicialComplex
     extends AbstractSimplicialComplex E where
   /-- the vertices in each face are affine independent: this is an implementation detail -/
   indep : ∀ {s}, s ∈ faces → AffineIndependent 𝕜 ((↑) : s → E)
   inter_subset_convexHull : ∀ {s t}, s ∈ faces → t ∈ faces →
     convexHull 𝕜 ↑s ∩ convexHull 𝕜 ↑t ⊆ convexHull 𝕜 (s ∩ t : Set E)
 
-variable (𝕜 E : Type*) [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E]
-
 namespace SimplicialComplex
 
 variable {𝕜 E}

From ce50ade62eef538a7ed8a0eed3f9202da4d7cbc5 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Tue, 30 Dec 2025 10:30:50 -0800
Subject: [PATCH 19/22] reduce line count

---
 Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
index 6d6d8009ef8d08..333ec08b8b72ec 100644
--- a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
+++ b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
@@ -94,8 +94,7 @@ 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
-    extends AbstractSimplicialComplex E where
+structure SimplicialComplex extends AbstractSimplicialComplex E where
   /-- the vertices in each face are affine independent: this is an implementation detail -/
   indep : ∀ {s}, s ∈ faces → AffineIndependent 𝕜 ((↑) : s → E)
   inter_subset_convexHull : ∀ {s t}, s ∈ faces → t ∈ faces →

From a320858ce72a8e8c3ea60c6dfb2e76215339d89e Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sun, 4 Jan 2026 15:59:14 -0800
Subject: [PATCH 20/22] Update
 Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean

Co-authored-by: Ben Eltschig <43812953+peabrainiac@users.noreply.github.com>
---
 Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
index 333ec08b8b72ec..63da64c00a753d 100644
--- a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
+++ b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
@@ -12,7 +12,7 @@ public import Mathlib.LinearAlgebra.AffineSpace.Independent
 # Simplicial complexes
 
 In this file, we define simplicial complexes, both abstractly and in `𝕜`-modules.
-An abstract simplicial complex is a downwards-closed collection of nonempty finte sets,
+An 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

From 356b8c86587c13984273b4bc3c536cd969b6d520 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sun, 4 Jan 2026 16:29:58 -0800
Subject: [PATCH 21/22] refactor to new file

---
 .../SimplicialComplex/Basic.lean              | 136 ++++++++++++++++++
 .../Convex/SimplicialComplex/Basic.lean       |  42 +-----
 2 files changed, 139 insertions(+), 39 deletions(-)
 create mode 100644 Mathlib/AlgebraicTopology/SimplicialComplex/Basic.lean

diff --git a/Mathlib/AlgebraicTopology/SimplicialComplex/Basic.lean b/Mathlib/AlgebraicTopology/SimplicialComplex/Basic.lean
new file mode 100644
index 00000000000000..5c4ef0eba17d81
--- /dev/null
+++ b/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
diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
index 63da64c00a753d..23353e2a044f0f 100644
--- a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
+++ b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
@@ -5,13 +5,14 @@ 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, both abstractly and in `𝕜`-modules.
+In this file, we define simplicial complexes over `𝕜`-modules.
 An 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)
@@ -20,7 +21,6 @@ to the vertices and the underlying set of a simplex.
 
 ## Main declarations
 
-* `AbstractSimplicialComplex ι`: An abstract simplicial complex with vertices of type `ι`.
 * `SimplicialComplex 𝕜 E`: A simplicial complex in the `𝕜`-module `E`.
 * `SimplicialComplex.vertices`: The zero-dimensional faces of a simplicial complex.
 * `SimplicialComplex.facets`: The maximal faces of a simplicial complex.
@@ -48,42 +48,6 @@ Simplicial complexes can be generalized to affine spaces once `ConvexHull` has b
 
 open Finset Set
 
-section Abstract
-
-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 AbstractSimplicialComplex 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 AbstractSimplicialComplex
-
-/-- The complex consisting of only the faces present in both of its arguments. -/
-instance : Min (AbstractSimplicialComplex ι) :=
-  ⟨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⟩ }⟩
-
-instance : SemilatticeInf (AbstractSimplicialComplex ι) :=
-  { PartialOrder.lift faces (fun _ _ => AbstractSimplicialComplex.ext) with
-    inf := (· ⊓ ·)
-    inf_le_left := fun _ _ _ hs => hs.1
-    inf_le_right := fun _ _ _ hs => hs.2
-    le_inf := fun _ _ _ hKL hKM _ hs => ⟨hKL hs, hKM hs⟩ }
-
-end AbstractSimplicialComplex
-
-end Abstract
-
 variable (𝕜 E : Type*) [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E]
 
 namespace Geometry
@@ -94,7 +58,7 @@ 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 extends AbstractSimplicialComplex E where
+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)
   inter_subset_convexHull : ∀ {s t}, s ∈ faces → t ∈ faces →

From 0989368e4904a3e12ea7ed9e2dccc642d6c4bf92 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sun, 4 Jan 2026 16:32:57 -0800
Subject: [PATCH 22/22] documentation

---
 Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
index 23353e2a044f0f..ec7de94386d547 100644
--- a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
+++ b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
@@ -13,7 +13,7 @@ public import Mathlib.LinearAlgebra.AffineSpace.Independent
 # Simplicial complexes
 
 In this file, we define simplicial complexes over `𝕜`-modules.
-An abstract simplicial complex is a downwards-closed collection of nonempty finite sets,
+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