Zulip Chat Archive

You have two userids on this site, you ask questions very rudely and you seem to show no signs of attempting to learn anything. This entire thread makes me miserable. Can you please try to do better? I don't know if it's a language issue but "what dose that suppose to mean" comes off as extremely rude, which is the exact opposite of essentially all other conversations going on in this Zulip. Please go and read the lean manual about lakefiles, or search this Zulip yourself, because your rudeness means that I am in no mood to answer your questions. NB the butterfly emoji above is something we use to indicate "this comment is inappropriate".

BANGJI HU (Dec 03 2024 at 11:07):

is it under active development in leancamcombi

BANGJI HU (Dec 03 2024 at 11:07):

@Yaël Dillies

Yaël Dillies (Dec 03 2024 at 13:54):

Not right now, no. I am too busy on other things

BANGJI HU (Dec 04 2024 at 03:03):

import Mathlib.Analysis.Convex.SimplicialComplex.Basic

open BigOperators
open Classical


namespace Geometry
open SimplicialComplex

variable (k : Type*) {E : Type*} {ι : Type*} [hLO: LinearOrderedField k]  [AddCommGroup E] [Module k E]

local notation "SC" => SimplicialComplex k E

noncomputable section Subdivision
variable [hCZ: CharZero k]

abbrev barycenter (s : Finset E) : E :=  (s.card:k)⁻¹ • (∑ x in s, x)


@[simp]
abbrev bary_simplex (L : List (Finset E))  : Finset E:= Finset.image (@barycenter k E _ _ _ ) L.toFinset

lemma bary_simplex.nonempty {L : List (Finset E)} (hL : L ≠ []) : (bary_simplex k L)≠ ∅ := by
  intro h
  have := L.toFinset_eq_empty_iff.1 <| Finset.image_eq_empty.mp h
  exact hL this

def chainSet (faces : Set (Finset E)) := {L : List (Finset E)| L≠ [] ∧ L.Forall (fun s => s ∈ faces) ∧   List.Pairwise (fun s t => t.1 ⊂ s.1) L}

--One have to establish various properties of the chainSet


--One have to establish that the barycentric subdivision is a simplicial complex
def barycentric_subdivision (x : SC) : SC where
  faces := Set.image (bary_simplex k)  <| chainSet x.faces
  not_empty_mem := by
    intro ⟨L, ⟨hL1,_⟩,hL2⟩
    have := bary_simplex.nonempty k hL1
    exact this hL2

  indep := by sorry
  down_closed := by sorry
  inter_subset_convexHull := by sorry

end Subdivision


class SimplicialSimplex (sc : SimplicialComplex k E) where
  extremes : Finset E
  extreme_in_vertices : ↑extremes ⊆ sc.vertices
  extreme_indep : AffineIndependent k (Subtype.val : extremes → E)
  spanning : ∀ x:E, x ∈ convexHull k ↑extremes ↔ ∃ s ∈ sc.faces, x ∈ convexHull k s

namespace SimplicialSimplex

instance  subdivision (sc : SC) [hsc: SimplicialSimplex k sc]: SimplicialSimplex k (barycentric_subdivision k sc) where
  extremes := hsc.extremes
  extreme_in_vertices := by sorry
  extreme_indep := hsc.extreme_indep
  spanning := by sorry




noncomputable section support
-- Suppose t is a set of points, x is in the convexHull of t
-- define the support of x to be the smallest subset of t such that x in the convexHull of t.

abbrev Support (t: Finset E) (x : E) : Set E :=
  if x ∈ convexHull k ↑t then
    ⋂ s ∈ { s | s ⊆ t ∧  x ∈ convexHull k s}, s
  else
    ∅


/-
Show that support is a subset of t if x is contained in
the convexHull of t
-/
lemma support_subset_face {t: Finset E} {x : E} : Support k t x ⊆ t:= by
  unfold Support
  split_ifs
  · apply Set.biInter_subset_of_mem
    constructor
    · simp only [subset_refl]
    · assumption
  · apply Set.empty_subset

instance support.fintype {t: Finset E} {x : E}: Fintype (Support k t x) := by
  let s := {e ∈ t | e ∈ Support k t x}
  apply Fintype.ofFinset s
  intro e
  rw [Finset.mem_filter]
  constructor
  · intro h; exact h.2
  · intro hx; exact ⟨support_subset_face k hx,hx⟩

abbrev Support' (t: Finset E) (x : E) : Finset E := Support k t x |>.toFinset

/-
Show that support is a subset of t if x is contained in
the convexHull of t
-/

lemma mem_convexHullsupport {t: Finset E} {x : E}
  (h1: x ∈ convexHull k ↑t)
  (h2 : AffineIndependent k ((↑):t → E)):
   x ∈ convexHull k (Support k t x):= by sorry


end support

variable {k} in
abbrev Coloring (sc : SimplicialComplex k E) (ι : Type*) := sc.vertices → ι

variable {k} in
def ProperColoring {sc : SimplicialComplex k E} [ss : SimplicialSimplex k sc] (c : Coloring sc E) :=
  ∀ x : sc.vertices, c x ∈ Support k ss.extremes x

variable {sc : SimplicialComplex k E}

section restriction

variable {α β : Type*} {s t: Set α} (h : s ⊆ t)

def res  (f : t→ β) : s → β := fun s => f ⟨s.1,h s.2 ⟩

lemma res_def : res h f x = f ⟨x.1, h x.2⟩ := rfl



end restriction


def iota (f : sc.faces) : f.1 → sc.vertices :=
  fun x => ⟨x.1, by
    rw [Geometry.SimplicialComplex.vertices_eq]
    have :∃ i ∈ sc.faces, ↑x ∈ i := by
      use f.1; exact ⟨f.2,x.2⟩
    simp [this]
    ⟩

variable {k} in
lemma faces_subset_vertices (f : sc.faces) : ↑f.1 ⊆ sc.vertices
  := by
    rw [Geometry.SimplicialComplex.vertices_eq]
    intro x hx
    have :∃ i ∈ sc.faces, ↑x ∈ i := by
      use f.1; exact ⟨f.2,hx⟩
    simp [this]


variable {k} in
def res_coloring (c : Coloring sc ι) (f : sc.faces) : f.1 → ι
  := res (faces_subset_vertices f: ↑f.1 ⊆ sc.vertices) c

variable [ss : SimplicialSimplex k sc]

variable {k} in
def Rainbowfacet  (c : Coloring sc E) (f : sc.facets)
 := res_coloring c ⟨f.1, facets_subset
 f.2⟩  '' Set.univ  = ss.extremes

theorem Sperner {c : Coloring sc E} (h : ProperColoring c) : ∃ f : sc.facets, Rainbowfacet c f := sorry





-- TODO: define boundary SimplicialSimplex, show that it is also a SimplicialSimplex

-- TODO: Show that every point in a SimplicialSimplex is a convex combination of its extrema

-- TODO: define the support of a convex combination of the extrema

-- TODO: define proper coloring on a SimplicialSimplex




end SimplicialSimplex




end Geometry


section Sperner


-- Define the notion of coloring.



-- TODO: State the Sperner's Lemma


end Sperner

Last updated: May 02 2025 at 03:31 UTC