PosetASC (#53)

* Fix unsolved goal * test pr * Update PosetChain.lean * Update PosetChain.lean * chain_nodup & chain_singleton_of_head_eq_tail * Update PosetChain.lean * maximal_chain'₂_iff_ledot & maximal_chain_iff_cover * small improve * maximal_chain'_cons * Update PosetChain.lean * prove 2 6 * Update PosetChain.lean * tmp * prove 8th lemma * Update PosetChain.lean * poset * max_chain_mem_edge & new lemma mem_adjPairs_iff * mem_adjPairs_iff * Update PosetChain.lean * PosetGraded && change of PosetChain (#12) * Update AbstractSimplicialComplex.lean Make all comments docComments * Update AbstractSimplicialComplex.lean * Update AbstractSimplicialComplex.lean * Update ASCShelling.lean Fix a mispelling * update ASC * change `simp` to `simp only` * i love coxeter groups(bushi ) * Update AbstractSimplicialComplex.lean * Update AbstractSimplicialComplex.lean * update ASC * Update AbstractSimplicialComplex.lean change `\U i\in s` to `\U i : s` * Update AbstractSimplicialComplex.lean * change rank to finite version * PosetGraded --------- Co-authored-by: Lei Bichang <[email protected]> Co-authored-by: Lei Bichang <[email protected]> Co-authored-by: Haotian Liu <[email protected]> Co-authored-by: lpya942 <[email protected]> Co-authored-by: Haocheng Wang <[email protected]> * Develop (#13) * Sync with NUS && fmt (#14) * Update AbstractSimplicialComplex.lean Make all comments docComments * Update AbstractSimplicialComplex.lean * Update AbstractSimplicialComplex.lean * Update ASCShelling.lean Fix a mispelling * update ASC * change `simp` to `simp only` * i love coxeter groups(bushi ) * Update AbstractSimplicialComplex.lean * Update AbstractSimplicialComplex.lean * update ASC * Update AbstractSimplicialComplex.lean change `\U i\in s` to `\U i : s` * Update AbstractSimplicialComplex.lean * Update AbstractSimplicialComplex.lean * update ASC (#5) * fmt * update ASC (#6) * update ASC * update ASC * Update AbstractSimplicialComplex.lean * Prove `closure_eq_iSup` 1. prove that taking supremum commutes with taking closure 2. prove `closure_eq_iSup` * Update AbstractSimplicialComplex.lean (#7) * Update AbstractSimplicialComplex.lean * Update AbstractSimplicialComplex.lean * Revert "Update AbstractSimplicialComplex.lean (#7)" (#8) This reverts commit 512d8fe. --------- Co-authored-by: Lei Bichang <[email protected]> Co-authored-by: Lei Bichang <[email protected]> Co-authored-by: Haotian Liu <[email protected]> Co-authored-by: lpya942 <[email protected]> Co-authored-by: Haocheng Wang <[email protected]> Co-authored-by: Haotian Liu <[email protected]> Co-authored-by: slashbade <[email protected]> * Develop (#15) * PosetASC aux sorries (#16) * fmt * fmt * aux for PosetASC * Update PosetChain.lean (#17) * prove Delta using List.filter (#18) * Develop (#20) * Create ReflectionOrder.lean * ReflectionOrder init * Update ReflectionOrder.lean * fix Hecke * Update Defs.lean * Update Defs.lean * redef * reflAlg init * Update GraphSearchAux.lean * Update GraphSearchAux.lean * fix refl * Update InitialSectionsOfRelf.lean * bruhat order locally finite * try to define h * Update PosetChain.lean * Update PosetASC.lean * Prove length_diff_one and dependent lemmas. * fix * fix Hecke * fix Rpoly * 000 --------- Co-authored-by: jjdishere <[email protected]> Co-authored-by: ampan98 <[email protected]> Co-authored-by: slashbade <[email protected]> Co-authored-by: Chong Jing Quan <[email protected]> * PosetASC Pure (#19) * Update PosetChain.lean * Update PosetASC.lean * 000 * PosetASC * Clear * sync --------- Co-authored-by: XintaoYu <[email protected]> Co-authored-by: XintaoYu <[email protected]> --------- Co-authored-by: timechess <[email protected]> Co-authored-by: zsj <[email protected]> Co-authored-by: zzsj2001 <[email protected]> Co-authored-by: Hennessy <[email protected]> Co-authored-by: Lei Bichang <[email protected]> Co-authored-by: Lei Bichang <[email protected]> Co-authored-by: Haotian Liu <[email protected]> Co-authored-by: lpya942 <[email protected]> Co-authored-by: Haocheng Wang <[email protected]> Co-authored-by: Haotian Liu <[email protected]> Co-authored-by: slashbade <[email protected]> Co-authored-by: jjdishere <[email protected]> Co-authored-by: ampan98 <[email protected]> Co-authored-by: Chong Jing Quan <[email protected]>
NUS-Math-Formalization · Apr 21, 2024 · ea8eb1d · ea8eb1d
1 parent 722d4cc
commit ea8eb1d
Show file tree

Hide file tree

Showing 2 changed files with 54 additions and 13 deletions.
diff --git a/Coxeter/ForMathlib/PosetASC.lean b/Coxeter/ForMathlib/PosetASC.lean
@@ -3,11 +3,11 @@ import Mathlib.Data.List.Basic
 import Coxeter.ForMathlib.AbstractSimplicialComplex
 import Coxeter.ForMathlib.PosetChain
 import Coxeter.ForMathlib.PosetGraded
+import Mathlib.Data.Finset.Sort
 
-
+noncomputable section
 open Classical
 
-
 namespace PartialOrder
 
 open AbstractSimplicialComplex
@@ -21,7 +21,6 @@ Note that each element in Delta(P) will considered as a chain.
 @[simp]
 def Delta_List (P : Type*) [PartialOrder P] : Set (List P) := {L : List P | chain L}
 
-
 /-
 Definition: Let P be a poset. Delta P is the set of all chains in P, which is an abstract simplicial complex.
 Note that each element in Delta (P) will considered as a subset of P.
@@ -31,13 +30,55 @@ abbrev Delta (P : Type*) [PartialOrder P] : AbstractSimplicialComplex P where
   faces := List.toFinset '' Delta_List P
   empty_mem := by simp
   lower' := by
-    sorry
+    simp only [IsLowerSet]
+    intro a b blea ain
+    simp only [Delta_List, Set.mem_image, Set.mem_setOf_eq]
+    simp at ain
+    rcases ain with ⟨al, chain_a, ha⟩
+    use List.filter (· ∈ b) al
+    simp only [List.toFinset_filter, decide_eq_true_eq]
+    constructor
+    · simp [chain]
+      exact List.Chain'.sublist chain_a (List.filter_sublist al)
+    · rw [ha]
+      simp at blea
+      ext x
+      simp only [Finset.mem_filter, and_iff_right_iff_imp]
+      intro hb
+      exact blea hb
+
+
+lemma List.sub_toFinset_of_sublist {L₁ L₂ : List P} : L₂.Sublist L₁ → L₂.toFinset ⊆ L₁.toFinset := by
+  intro sublst
+  intro x hx
+  simp at hx
+  have := List.Sublist.subset sublst
+  have : x ∈ L₁ := this hx
+  simp [this]
 
 /-
 Definition: Let P be a graded poset. Then Delta.ASC (P) is a pure abstract simplicial complex.
 -/
 instance Delta.Pure {P : Type*} [PartialOrder P] [Fintype P] [GradedPoset P]: Pure (Delta P) where
-  pure := sorry
+  pure := by
+    rintro s ⟨hs₁, hs₂⟩ t ⟨ht₁, ht₂⟩
+    have := GradedPoset.pure (P := P)
+    simp [Facets, IsFacet, Delta, mem_faces.symm] at *
+    rcases hs₁ with ⟨L₁, chain_l₁, seq⟩
+    rcases ht₁ with ⟨L₂, chain_l₂, teq⟩
+    subst seq teq
+    rw [List.toFinset_card_of_nodup (chain_nodup chain_l₁), List.toFinset_card_of_nodup (chain_nodup chain_l₂)]
+    refine this _ _ chain_l₁ ?_ chain_l₂ ?_
+    · intro L' chain_l' sublst
+      apply List.Sublist.eq_of_length sublst
+      rw [← List.toFinset_card_of_nodup (chain_nodup chain_l₁), ← List.toFinset_card_of_nodup (chain_nodup chain_l')]
+      have := hs₂ L' chain_l' (List.sub_toFinset_of_sublist sublst)
+      simp [this]
+    · intro L' chain_l' sublst
+      apply List.Sublist.eq_of_length sublst
+      rw [← List.toFinset_card_of_nodup (chain_nodup chain_l₂), ← List.toFinset_card_of_nodup (chain_nodup chain_l')]
+      have := ht₂ L' chain_l' (List.sub_toFinset_of_sublist sublst)
+      simp [this]
 
 
 

diff --git a/Coxeter/ForMathlib/PosetChain.lean b/Coxeter/ForMathlib/PosetChain.lean
@@ -29,7 +29,7 @@ Definition: A chain in the poset P is a finite sequence x₀ < x₁ < ⋯ < x_n.
 -/
 abbrev chain (L : List P) : Prop := List.Chain' (· < ·) L
 
-abbrev Chains (P : Type*) [PartialOrder P] : Set (List P) := { L | chain L}
+abbrev Chains (P : Type*) [PartialOrder P] : Set (List P) := { L | chain L }
 
 section chain
 
@@ -105,6 +105,7 @@ lemma chain_nodup {L : List P} (h : chain L) : L.Nodup := by
         apply List.Chain'.tail h
       exact hl' this
 
+
 -- May not be needed, use chain_nodup
 lemma chain_singleton_of_head_eq_tail  {L : List P} (a : P) (chain_l : chain L)
  (lha : L.head? = some a) (lta :  L.getLast? = some a) : L.length = 1  := by
@@ -567,18 +568,17 @@ lemma max_chain_mem_edge {P : Type*} [PartialOrder P] {L: List P} {e: P × P} :
     exact this.2.1
 
 
+
+
 /-
 We define the set of all maximal chains of P.
 -/
 
-instance : Fintype (Set.Elem {L : List P | L.Nodup}) :=
-  inferInstanceAs (Fintype {L : List P // L.Nodup})
-
-def auxinj : { L : List P | maximal_chain L } → Set.toFinset {L : List P | L.Nodup} :=
-  fun l ↦ ⟨l.val, by simp; apply chain_nodup l.prop.1⟩
+instance : Fintype (Set.Elem { L : List P | L.Nodup }) :=
+  inferInstanceAs (Fintype { L : List P // L.Nodup })
 
-instance : Fintype { L : List P| maximal_chain L } :=
-  Fintype.ofInjective auxinj (by simp [Function.Injective, auxinj])
+instance : Fintype { L : List P | maximal_chain L } :=
+  Set.fintypeSubset { L : List P | L.Nodup} fun _ h ↦ Set.mem_setOf_eq.mpr (chain_nodup (Set.mem_setOf_eq.mp h).1)
 
 abbrev maximalChains (P : Type*) [PartialOrder P] [Fintype P] : Finset (List P) :=
   Set.toFinset { L | maximal_chain L }