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) : (CategoryTheory.ConcreteCategory.hom ((opFunctor.map f).app n)) x = opObjEquiv.symm ((CategoryTheory.ConcreteCategory.hom (f.app n)) (opObjEquiv x))

theorem SSet.op_map (X : SSet) {n m : SimplexCategoryᵒᵖ} (f : n ⟶ m) (x : X.op.obj n) : (CategoryTheory.ConcreteCategory.hom (X.op.map f)) x = opObjEquiv.symm ((CategoryTheory.ConcreteCategory.hom (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 { len := n + 1 })) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X.op i)) x = opObjEquiv.symm ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X i.rev)) (opObjEquiv x))

@[simp]

theorem SSet.op_σ (X : SSet) {n : ℕ} (i : Fin (n + 1)) (x : X.obj (Opposite.op { len := n })) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ X.op i)) x = opObjEquiv.symm ((CategoryTheory.ConcreteCategory.hom (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_inv_app_app_hom_apply (X : SSet) (X✝ : SimplexCategoryᵒᵖ) (x : X.obj X✝) : (CategoryTheory.ConcreteCategory.hom ((opFunctorCompOpFunctorIso.inv.app X).app X✝)) x = opObjEquiv.symm (opObjEquiv.symm x)

@[simp]

theorem SSet.opFunctorCompOpFunctorIso_hom_app_app_hom_apply (X : SSet) (X✝ : SimplexCategoryᵒᵖ) (x : (opFunctor.obj (opFunctor.obj X)).obj X✝) : (CategoryTheory.ConcreteCategory.hom ((opFunctorCompOpFunctorIso.hom.app X).app X✝)) x = opObjEquiv (opObjEquiv x)

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_inverse : opEquivalence.inverse = opFunctor

@[simp]

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

@[simp]

theorem SSet.opEquivalence_counitIso : opEquivalence.counitIso = opFunctorCompOpFunctorIso

@[simp]

theorem SSet.opEquivalence_functor : opEquivalence.functor = opFunctor