PosetChain (#37)

* 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]> --------- 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]>
NUS-Math-Formalization · Apr 19, 2024 · 428bc98 · 428bc98
1 parent fd31af8
commit 428bc98
Show file tree

Hide file tree

Showing 4 changed files with 417 additions and 39 deletions.
diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -203,6 +203,7 @@ If the size of simplices in F is unbounded, it has rank 0 by definition.
 
 Remark: We should general be careful with the unbounded case.
 -/
+
 noncomputable def rank (F : AbstractSimplicialComplex V) : ℕ := iSup fun s : F.faces => s.1.card
 
 /-- Definition: For a collection s of subsets of V, we denote by closure s the smallest ASC over V containing all elements in s

diff --git a/Coxeter/ForMathlib/AdjacentPair.lean b/Coxeter/ForMathlib/AdjacentPair.lean
@@ -7,7 +7,8 @@ variable {α : Type*}
 /- Definition: The adjacent pairs of a list [a_1,a_2, ⋯, a_n] is defined to be
   [(a_1, a_2), (a_2, a_3), ⋯, (a_{n-1}, a_n)].
   If the list L has length less than 2, the new list will be an empty list by convention. -/
-def adjPairs : List α  → List (α × α )
+@[simp]
+def adjPairs : List α  → List (α × α)
   | [] => []
   | _ :: []  => []
   | a :: b :: l =>  ((a, b) : α  × α) ::  (b :: l).adjPairs
@@ -28,11 +29,47 @@ lemma adjPairs_tail {h a b : α} {tail : List α} : (a,b) ∈ tail.adjPairs →
     intro h1
     right; exact h1
 
+
+lemma mem_adjPairs_iff {a b : α} {L : List α} : (a,b) ∈ L.adjPairs ↔ ∃ l₁ l₂ : List α, L = l₁ ++ a :: b :: l₂ := by
+  constructor
+  · intro h
+    induction L with
+    | nil => simp at h
+    | cons e tail he =>
+        by_cases h' : (a, b) ∈ tail.adjPairs
+        · have := he h'
+          rcases this with ⟨l₁, l₂, hl⟩
+          use e :: l₁, l₂
+          simp [hl]
+        · match tail with
+          | [] => simp at h
+          | f :: tail' =>
+              simp at h
+              rcases h with h'' | h''
+              · simp [h'']
+                use [], tail'
+                simp
+              · contradiction
+  · intro h
+    rcases h with ⟨l₁, l₂, h'⟩
+    rw [h']
+    revert L
+    induction l₁ with
+    | nil => simp
+    | cons e tail he =>
+        intro L hL
+        have aux : L.tail = tail ++ a :: b :: l₂ := by simp [hL]
+        have := he aux
+        apply adjPairs_tail this
+
+
 /- Definition (programming):
 The adjacent extened pairs of a List L is a List of adjacent pairs of L together with the claim that e ∈ adjPairs L -/
 def adjEPairs (L : List α) : List ({e : α × α  | e ∈ L.adjPairs}) := match L with
   | [] => []
   | _ :: [] => []
   | a :: b :: l =>  ⟨(a, b), List.adjPairs_cons⟩ :: (List.map (fun e => ⟨e.val, List.adjPairs_tail e.prop ⟩) <| List.adjEPairs (b :: l))
 
+
+
 end List
-Original file line number
+Diff line change
@@ Expand Up @@
     Remark: We should general be careful with the unbounded case.
     -/
     noncomputable def rank (F : AbstractSimplicialComplex V) : ℕ := iSup fun s : F.faces => s.1.card
     /-- Definition: For a collection s of subsets of V, we denote by closure s the smallest ASC over V containing all elements in s
@@ Expand Down @@