The standard simplex

We define the standard simplices Δ[n] as simplicial sets. See files SimplicialSet.Boundary and SimplicialSet.Horn for their boundaries∂Δ[n] and horns Λ[n, i]. (The notations are available via open Simplicial.)

def SSet.stdSimplex : CategoryTheory.CosimplicialObject SSet

The functor SimplexCategory ⥤ SSet which sends ⦋n⦌ to the standard simplex Δ[n] is a cosimplicial object in the category of simplicial sets. (This functor is essentially given by the Yoneda embedding).

Equations

• SSet.stdSimplex = CategoryTheory.uliftYoneda.{?u.4, 0, 0}

def Simplicial.«termΔ[_]» : Lean.ParserDescr

The functor SimplexCategory ⥤ SSet which sends ⦋n⦌ to the standard simplex Δ[n] is a cosimplicial object in the category of simplicial sets. (This functor is essentially given by the Yoneda embedding).

Equations

• One or more equations did not get rendered due to their size.

instance SSet.instInhabited : Inhabited SSet

Equations

• SSet.instInhabited = { default := SSet.stdSimplex.obj (SimplexCategory.mk 0) }

instance SSet.instInhabitedTruncated {n : ℕ} : Inhabited (Truncated n)

Equations

• SSet.instInhabitedTruncated = { default := (SSet.truncation n).obj (SSet.stdSimplex.obj (SimplexCategory.mk 0)) }

@[simp]

theorem SSet.stdSimplex.map_id (n : SimplexCategory) : stdSimplex.map (SimplexCategory.Hom.mk OrderHom.id) = CategoryTheory.CategoryStruct.id (stdSimplex.obj n)

def SSet.stdSimplex.objEquiv {n : SimplexCategory} {m : SimplexCategoryᵒᵖ} : (stdSimplex.obj n).obj m ≃ (Opposite.unop m ⟶ n)

Simplices of the standard simplex identify to morphisms in SimplexCategory.

Equations

• SSet.stdSimplex.objEquiv = Equiv.ulift

instance SSet.stdSimplex.instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat (n i : ℕ) : FunLike ((stdSimplex.obj (SimplexCategory.mk n)).obj (Opposite.op (SimplexCategory.mk i))) (Fin (i + 1)) (Fin (n + 1))

If x : Δ[n] _⦋d⦌ and i : Fin (d + 1), we may evaluate x i : Fin (n + 1).

Equations

• One or more equations did not get rendered due to their size.

theorem SSet.stdSimplex.monotone_apply {n i : ℕ} (x : (stdSimplex.obj (SimplexCategory.mk n)).obj (Opposite.op (SimplexCategory.mk i))) : Monotone fun (j : Fin (i + 1)) => x j

theorem SSet.stdSimplex.ext {n d : ℕ} (x y : (stdSimplex.obj (SimplexCategory.mk n)).obj (Opposite.op (SimplexCategory.mk d))) (h : ∀ (i : Fin (d + 1)), x i = y i) : x = y

theorem SSet.stdSimplex.ext_iff {n d : ℕ} {x y : (stdSimplex.obj (SimplexCategory.mk n)).obj (Opposite.op (SimplexCategory.mk d))} : x = y ↔ ∀ (i : Fin (d + 1)), x i = y i

@[simp]

theorem SSet.stdSimplex.objEquiv_toOrderHom_apply {n i : ℕ} (x : (stdSimplex.obj (SimplexCategory.mk n)).obj (Opposite.op (SimplexCategory.mk i))) (j : Fin (i + 1)) : (SimplexCategory.Hom.toOrderHom (objEquiv x)) j = x j

theorem SSet.stdSimplex.objEquiv_symm_comp {n n' : SimplexCategory} {m : SimplexCategoryᵒᵖ} (f : Opposite.unop m ⟶ n) (g : n ⟶ n') : objEquiv.symm (CategoryTheory.CategoryStruct.comp f g) = (stdSimplex.map g).app m (objEquiv.symm f)

