Do some ASC Shelling propositions

Coxeter/ForMathlib/ASCShelling.lean

@@ -1,45 +1,65 @@
---import Mathlib.Data.Finset.Basic
 import Mathlib.Data.Set.Card
 import Coxeter.ForMathlib.AbstractSimplicialComplex
 
-
-
-
 namespace AbstractSimplicialComplex
-variable {V : Type*} --[DecidableEq V]
-
-/-
-Definition: Let F be a pure abstract simplicial complex of rank d+1.
-A shelling of F is an linear ordering l_1, ⋯ , l_m of all (maximal) facets of F such that
- l_i ⊓ (⨆ {j < i}, l_j)  is an abstract simplicial complex pure of rank d.
--/
+variable {V : Type*} [Fintype V] [DecidableEq V]
 
-def shelling {F : AbstractSimplicialComplex V} [hpure: Pure F] {m : ℕ } (l : Fin m ≃ Facets F) := F.rank > 0 ∧
-  ∀ i : Fin m, 1 < i.val → IsPure' ((⨆ j ∈ {j | j<i}, closure {(l j).val}) ⊓ (closure {(l i).val})) (F.rank-1)
+/-- If there is *some finiteness condition* on `F : ASC V`, then there every face of `F` is contained in a facet -/
+theorem exists_subset_Facet {F : AbstractSimplicialComplex V} (hf : f ∈ F) : ∃ g ∈ F.Facets, f ⊆ g := by
+  let s := {g ∈ F | f ⊆ g}
+  have : Set.Finite s := Set.Finite.subset (s := F.faces) (Set.toFinite _) fun a ha ↦ ha.1
+  rcases Set.Finite.exists_maximal_wrt (fun (a : Finset V) ↦ a) s this ⟨f, hf, by rfl⟩ with ⟨g, hg1, hg2⟩
+  refine ⟨g, ⟨hg1.1, ?_⟩, hg1.2⟩
+  intro a ha1 ha2
+  apply hg2 a ⟨ha1, (subset_trans hg1.2 ha2)⟩ ha2
 
+/--
+Definition: Let `F` be a pure abstract simplicial complex of rank `d + 1` with finite facets.
+A shelling of `F` is an linear ordering `l₁`, ⋯ , `lₘ` of all (maximal) facets of F such that
+ `lᵢ ⊓ (⨆ {j < i}, lⱼ)`  is an abstract simplicial complex pure of rank `d`.
+-/
+def Shelling {F : AbstractSimplicialComplex V} {m : ℕ} (l : Fin m ≃ Facets F) := F.rank > 0 ∧
+  ∀ k : Fin m, 0 < k.1 → IsPure' ((⨆ j : {j // j < k}, closure {(l j).1}) ⊓ (closure {(l k).1})) (F.rank - 1)
 
-/-
-Definition': Let F be a pure abstract simplicial complex of rank d+1.
-A shelling of F is an linear ordering l_1, ⋯ , l_m of all (maximal) facets of F such that
- for any i < k, there exists j < k, such that l_i ∩ l_k ⊆ l_j ∩ l_k and |l_j ∩ l_k| = d.
+/--
+Definition': Let `F` be a pure abstract simplicial complex of rank `d + 1`.
+A shelling of `F` is an linear ordering `l₁`, ⋯ , `lₘ` of all (maximal) facets of `F` such that
+ for any `i < k`, there exists `j < k`, such that `lᵢ ∩ lₖ ⊆ lⱼ ∩ lₖ` and `|lⱼ ∩ lₖ| = d`.
 -/
-def shelling' [DecidableEq V] {F :  AbstractSimplicialComplex V} [hpure:Pure F]  {m : ℕ } (l : Fin m ≃ Facets F) :=
+def Shelling' {F :  AbstractSimplicialComplex V} {m : ℕ} (l : Fin m ≃ Facets F) :=
   F.rank > 0 ∧
   ∀ k i : Fin m, i < k → ∃ j : Fin m, j < k ∧
-    ((l i).val ∩ (l k).val ⊆ (l j).val ∩ (l k).val) ∧
-    ((l j).val ∩ (l k).val).card + 1 = F.rank
-
+    (l i).1 ∩ (l k).1 ⊆ (l j).1 ∩ (l k).1 ∧
+    ((l j).1 ∩ (l k).1).card + 1 = F.rank
 
-/- Lemma: The two definitions of shellings are equivalent.
+/-- Lemma: The two definitions of shellings are equivalent.
 -/
