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.5, 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.

@[implicit_reducible]

instance SSet.instInhabited : Inhabited SSet

Equations

• SSet.instInhabited = { default := SSet.stdSimplex.obj { len := 0 } }

@[implicit_reducible]

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

Equations

• SSet.instInhabitedTruncated = { default := (SSet.truncation n).obj (SSet.stdSimplex.obj { len := 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

@[implicit_reducible]

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

Equations

• SSet.stdSimplex.instDecidableEqObjOppositeSimplexCategory n m a b = decidable_of_iff (SSet.stdSimplex.objEquiv a = SSet.stdSimplex.objEquiv b) ⋯

@[implicit_reducible]

instance SSet.stdSimplex.instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat (n i : ℕ) : FunLike ((stdSimplex.obj { len := n }).obj (Opposite.op { len := 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 { len := n }).obj (Opposite.op { len := i })) : Monotone fun (j : Fin (i + 1)) => x j

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

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

@[simp]

theorem SSet.stdSimplex.objEquiv_toOrderHom_apply {n i : ℕ} (x : (stdSimplex.obj { len := n }).obj (Opposite.op { len := 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) = (CategoryTheory.ConcreteCategory.hom ((stdSimplex.map g).app m)) (objEquiv.symm f)

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

@[simp]

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

@[simp]

theorem SSet.stdSimplex.δ_objEquiv_symm_apply {n : ℕ} {m : SimplexCategory} (f : { len := n + 1 } ⟶ m) (i : Fin (n + 2)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (stdSimplex.obj m) i)) (objEquiv.symm f) = objEquiv.symm (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) f)

@[simp]

theorem SSet.stdSimplex.σ_objEquiv_symm_apply {n : ℕ} {m : SimplexCategory} (f : { len := n } ⟶ m) (i : Fin (n + 1)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ (stdSimplex.obj m) i)) (objEquiv.symm f) = objEquiv.symm (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ i) f)

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

theorem SSet.stdSimplex.objMk_bijective {n : SimplexCategory} {m : SimplexCategoryᵒᵖ} : Function.Bijective objMk

def SSet.stdSimplex.asOrderHom {n : ℕ} {m : SimplexCategoryᵒᵖ} (α : (stdSimplex.obj { len := 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₁) : (CategoryTheory.ConcreteCategory.hom ((stdSimplex.obj n).map f)) x = objEquiv.symm (CategoryTheory.CategoryStruct.comp f.unop (objEquiv x))

@[simp]

theorem SSet.stdSimplex.coe_asOrderHom_objEquiv_symm {n m : ℕ} (α : { len := n } ⟶ { len := m }) : ⇑(asOrderHom (objEquiv.symm α)) = ⇑(CategoryTheory.ConcreteCategory.hom α)

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

@[implicit_reducible]

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

Equations

• X.instDecidableEqHomObjSimplexCategoryStdSimplexOfOppositeOp n a b = decidable_of_iff (SSet.yonedaEquiv a = SSet.yonedaEquiv b) ⋯

@[simp]

theorem SSet.yonedaEquiv_symm_comp {X Y : SSet} {n : SimplexCategory} (x : X.obj (Opposite.op n)) (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (yonedaEquiv.symm x) f = yonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op n))) x)

theorem SSet.yonedaEquiv_const {X : SSet} (x : X.obj (Opposite.op { len := 0 })) : yonedaEquiv (const x) = x

@[simp]

theorem SSet.yonedaEquiv_symm_zero {X : SSet} (x : X.obj (Opposite.op { len := 0 })) : yonedaEquiv.symm x = const x

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

@[deprecated SSet.yonedaEquiv_map (since := "2026-03-21")]

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

Alias of SSet.yonedaEquiv_map.

@[simp]

theorem SSet.yonedaEquiv_symm_app {S : SSet} (n : SimplexCategory) (x : S.obj (Opposite.op n)) (α : (stdSimplex.obj n).obj (Opposite.op n)) : (CategoryTheory.ConcreteCategory.hom ((yonedaEquiv.symm x).app (Opposite.op n))) α = (CategoryTheory.ConcreteCategory.hom (S.map (stdSimplex.objEquiv α).op)) x

@[simp]

theorem SSet.yonedaEquiv_symm_stdSimplex_id (n : SimplexCategory) : yonedaEquiv.symm (stdSimplex.objEquiv.symm (CategoryTheory.CategoryStruct.id n)) = CategoryTheory.CategoryStruct.id (stdSimplex.obj n)

theorem SSet.yonedaEquiv_symm_app_objEquiv_symm {X : SSet} {n : SimplexCategory} (x : X.obj (Opposite.op n)) {m : SimplexCategoryᵒᵖ} (f : Opposite.unop m ⟶ n) : (CategoryTheory.ConcreteCategory.hom ((yonedaEquiv.symm x).app m)) (stdSimplex.objEquiv.symm f) = (CategoryTheory.ConcreteCategory.hom (X.map f.op)) x

@[simp]

theorem SSet.stdSimplex.objEquiv_yonedaEquiv_id (n : ℕ) : objEquiv (yonedaEquiv (CategoryTheory.CategoryStruct.id (stdSimplex.obj { len := n }))) = CategoryTheory.CategoryStruct.id { len := n }

theorem SSet.stdSimplex.map_objEquiv_op_apply {X : SSet} {n : SimplexCategory} (x : X.obj (Opposite.op n)) {m : SimplexCategoryᵒᵖ} (y : (stdSimplex.obj n).obj m) : (CategoryTheory.ConcreteCategory.hom (X.map (objEquiv y).op)) x = (CategoryTheory.ConcreteCategory.hom ((yonedaEquiv.symm x).app m)) y

def SSet.stdSimplex.const (n : ℕ) (k : Fin (n + 1)) (m : SimplexCategoryᵒᵖ) : (stdSimplex.obj { len := 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 { len := n }).obj (Opposite.op { len := 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 { len := n }).obj (Opposite.op { len := 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 { len := 0 })

theorem SSet.stdSimplex.δ_one_eq_const : stdSimplex.δ 1 = SSet.const (obj₀Equiv.symm 0)

theorem SSet.stdSimplex.δ_zero_eq_const : stdSimplex.δ 0 = SSet.const (obj₀Equiv.symm 1)

def SSet.stdSimplex.edge (n : ℕ) (a b : Fin (n + 1)) (hab : a ≤ b) : (stdSimplex.obj { len := n }).obj (Opposite.op { len := 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 { len := n }).obj (Opposite.op { len := 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 { len := 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 { len := 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 { len := n }).obj (Opposite.op { len := d })) : x ∈ (face S).obj (Opposite.op { len := 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₂)

@[simp]

theorem SSet.stdSimplex.face_empty (n : ℕ) : face ∅ = ⊥

@[simp]

theorem SSet.stdSimplex.face_univ (n : ℕ) : face Finset.univ = ⊤

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

@[simp]

theorem SSet.yonedaEquiv_symm_app_id {X : SSet} {n : ℕ} (x : X.obj (Opposite.op { len := n })) : (CategoryTheory.ConcreteCategory.hom ((yonedaEquiv.symm x).app (Opposite.op { len := n }))) (yonedaEquiv (CategoryTheory.CategoryStruct.id (stdSimplex.obj { len := n }))) = x

theorem SSet.Subcomplex.range_eq_ofSimplex {X : SSet} {n : ℕ} (f : stdSimplex.obj { len := 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 { len := 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 { len := 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 { len := m }) : stdSimplex.obj { len := 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)) : Subcomplex.range (stdSimplex.δ i) = face {i}ᶜ

def SSet.stdSimplex.isoNerve (n : ℕ) : stdSimplex.obj { len := 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 { len := n }).obj (Opposite.op { len := d })) (i : Fin (d + 1)) : ((CategoryTheory.ConcreteCategory.hom ((isoNerve.{u} n).hom.app (Opposite.op { len := 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 { len := d })) (i : Fin (d + 1)) : ((CategoryTheory.ConcreteCategory.hom ((isoNerve.{u} n).inv.app (Opposite.op { len := d }))) F) i = (F.obj i).down

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

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

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

def SSet.stdSimplex.nonDegenerateEquiv {n d : ℕ} : ↑((stdSimplex.obj { len := 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_apply_apply {n d : ℕ} (s : ↑((stdSimplex.obj { len := n }).nonDegenerate d)) (a : Fin (d + 1)) : (nonDegenerateEquiv s) a = ↑s a

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

instance SSet.stdSimplex.instHasDimensionLEObjSimplexCategoryMk (n : ℕ) : (stdSimplex.obj { len := 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.

Equations

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

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 { len := n } ≅ (face {i}ᶜ).toSSet

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

Equations

• SSet.stdSimplex.faceSingletonComplIso i = SSet.stdSimplex.isoOfRepresentableBy (SSet.stdSimplex.faceRepresentableBy {i}ᶜ n (SSet.stdSimplex.finSuccAboveOrderIsoFinset i))

@[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 { len := 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 { len := 0 } ≅ (face {i}).toSSet

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

Equations

• SSet.stdSimplex.faceSingletonIso i = SSet.stdSimplex.isoOfRepresentableBy (SSet.stdSimplex.faceRepresentableBy {i} 0 (Fin.orderIsoSingleton 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 { len := 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 { len := 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 { len := 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}.

Equations

• SSet.stdSimplex.facePairIso i j hij = SSet.stdSimplex.isoOfRepresentableBy (SSet.stdSimplex.faceRepresentableBy {i, j} 1 (Fin.orderIsoPair i j hij))

noncomputable def SSet.stdSimplex.nonDegenerateEquiv' {n d : ℕ} : ↑((stdSimplex.obj { len := n }).nonDegenerate d) ≃ ↑{S : Finset (Fin (n + 1)) | S.card = d + 1}

Nondegenerate d-dimensional simplices of the standard simplex Δ[n] identify to subsets of Fin (n + 1) of cardinality d + 1.

Equations

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

theorem SSet.stdSimplex.nonDegenerateEquiv'_iff {n d : ℕ} (x : ↑((stdSimplex.obj { len := n }).nonDegenerate d)) (j : Fin (n + 1)) : j ∈ ↑(nonDegenerateEquiv' x) ↔ ∃ (i : Fin (d + 1)), ↑x i = j

noncomputable def SSet.stdSimplex.orderIsoOfNonDegenerate {n d : ℕ} (x : ↑((stdSimplex.obj { len := n }).nonDegenerate d)) : Fin (d + 1) ≃o ↥↑(nonDegenerateEquiv' x)

If x is a nondegenerate d-simplex of Δ[n], this is the order isomorphism between Fin (d + 1) and the corresponding subset of Fin (n + 1) of cardinality d + 1.

Equations

• SSet.stdSimplex.orderIsoOfNonDegenerate x = { toEquiv := Equiv.ofBijective (fun (i : Fin (d + 1)) => ⟨↑x i, ⋯⟩) ⋯, map_rel_iff' := ⋯ }

theorem SSet.stdSimplex.face_nonDegenerateEquiv' {n d : ℕ} (x : ↑((stdSimplex.obj { len := n }).nonDegenerate d)) : face ↑(nonDegenerateEquiv' x) = Subcomplex.ofSimplex ↑x

theorem SSet.stdSimplex.nonDegenerateEquiv'_symm_apply_mem {n d : ℕ} (S : ↑{S : Finset (Fin (n + 1)) | S.card = d + 1}) (i : Fin (d + 1)) : ↑(nonDegenerateEquiv'.symm S) i ∈ ↑S

theorem SSet.stdSimplex.nonDegenerateEquiv'_symm_mem_iff_face_le {n d : ℕ} (S : ↑{S : Finset (Fin (n + 1)) | S.card = d + 1}) (A : (stdSimplex.obj { len := n }).Subcomplex) : ↑(nonDegenerateEquiv'.symm S) ∈ A.obj (Opposite.op { len := d }) ↔ face ↑S ≤ A

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 { len := n })) : (Subcomplex.ofSimplex x).toSSet.Finite

theorem SSet.stdSimplex.hasDimensionLT_face {n : ℕ} (S : Finset (Fin (n + 1))) (d : ℕ) (hd : S.card ≤ d) : (face S).toSSet.HasDimensionLT d

theorem SSet.stdSimplex.ofSimplex_objEquiv_symm_id (n : ℕ) : Subcomplex.ofSimplex (objEquiv.symm (CategoryTheory.CategoryStruct.id { len := n })) = ⊤

theorem SSet.stdSimplex.objEquiv_symm_id_mem_nonDegenerate (n : ℕ) : objEquiv.symm (CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op { len := n }))) ∈ (stdSimplex.obj { len := n }).nonDegenerate n

theorem SSet.stdSimplex.nonDegenerate_top_dim (n : ℕ) : (stdSimplex.obj { len := n }).nonDegenerate n = {objEquiv.symm (CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op { len := n })))}

theorem SSet.stdSimplex.not_hasDimensionLT (n : ℕ) : autoParam ((stdSimplex.obj { len := n }).HasDimensionLT n) not_hasDimensionLT._auto_1 → False

def SSet.stdSimplex.opObjEquiv {n : SimplexCategory} {d : SimplexCategoryᵒᵖ} : (stdSimplex.obj n).op.obj d ≃ (stdSimplex.obj n).obj d

The bijection (stdSimplex.obj n).op.obj d ≃ (stdSimplex.obj n).obj d for any n : ℕ and d : ℕ. See also stdSimplex.opIso.

Equations

• SSet.stdSimplex.opObjEquiv = SSet.opObjEquiv.trans (SSet.stdSimplex.objEquiv.trans (SimplexCategory.revEquivalence.fullyFaithfulFunctor.homEquiv.trans SSet.stdSimplex.objEquiv.symm))

theorem SSet.stdSimplex.opObjEquiv_apply {d n : ℕ} (f : (stdSimplex.obj { len := n }).op.obj (Opposite.op { len := d })) (i : Fin (d + 1)) : (stdSimplex.opObjEquiv f) i = ((opObjEquiv f) i.rev).rev

theorem SSet.stdSimplex.opObjEquiv_opObjEquiv_symm_apply {d n : ℕ} (f : (stdSimplex.obj { len := n }).obj (Opposite.op { len := d })) (i : Fin (d + 1)) : (opObjEquiv (stdSimplex.opObjEquiv.symm f)) i = (f i.rev).rev

theorem SSet.stdSimplex.map_rev_map_op_apply {n d d' : ℕ} (f : { len := d } ⟶ { len := d' }) (g : (stdSimplex.obj { len := n }).obj (Opposite.op { len := d' })) (i : Fin (d + 1)) : ((CategoryTheory.ConcreteCategory.hom ((stdSimplex.obj { len := n }).map (SimplexCategory.rev.map f).op)) g) i = g ((CategoryTheory.ConcreteCategory.hom f) i.rev).rev

def SSet.stdSimplex.opIso (n : SimplexCategory) : (stdSimplex.obj n).op ≅ stdSimplex.obj n

The opposite of Δ[n] is isomorphic to Δ[n].

Equations

• SSet.stdSimplex.opIso n = CategoryTheory.NatIso.ofComponents (fun (d : SimplexCategoryᵒᵖ) => SSet.stdSimplex.opObjEquiv.toIso) ⋯

@[simp]

theorem SSet.stdSimplex.opIso_inv_app_hom_apply (n : SimplexCategory) (X : SimplexCategoryᵒᵖ) (x : (stdSimplex.obj n).obj X) : (CategoryTheory.ConcreteCategory.hom ((opIso n).inv.app X)) x = stdSimplex.opObjEquiv.symm x

@[simp]

theorem SSet.stdSimplex.opIso_hom_app_hom_apply (n : SimplexCategory) (X : SimplexCategoryᵒᵖ) (x : (stdSimplex.obj n).op.obj X) : (CategoryTheory.ConcreteCategory.hom ((opIso n).hom.app X)) x = stdSimplex.opObjEquiv x

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_obj_hom_app (Δ : SimplexCategory) (x✝ : SimplexCategoryᵒᵖ) : (stdSimplex.obj Δ).hom.app x✝ = CategoryTheory.Limits.terminal.from (((CategoryTheory.Functor.id (CategoryTheory.SimplicialObject (Type u))).obj (SSet.stdSimplex.obj Δ)).obj x✝)

@[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✝) : (stdSimplex.map θ).right = 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

@[simp]

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

@[simp]

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