@[simp]

theorem SSet.stdSimplex.objEquiv_symm_apply {n m : ℕ} (f : SimplexCategory.mk m ⟶ SimplexCategory.mk n) (i : Fin (m + 1)) : (objEquiv.symm f) i = (SimplexCategory.Hom.toOrderHom f) i

@[reducible, inline]

abbrev SSet.stdSimplex.objMk {n : SimplexCategory} {m : SimplexCategoryᵒᵖ} (f : Fin ((Opposite.unop m).len + 1) →o Fin (n.len + 1)) : (stdSimplex.obj n).obj m

Constructor for simplices of the standard simplex which takes a OrderHom as an input.

Equations

• SSet.stdSimplex.objMk f = SSet.stdSimplex.objEquiv.symm (SimplexCategory.Hom.mk f)

@[simp]

theorem SSet.stdSimplex.objMk_apply {n m : ℕ} (f : Fin (m + 1) →o Fin (n + 1)) (i : Fin (m + 1)) : (objMk f) i = f i

def SSet.stdSimplex.asOrderHom {n : ℕ} {m : SimplexCategoryᵒᵖ} (α : (stdSimplex.obj (SimplexCategory.mk n)).obj m) : Fin ((Opposite.unop m).len + 1) →o Fin (n + 1)

The m-simplices of the n-th standard simplex are the monotone maps from Fin (m+1) to Fin (n+1).

Equations

• SSet.stdSimplex.asOrderHom α = SimplexCategory.Hom.toOrderHom α.down

theorem SSet.stdSimplex.map_apply {m₁ m₂ : SimplexCategoryᵒᵖ} (f : m₁ ⟶ m₂) {n : SimplexCategory} (x : (stdSimplex.obj n).obj m₁) : (stdSimplex.obj n).map f x = objEquiv.symm (CategoryTheory.CategoryStruct.comp f.unop (objEquiv x))

def SSet.yonedaEquiv {X : SSet} {n : SimplexCategory} : (stdSimplex.obj n ⟶ X) ≃ X.obj (Opposite.op n)

The canonical bijection (stdSimplex.obj n ⟶ X) ≃ X.obj (op n).

Equations

• SSet.yonedaEquiv = CategoryTheory.uliftYonedaEquiv

theorem SSet.stdSimplex.yonedaEquiv_map {n m : SimplexCategory} (f : n ⟶ m) : yonedaEquiv (stdSimplex.map f) = objEquiv.symm f

def SSet.stdSimplex.const (n : ℕ) (k : Fin (n + 1)) (m : SimplexCategoryᵒᵖ) : (stdSimplex.obj (SimplexCategory.mk n)).obj m

The (degenerate) m-simplex in the standard simplex concentrated in vertex k.

Equations

• SSet.stdSimplex.const n k m = SSet.stdSimplex.objMk ((OrderHom.const (Fin ((Opposite.unop m).len + 1))) k)

@[simp]

theorem SSet.stdSimplex.const_down_toOrderHom (n : ℕ) (k : Fin (n + 1)) (m : SimplexCategoryᵒᵖ) : SimplexCategory.Hom.toOrderHom (const n k m).down = (OrderHom.const (Fin ((Opposite.unop m).len + 1))) k

def SSet.stdSimplex.obj₀Equiv {n : ℕ} : (stdSimplex.obj (SimplexCategory.mk n)).obj (Opposite.op (SimplexCategory.mk 0)) ≃ Fin (n + 1)

The 0-simplices of Δ[n] identify to the elements in Fin (n + 1).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SSet.stdSimplex.obj₀Equiv_apply {n : ℕ} (x : (stdSimplex.obj (SimplexCategory.mk n)).obj (Opposite.op (SimplexCategory.mk 0))) : obj₀Equiv x = x 0

@[simp]

theorem SSet.stdSimplex.obj₀Equiv_symm_apply {n : ℕ} (i : Fin (n + 1)) : obj₀Equiv.symm i = const n i (Opposite.op (SimplexCategory.mk 0))