-lemma shelling_iff_shelling' [DecidableEq V] {F : AbstractSimplicialComplex V}  [hpure: Pure F]    {m : ℕ} (l : Fin m ≃ Facets F) :
-    shelling l ↔ shelling' l := by sorry
+lemma shelling_iff_shelling'_aux {F : AbstractSimplicialComplex V} (hF : IsPure F) {m : ℕ} [NeZero m] (l : Fin m ≃ Facets F) :
+    Shelling l ↔ Shelling' l := by
+    constructor <;> refine fun ⟨a, h⟩ ↦ ⟨a, ?_⟩
+    · intro k i ilek
+      replace h := h k <| lt_of_le_of_lt (zero_le _) (Fin.lt_def.mp ilek)
+      rw [iSup_inf_eq] at h
+      letI : Nonempty { j // j < k } := ⟨0, lt_of_le_of_lt (Fin.zero_le' _) ilek⟩
+      have : (l i).1 ∩ (l k).1 ∈ ⨆ j : {j // j < k}, closure {(l j).1} ⊓ closure {(l k).1} := by
+        -- rw [← mem_faces, iSup_faces_of_nonempty]
+        sorry
+      -- have : (l i).1 ∩ (l k).1 ∈ F := F.lower' (Finset.inter_subset_left _ _) (l i).2.1
+      rcases exists_subset_Facet this with ⟨f, hf_mem, hf_big⟩
+      rcases exits_mem_faces_of_mem_iSup hf_mem with ⟨j, hj⟩
+      rw [← closure_singleton_inter_eq_inf, closure_singleton_Facets, Set.mem_singleton_iff] at hj
+      subst hj
+      refine ⟨j, j.2, by convert hf_big, ?_⟩ -- have to `covnert` due to previous using of classical
 
-/- Definition: An abstract simplicial complex F is called shellable, if it admits a shelling.
--/
-def shellable (F : AbstractSimplicialComplex F) [Pure F] := ∃ (m: ℕ) (l : Fin m ≃ Facets F), shelling l
+      sorry
+    · intro k kge0
+
+      sorry
+
+/-- Definition: An abstract simplicial complex `F` is called shellable, if it admits a shelling. -/
+def Shellable (F : AbstractSimplicialComplex F) := ∃ (m : ℕ) (l : Fin m ≃ Facets F), Shelling l
 
-lemma cone_shellabe_iff [DecidableEq V] {F G : AbstractSimplicialComplex V} {r : ℕ} [Pure F] [Pure G] (x : V)  (hcone: Cone F G x) :
-  shellable F ↔ shellable G  := by sorry
+-- lemma cone_Shellabe_iff {F G : AbstractSimplicialComplex V} {r : ℕ} [Pure F] [Pure G] (x : V) (hcone: Cone F G x) :
+--   Shellable F ↔ Shellable G  := by sorry
 
 end AbstractSimplicialComplex

Coxeter/ForMathlib/ASCShellingProps.lean

@@ -0,0 +1,121 @@
+import Mathlib.Data.Set.Card
+import Coxeter.ForMathlib.ASCShelling
+
+namespace ASCShellingProps
+
+open AbstractSimplicialComplex
+open Classical
+
+variable {V : Type*} --[DecidableEq V]
+
+def Deletion (F : AbstractSimplicialComplex V) (x : V) : Set F.faces :=
+  {f | x ∉ f.1}
+
+def DeletionSimplex (F : AbstractSimplicialComplex V) (x : V) : AbstractSimplicialComplex V where
+  faces := Deletion F x
+  empty_mem := by
+    simp only [Deletion, Set.mem_image, Set.mem_setOf_eq, Subtype.exists, mem_faces,
+      exists_and_left, exists_prop, exists_eq_right_right, Finset.not_mem_empty, not_false_eq_true,
+      true_and]
+    exact F.empty_mem
+  lower' := by
+    simp only [Deletion]
+    intro _ _ hab ha
+    simp only [Set.mem_image, Set.mem_setOf_eq, Subtype.exists, mem_faces, exists_and_left,
+      exists_prop, exists_eq_right_right] at ha ⊢
+    constructor
+    · have := ha.1
+      contrapose! this
+      exact hab this
+    · exact F.lower' hab ha.2
+
+def Link (F : AbstractSimplicialComplex V) (x : vertices F) : Set F.faces :=
+  {f | x.1 ∉ f.1 ∧ {x.1} ∪ f.1 ∈ F.faces}
+
+def LinkSimplex (F : AbstractSimplicialComplex V) (x : vertices F) : AbstractSimplicialComplex V where
+  faces := Link F x
+  empty_mem := by
+    simp only [Set.mem_image, Subtype.exists, mem_faces, exists_and_right, exists_eq_right, Link]
+    use F.empty_mem
+    simp only [Set.mem_setOf_eq, Finset.not_mem_empty, not_false_eq_true, Finset.union_empty,
+      true_and]
+    exact (vertices_iff_singleton_set_face F x).mpr x.2
+  lower' := sorry
+
+def LinkFace (F : AbstractSimplicialComplex V) (s : F.faces) : Set F.faces :=
+  {f | s.1 ∩ f.1 = ∅ ∧ s.1 ∪ f.1 ∈ F.faces }
+
+def Star (F : AbstractSimplicialComplex V) (s : F.faces) : Set F.faces :=
+  {f | s.1 ∪ f.1 ∈ F.faces }
+
+lemma LinkFace_subset_Star (F : AbstractSimplicialComplex V) (s : F.faces) :
+  LinkFace F s ⊆ Star F s := fun _ h ↦ h.2
+
+lemma delete_vertex (F : AbstractSimplicialComplex V) (x : vertices F) :
+    vertices F \ {x.1} = (vertices (DeletionSimplex F x.1)) := by
+  ext t
+  simp [DeletionSimplex, Deletion]
+  constructor
+  · intro h
+    simp [Set.image]
+    use {t}
+    simp only [id_eq, Set.coe_setOf, Set.mem_setOf_eq, Set.mem_range, Finset.coe_eq_singleton,
+      Subtype.exists, exists_prop, exists_eq_right, Finset.mem_singleton, Set.mem_singleton_iff,
+      and_true]
+    refine And.intro ?_ ((vertices_iff_singleton_set_face F t).mpr h.1)
+    by_contra a
+    rw [a] at h
+    exact h.2 rfl
+  · rintro ⟨s, ⟨⟨a, ha⟩, hts⟩⟩
+    refine And.intro ⟨s, And.intro ?_ hts⟩ ?_
+    · simp only [Set.image, Set.range, Set.mem_setOf_eq]
+      have := a.2
+      simp only [id_eq, Set.mem_image, Set.mem_setOf_eq, Subtype.exists, mem_faces, exists_and_left,
+        exists_prop, exists_eq_right_right] at this
+      refine ⟨⟨a.1, this.2⟩, ?_⟩
+      rw [← ha]
+    · by_contra tx
+      rw [tx, ← ha] at hts
+      --apply a.2.2.1
+      sorry
+      /-have : x.1 ∈ a.1 := by
+        sorry
+      sorry
+      --simp [ha]-/
+
+lemma terminating_size [Fintype V] (F : AbstractSimplicialComplex V) (x : vertices F) :
+    (vertices (DeletionSimplex F x.1)).ncard < (vertices F).ncard := by
+  sorry
+
+-- Consider replacing Fintype V -> Fintype (vertices F)
+def VertexDecomposableInductive (r n : ℕ) [Fintype V] (F : AbstractSimplicialComplex V)
+    (h1 : r = F.rank) (h2 : n = (vertices F).ncard) : Prop :=
+  match r, n with
+  | 0, _ => True
+  --| _, 0 => True
+  | r' + 1, _ => (Pure F) ∧ (∃ (f : Finset V), F = simplex f) ∨
+      (∃ (x : vertices F), (by
+    let nd := (vertices (DeletionSimplex F x.1)).ncard
+    let nl := (vertices (LinkSimplex F x)).ncard
+    by_cases h : ((DeletionSimplex F x.1).rank = r' + 1) ∧ (LinkSimplex F x).rank = r'
+    · have := terminating_size F x
+      refine VertexDecomposableInductive (r' + 1) nd (DeletionSimplex F x) h.1.symm rfl ∧
+        VertexDecomposableInductive r' nl (LinkSimplex F x) h.2.symm rfl
+    · exact False
+      ))
+
+lemma fin_vertex_iff_fin_faces (F : AbstractSimplicialComplex V) : Finite F.faces ↔ Finite (vertices F) := by
+  sorry
+
+def VertexDecomposable [Fintype V] (F : AbstractSimplicialComplex V) : Prop :=
+  VertexDecomposableInductive F.rank (vertices F).ncard F rfl rfl
+
+-- see if we can remove Fintype V
+-- something is off, need to check empty set
+
+
+
+-- Page 83: define VertexDecomposable, SheddingVertex
+-- create new file to do property 1, import ASC shelling, merge to master before taking
+
+end ASCShellingProps