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).

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).

instance SSet.instInhabited : Inhabited SSet

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

@[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.

instance SSet.stdSimplex.instDecidableEqObjOppositeSimplexCategory (n : SimplexCategory) (m : SimplexCategoryᵒᵖ) : DecidableEq ((stdSimplex.obj n).obj m)

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).

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.

@[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).

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).

instance SSet.stdSimplex.instDecidableEqHomObjSimplexCategoryOfOppositeOp (X : SSet) (n : SimplexCategory) [DecidableEq (X.obj (Opposite.op n))] : DecidableEq (stdSimplex.obj n ⟶ X)

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.

@[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).

@[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))

@[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

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.

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.

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.

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) : 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.obj₀Equiv_symm_mem_face_iff {n : ℕ} (S : Finset (Fin (n + 1))) (i : Fin (n + 1)) : obj₀Equiv.symm i ∈ (face S).obj (Opposite.op (SimplexCategory.mk 0)) ↔ i ∈ S

theorem SSet.stdSimplex.face_le_face_iff {n : ℕ} (S₁ S₂ : Finset (Fin (n + 1))) : face S₁ ≤ face S₂ ↔ S₁ ≤ S₂

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.

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.

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)) : Subcomplex.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)).

@[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).

@[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

instance SSet.stdSimplex.instHasDimensionLEObjSimplexCategoryMk (n : ℕ) : (stdSimplex.obj (SimplexCategory.mk n)).HasDimensionLE n

def SSet.stdSimplex.finSuccAboveOrderIsoFinset {n : ℕ} (i : Fin (n + 2)) : Fin (n + 1) ≃o ↥{i}ᶜ

If i : Fin (n + 2), this is the order isomorphism between Fin (n +1) and the complement of {i} as a finset.

theorem SSet.stdSimplex.face_singleton_compl {n : ℕ} (i : Fin (n + 2)) : face {i}ᶜ = Subcomplex.ofSimplex (objEquiv.symm (SimplexCategory.δ i))

def SSet.stdSimplex.faceSingletonComplIso {n : ℕ} (i : Fin (n + 2)) : stdSimplex.obj (SimplexCategory.mk n) ≅ (face {i}ᶜ).toSSet

In Δ[n + 1], the face corresponding to the complement of {i} for i : Fin (n + 2) is isomorphic to Δ[n].

@[simp]

theorem SSet.stdSimplex.faceSingletonComplIso_hom_ι {n : ℕ} (i : Fin (n + 2)) : CategoryTheory.CategoryStruct.comp (faceSingletonComplIso i).hom (face {i}ᶜ).ι = stdSimplex.δ i

@[simp]

theorem SSet.stdSimplex.faceSingletonComplIso_hom_ι_assoc {n : ℕ} (i : Fin (n + 2)) {Z : SSet} (h : stdSimplex.obj (SimplexCategory.mk (n + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (faceSingletonComplIso i).hom (CategoryTheory.CategoryStruct.comp (face {i}ᶜ).ι h) = CategoryTheory.CategoryStruct.comp (stdSimplex.δ i) h

noncomputable def SSet.stdSimplex.faceSingletonIso {n : ℕ} (i : Fin (n + 1)) : stdSimplex.obj (SimplexCategory.mk 0) ≅ (face {i}).toSSet

Given i : Fin (n + 1), this is the isomorphism from Δ[0] to the face of Δ[n] corresponding to {i}.

theorem SSet.stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ : CategoryTheory.CategoryStruct.comp (faceSingletonIso 0).hom (face {0}).ι = stdSimplex.δ 1

theorem SSet.stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ_assoc {Z : SSet} (h : stdSimplex.obj (SimplexCategory.mk 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (faceSingletonIso 0).hom (CategoryTheory.CategoryStruct.comp (face {0}).ι h) = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) h

theorem SSet.stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ : CategoryTheory.CategoryStruct.comp (faceSingletonIso 1).hom (face {1}).ι = stdSimplex.δ 0

theorem SSet.stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ_assoc {Z : SSet} (h : stdSimplex.obj (SimplexCategory.mk 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (faceSingletonIso 1).hom (CategoryTheory.CategoryStruct.comp (face {1}).ι h) = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) h

noncomputable def SSet.stdSimplex.facePairIso {n : ℕ} (i j : Fin (n + 1)) (hij : i < j) : stdSimplex.obj (SimplexCategory.mk 1) ≅ (face {i, j}).toSSet

Given i and j in Fin (n + 1) such that i < j, this is the isomorphism from Δ[1] to the face of Δ[n] corresponding to {i, j}.

instance SSet.stdSimplex.instFiniteObjOppositeSimplexCategory (n : SimplexCategory) (d : SimplexCategoryᵒᵖ) : Finite ((stdSimplex.obj n).obj d)

instance SSet.stdSimplex.instFiniteObjSimplexCategory (n : SimplexCategory) : (stdSimplex.obj n).Finite

instance SSet.stdSimplex.instFiniteToSSetOfSimplex {X : SSet} {n : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk n))) : (Subcomplex.ofSimplex x).toSSet.Finite

noncomputable def SSet.S1 : SSet

The simplicial circle.

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.

@[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_map_left {X✝ Y✝ : SimplexCategory} (θ : X✝ ⟶ Y✝) : (stdSimplex.map θ).left = SSet.stdSimplex.map θ

@[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_obj_left (Δ : SimplexCategory) : (stdSimplex.obj Δ).left = SSet.stdSimplex.obj Δ

@[simp]

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