def SSet.stdSimplex.edge (n : ℕ) (a b : Fin (n + 1)) (hab : a ≤ b) : (stdSimplex.obj (SimplexCategory.mk n)).obj (Opposite.op (SimplexCategory.mk 1))

The edge of the standard simplex with endpoints a and b.

Equations

• SSet.stdSimplex.edge n a b hab = SSet.stdSimplex.objMk { toFun := ![a, b], monotone' := ⋯ }

theorem SSet.stdSimplex.coe_edge_down_toOrderHom (n : ℕ) (a b : Fin (n + 1)) (hab : a ≤ b) : ⇑(SimplexCategory.Hom.toOrderHom (edge n a b hab).down) = ![a, b]

def SSet.stdSimplex.triangle {n : ℕ} (a b c : Fin (n + 1)) (hab : a ≤ b) (hbc : b ≤ c) : (stdSimplex.obj (SimplexCategory.mk n)).obj (Opposite.op (SimplexCategory.mk 2))

The triangle in the standard simplex with vertices a, b, and c.

Equations

• SSet.stdSimplex.triangle a b c hab hbc = SSet.stdSimplex.objMk { toFun := ![a, b, c], monotone' := ⋯ }

theorem SSet.stdSimplex.coe_triangle_down_toOrderHom {n : ℕ} (a b c : Fin (n + 1)) (hab : a ≤ b) (hbc : b ≤ c) : ⇑(SimplexCategory.Hom.toOrderHom (triangle a b c hab hbc).down) = ![a, b, c]

def SSet.stdSimplex.face {n : ℕ} (S : Finset (Fin (n + 1))) : (stdSimplex.obj (SimplexCategory.mk n)).Subcomplex

Given S : Finset (Fin (n + 1)), this is the corresponding face of Δ[n], as a subcomplex.

Equations

• One or more equations did not get rendered due to their size.

theorem SSet.stdSimplex.face_obj {n : ℕ} (S : Finset (Fin (n + 1))) (U : SimplexCategoryᵒᵖ) : (face S).obj U = {f : (stdSimplex.obj (SimplexCategory.mk n)).obj U | Finset.image ⇑(SimplexCategory.Hom.toOrderHom (objEquiv f)) ⊤ ≤ S}

@[simp]

theorem SSet.stdSimplex.mem_face_iff {n : ℕ} (S : Finset (Fin (n + 1))) {d : ℕ} (x : (stdSimplex.obj (SimplexCategory.mk n)).obj (Opposite.op (SimplexCategory.mk d))) : x ∈ (face S).obj (Opposite.op (SimplexCategory.mk d)) ↔ ∀ (i : Fin (d + 1)), x i ∈ S

theorem SSet.stdSimplex.face_inter_face {n : ℕ} (S₁ S₂ : Finset (Fin (n + 1))) : face S₁ ⊓ face S₂ = face (S₁ ⊓ S₂)

theorem SSet.yonedaEquiv_comp {X Y : SSet} {n : SimplexCategory} (f : stdSimplex.obj n ⟶ X) (g : X ⟶ Y) : yonedaEquiv (CategoryTheory.CategoryStruct.comp f g) = g.app (Opposite.op n) (yonedaEquiv f)

theorem SSet.Subcomplex.range_eq_ofSimplex {X : SSet} {n : ℕ} (f : stdSimplex.obj (SimplexCategory.mk n) ⟶ X) : CategoryTheory.Subpresheaf.range f = ofSimplex (yonedaEquiv f)

theorem SSet.Subcomplex.yonedaEquiv_coe {X : SSet} {A : X.Subcomplex} {n : SimplexCategory} (f : stdSimplex.obj n ⟶ A.toSSet) : ↑(yonedaEquiv f) = yonedaEquiv (CategoryTheory.CategoryStruct.comp f A.ι)

theorem SSet.stdSimplex.face_eq_ofSimplex {n : ℕ} (S : Finset (Fin (n + 1))) (m : ℕ) (e : Fin (m + 1) ≃o ↥S) : face S = Subcomplex.ofSimplex (objMk ((OrderHom.Subtype.val fun (x : Fin (n + 1)) => x ∈ S).comp e.toOrderEmbedding.toOrderHom))

def SSet.stdSimplex.faceRepresentableBy {n : ℕ} (S : Finset (Fin (n + 1))) (m : ℕ) (e : Fin (m + 1) ≃o ↥S) : CategoryTheory.Functor.RepresentableBy (face S).toSSet (SimplexCategory.mk m)

If S : Finset (Fin (n + 1)) is order isomorphic to Fin (m + 1), then the face face S of Δ[n] is representable by m, i.e. face S is isomorphic to Δ[m], see stdSimplex.isoOfRepresentableBy.

Equations

• One or more equations did not get rendered due to their size.

def SSet.stdSimplex.isoOfRepresentableBy {X : SSet} {m : ℕ} (h : CategoryTheory.Functor.RepresentableBy X (SimplexCategory.mk m)) : stdSimplex.obj (SimplexCategory.mk m) ≅ X

If a simplicial set X is representable by ⦋m⦌ for some m : ℕ, then this is the corresponding isomorphism Δ[m] ≅ X.

Equations

• SSet.stdSimplex.isoOfRepresentableBy h = CategoryTheory.NatIso.ofComponents (fun (n : SimplexCategoryᵒᵖ) => (SSet.stdSimplex.objEquiv.trans h.homEquiv).toIso) ⋯

theorem SSet.stdSimplex.ofSimplex_yonedaEquiv_δ {n : ℕ} (i : Fin (n + 2)) : Subcomplex.ofSimplex (yonedaEquiv (stdSimplex.δ i)) = face {i}ᶜ

@[simp]

theorem SSet.stdSimplex.range_δ {n : ℕ} (i : Fin (n + 2)) : CategoryTheory.Subpresheaf.range (stdSimplex.δ i) = face {i}ᶜ

def SSet.stdSimplex.isoNerve (n : ℕ) : stdSimplex.obj (SimplexCategory.mk n) ≅ CategoryTheory.nerve (ULift.{u, 0} (Fin (n + 1)))

The standard simplex identifies to the nerve to the preordered type ULift (Fin (n + 1)).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SSet.stdSimplex.isoNerve_hom_app_apply {n d : ℕ} (s : (stdSimplex.obj (SimplexCategory.mk n)).obj (Opposite.op (SimplexCategory.mk d))) (i : Fin (d + 1)) : ((isoNerve.{u} n).hom.app (Opposite.op (SimplexCategory.mk d)) s).obj i = { down := s i }

@[simp]

theorem SSet.stdSimplex.isoNerve_inv_app_apply {n d : ℕ} (F : (CategoryTheory.nerve (ULift.{u, 0} (Fin (n + 1)))).obj (Opposite.op (SimplexCategory.mk d))) (i : Fin (d + 1)) : ((isoNerve.{u} n).inv.app (Opposite.op (SimplexCategory.mk d)) F) i = (F.obj i).down

theorem SSet.stdSimplex.mem_nonDegenerate_iff_strictMono {n d : ℕ} (s : (stdSimplex.obj (SimplexCategory.mk n)).obj (Opposite.op (SimplexCategory.mk d))) : s ∈ (stdSimplex.obj (SimplexCategory.mk n)).nonDegenerate d ↔ StrictMono ⇑s

theorem SSet.stdSimplex.mem_nonDegenerate_iff_mono {n d : ℕ} (s : (stdSimplex.obj (SimplexCategory.mk n)).obj (Opposite.op (SimplexCategory.mk d))) : s ∈ (stdSimplex.obj (SimplexCategory.mk n)).nonDegenerate d ↔ CategoryTheory.Mono (objEquiv s)

theorem SSet.stdSimplex.objEquiv_symm_mem_nonDegenerate_iff_mono {n d : ℕ} (f : SimplexCategory.mk d ⟶ SimplexCategory.mk n) : objEquiv.symm f ∈ (stdSimplex.obj (SimplexCategory.mk n)).nonDegenerate d ↔ CategoryTheory.Mono f

def SSet.stdSimplex.nonDegenerateEquiv {n d : ℕ} : ↑((stdSimplex.obj (SimplexCategory.mk n)).nonDegenerate d) ≃ (Fin (d + 1) ↪o Fin (n + 1))

Nondegenerate d-dimensional simplices of the standard simplex Δ[n] identify to order embeddings Fin (d + 1) ↪o Fin (n + 1).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SSet.stdSimplex.nonDegenerateEquiv_symm_apply_coe {n d : ℕ} (s : Fin (d + 1) ↪o Fin (n + 1)) : ↑(nonDegenerateEquiv.symm s) = objEquiv.symm (SimplexCategory.Hom.mk s.toOrderHom)

@[simp]

theorem SSet.stdSimplex.nonDegenerateEquiv_apply_apply {n d : ℕ} (s : ↑((stdSimplex.obj (SimplexCategory.mk n)).nonDegenerate d)) (a : Fin (d + 1)) : (nonDegenerateEquiv s) a = ↑s a

noncomputable def SSet.S1 : SSet

The simplicial circle.

Equations

• SSet.S1 = CategoryTheory.Limits.colimit (CategoryTheory.Limits.parallelPair (SSet.stdSimplex.δ 0) (SSet.stdSimplex.δ 1))

noncomputable def SSet.Augmented.stdSimplex : CategoryTheory.Functor SimplexCategory Augmented

The functor which sends ⦋n⦌ to the simplicial set Δ[n] equipped by the obvious augmentation towards the terminal object of the category of sets.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SSet.Augmented.stdSimplex_map_right {X✝ Y✝ : SimplexCategory} (θ : X✝ ⟶ Y✝) (a✝ : { left := SSet.stdSimplex.obj X✝, right := ⊤_ Type u, hom := { app := fun (x : SimplexCategoryᵒᵖ) => CategoryTheory.Limits.terminal.from (((CategoryTheory.Functor.id (CategoryTheory.SimplicialObject (Type u))).obj (SSet.stdSimplex.obj X✝)).obj x), naturality := ⋯ } }.right) : (stdSimplex.map θ).right a✝ = CategoryTheory.Limits.terminal.from { left := SSet.stdSimplex.obj X✝, right := ⊤_ Type u, hom := { app := fun (x : SimplexCategoryᵒᵖ) => CategoryTheory.Limits.terminal.from (((CategoryTheory.Functor.id (CategoryTheory.SimplicialObject (Type u))).obj (SSet.stdSimplex.obj X✝)).obj x), naturality := ⋯ } }.right a✝

@[simp]

theorem SSet.Augmented.stdSimplex_map_left {X✝ Y✝ : SimplexCategory} (θ : X✝ ⟶ Y✝) : (stdSimplex.map θ).left = SSet.stdSimplex.map θ

@[simp]

theorem SSet.Augmented.stdSimplex_obj_right (Δ : SimplexCategory) : (stdSimplex.obj Δ).right = ⊤_ Type u

@[simp]

theorem SSet.Augmented.stdSimplex_obj_hom_app (Δ : SimplexCategory) (x✝ : SimplexCategoryᵒᵖ) (a✝ : ((CategoryTheory.Functor.id (CategoryTheory.SimplicialObject (Type u))).obj (SSet.stdSimplex.obj Δ)).obj x✝) : (stdSimplex.obj Δ).hom.app x✝ a✝ = CategoryTheory.Limits.terminal.from (((CategoryTheory.Functor.id (CategoryTheory.SimplicialObject (Type u))).obj (SSet.stdSimplex.obj Δ)).obj x✝) a✝

@[simp]

theorem SSet.Augmented.stdSimplex_obj_left (Δ : SimplexCategory) : (stdSimplex.obj Δ).left = SSet.stdSimplex.obj Δ