The covariant involution of the category of simplicial sets

In this file, we define the covariant involution opFunctor : SSet ⥤ SSet of the category of simplicial sets that is induced by the covariant involution SimplexCategory.op : SimplexCategory ⥤ SimplexCategory. We use an abbreviation X.op for opFunctor.obj X.

TODO

• Show that this involution sends Δ[n] to itself, and that via this identification, the horn horn n i is sent to horn n i.rev (@joelriou)
• Construct an isomorphism nerve Cᵒᵖ ≅ (nerve C).op (@robin-carlier)
• Show that the topological realization of X.op identifies to the topological realization of X (@joelriou)

def SSet.opFunctor : CategoryTheory.Functor SSet SSet

The covariant involution of the category of simplicial sets that is induced by SimplexCategory.rev : SimplexCategory ⥤ SimplexCategory.

Equations

• SSet.opFunctor = SimplicialObject.opFunctor

@[reducible, inline]

abbrev SSet.op (X : SSet) : SSet

The image of a simplicial set by the involution opFunctor : SSet ⥤ SSet.

Equations

• X.op = SSet.opFunctor.obj X

def SSet.opObjEquiv {X : SSet} {n : SimplexCategoryᵒᵖ} : X.op.obj n ≃ X.obj n

The type of n-simplices of X.op identify to type of n-simplices of X.

Equations

• SSet.opObjEquiv = Equiv.refl (X.op.obj n)

theorem SSet.opFunctor_map {X Y : SSet} (f : X ⟶ Y) {n : SimplexCategoryᵒᵖ} (x : X.op.obj n) : (opFunctor.map f).app n x = opObjEquiv.symm (f.app n (opObjEquiv x))

theorem SSet.op_map (X : SSet) {n m : SimplexCategoryᵒᵖ} (f : n ⟶ m) (x : X.op.obj n) : X.op.map f x = opObjEquiv.symm (X.map (SimplexCategory.rev.map f.unop).op (opObjEquiv x))

@[simp]

theorem SSet.op_δ (X : SSet) {n : ℕ} (i : Fin (n + 2)) (x : X.obj (Opposite.op (SimplexCategory.mk (n + 1)))) : CategoryTheory.SimplicialObject.δ X.op i x = opObjEquiv.symm (CategoryTheory.SimplicialObject.δ X i.rev (opObjEquiv x))

@[simp]

theorem SSet.op_σ (X : SSet) {n : ℕ} (i : Fin (n + 1)) (x : X.obj (Opposite.op (SimplexCategory.mk n))) : CategoryTheory.SimplicialObject.σ X.op i x = opObjEquiv.symm (CategoryTheory.SimplicialObject.σ X i.rev (opObjEquiv x))

def SSet.opFunctorCompOpFunctorIso : opFunctor.comp opFunctor ≅ CategoryTheory.Functor.id SSet

The functor opFunctor : SSet ⥤ SSet is an involution.

Equations

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

@[simp]

theorem SSet.opFunctorCompOpFunctorIso_hom_app_app (X : SSet) (X✝ : SimplexCategoryᵒᵖ) (a✝ : ((opFunctor.comp opFunctor).obj X).obj X✝) : (opFunctorCompOpFunctorIso.hom.app X).app X✝ a✝ = opObjEquiv (opObjEquiv a✝)

@[simp]

theorem SSet.opFunctorCompOpFunctorIso_inv_app_app (X : SSet) (X✝ : SimplexCategoryᵒᵖ) (a✝ : ((CategoryTheory.Functor.id SSet).obj X).obj X✝) : (opFunctorCompOpFunctorIso.inv.app X).app X✝ a✝ = opObjEquiv.symm (opObjEquiv.symm a✝)

def SSet.opEquivalence : SSet ≌ SSet

The covariant involution opFunctor : SSet ⥤ SSet, as an equivalence of categories.

Equations

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

@[simp]

theorem SSet.opEquivalence_unitIso : opEquivalence.unitIso = opFunctorCompOpFunctorIso.symm

@[simp]

theorem SSet.opEquivalence_functor : opEquivalence.functor = opFunctor

@[simp]

theorem SSet.opEquivalence_inverse : opEquivalence.inverse = opFunctor

@[simp]

theorem SSet.opEquivalence_counitIso : opEquivalence.counitIso = opFunctorCompOpFunctorIso