theorem SSet.map_yonedaEquiv {n m : ℕ} {X : SSet} (f : { len := n } ⟶ { len := m }) (g : stdSimplex.obj { len := m } ⟶ X) : (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (yonedaEquiv g) = (CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op { len := 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 : { len := m } ⟶ { len := n }} {σ : X.obj (Opposite.op { len := n })} {s : { len := n } ⟶ { len := k }} {g : stdSimplex.obj { len := k } ⟶ X} (h : yonedaEquiv.symm σ = CategoryTheory.CategoryStruct.comp (stdSimplex.map s) g) : (CategoryTheory.ConcreteCategory.hom (X.map f.op)) σ = (CategoryTheory.ConcreteCategory.hom (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 : { len := m } ⟶ { len := n }) {g : stdSimplex.obj { len := n } ⟶ X} : yonedaEquiv (CategoryTheory.CategoryStruct.comp (stdSimplex.map f) g) = (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (yonedaEquiv g)

A variant of map_yonedaEquiv.

theorem SSet.push_yonedaEquiv' {n m : ℕ} {X : SSet} {f : { len := m } ⟶ { len := n }} {σ : X.obj (Opposite.op { len := m })} {g : stdSimplex.obj { len := n } ⟶ X} (h : yonedaEquiv.symm σ = CategoryTheory.CategoryStruct.comp (stdSimplex.map f) g) : σ = (CategoryTheory.ConcreteCategory.hom (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 : { len := n } ⟶ { len := m }) (s : X.obj (Opposite.op { len := m })) : CategoryTheory.CategoryStruct.comp (stdSimplex.map f) (yonedaEquiv.symm s) = yonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (X.map f.op)) s)

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

theorem SSet.yonedaEquiv_naturality {X : SSet} {m n : SimplexCategory} (f : m ⟶ n) (g : stdSimplex.obj n ⟶ X) : (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (yonedaEquiv g) = yonedaEquiv (CategoryTheory.CategoryStruct.comp (stdSimplex.map f) g)

yonedaEquiv is natural.

theorem SSet.yonedaEquiv_symm_naturality {X : SSet} {m n : SimplexCategory} (f : m ⟶ n) (g : X.obj (Opposite.op n)) : CategoryTheory.CategoryStruct.comp (stdSimplex.map f) (yonedaEquiv.symm g) = yonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (X.map f.op)) g)

yonedaEquiv.symm is natural