theorem SSet.map_yonedaEquiv {n m : ℕ} {X : SSet} (f : SimplexCategory.mk n ⟶ SimplexCategory.mk m) (g : stdSimplex.obj (SimplexCategory.mk m) ⟶ X) : X.map f.op (yonedaEquiv g) = g.app (Opposite.op (SimplexCategory.mk n)) (stdSimplex.objEquiv.symm f)

A variant of CategoryTheory.map_yonedaEquiv specialized to simplicial sets.

theorem SSet.push_yonedaEquiv {n m k : ℕ} {X : SSet} {f : SimplexCategory.mk m ⟶ SimplexCategory.mk n} {σ : X.obj (Opposite.op (SimplexCategory.mk n))} {s : SimplexCategory.mk n ⟶ SimplexCategory.mk k} {g : stdSimplex.obj (SimplexCategory.mk k) ⟶ X} (h : yonedaEquiv.symm σ = CategoryTheory.CategoryStruct.comp (stdSimplex.map s) g) : X.map f.op σ = X.map (CategoryTheory.CategoryStruct.comp f s).op (yonedaEquiv g)

If a simplex σ of a simplicial set X is equivalent to a composition stdSimplex.map s ≫ g then we can pull the stdSimplex.map s out from under an application of any X.map f.op.

theorem SSet.map_yonedaEquiv' {n m : ℕ} {X : SSet} (f : SimplexCategory.mk m ⟶ SimplexCategory.mk n) {g : stdSimplex.obj (SimplexCategory.mk n) ⟶ X} : yonedaEquiv (CategoryTheory.CategoryStruct.comp (stdSimplex.map f) g) = X.map f.op (yonedaEquiv g)

A variant of map_yonedaEquiv.

theorem SSet.push_yonedaEquiv' {n m : ℕ} {X : SSet} {f : SimplexCategory.mk m ⟶ SimplexCategory.mk n} {σ : X.obj (Opposite.op (SimplexCategory.mk m))} {g : stdSimplex.obj (SimplexCategory.mk n) ⟶ X} (h : yonedaEquiv.symm σ = CategoryTheory.CategoryStruct.comp (stdSimplex.map f) g) : σ = X.map f.op (yonedaEquiv g)

A specialization of push_yonedaEquiv to the case where f is the identity.

theorem SSet.map_comp_yonedaEquiv_symm {n m : ℕ} {X : SSet} (f : SimplexCategory.mk n ⟶ SimplexCategory.mk m) (s : X.obj (Opposite.op (SimplexCategory.mk m))) : CategoryTheory.CategoryStruct.comp (stdSimplex.map f) (yonedaEquiv.symm s) = yonedaEquiv.symm (X.map f.op s)

Another version of map_yonedaEquiv, but at the level of functions Δ[n] ⟶ X.