The covariant involution of the category of simplicial objects

In this file, we define the covariant involution SimplicialObject.opFunctor of the category of simplicial objects that is induced by the covariant involution SimplexCategory.rev : SimplexCategory ⥤ SimplexCategory.

def SimplicialObject.opFunctor {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] : CategoryTheory.Functor (CategoryTheory.SimplicialObject C) (CategoryTheory.SimplicialObject C)

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

def SimplicialObject.opObjIso {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] {X : CategoryTheory.SimplicialObject C} {n : SimplexCategoryᵒᵖ} : (opFunctor.obj X).obj n ≅ X.obj n

The isomorphism (opFunctor.obj X).obj n ≅ X.obj n when X is a simplicial object.

@[simp]

theorem SimplicialObject.opFunctor_map_app {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) (n : SimplexCategoryᵒᵖ) : (opFunctor.map f).app n = CategoryTheory.CategoryStruct.comp opObjIso.hom (CategoryTheory.CategoryStruct.comp (f.app n) opObjIso.inv)

@[simp]

theorem SimplicialObject.opFunctor_obj_map {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] (X : CategoryTheory.SimplicialObject C) {n m : SimplexCategoryᵒᵖ} (f : n ⟶ m) : (opFunctor.obj X).map f = CategoryTheory.CategoryStruct.comp opObjIso.hom (CategoryTheory.CategoryStruct.comp (X.map (SimplexCategory.rev.map f.unop).op) opObjIso.inv)

@[simp]

theorem SimplicialObject.opFunctor_obj_δ {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} (i : Fin (n + 2)) : (opFunctor.obj X).δ i = CategoryTheory.CategoryStruct.comp opObjIso.hom (CategoryTheory.CategoryStruct.comp (X.δ i.rev) opObjIso.inv)

@[simp]

theorem SimplicialObject.opFunctor_obj_σ {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} (i : Fin (n + 1)) : (opFunctor.obj X).σ i = CategoryTheory.CategoryStruct.comp opObjIso.hom (CategoryTheory.CategoryStruct.comp (X.σ i.rev) opObjIso.inv)

def SimplicialObject.opFunctorCompOpFunctorIso {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] : opFunctor.comp opFunctor ≅ CategoryTheory.Functor.id (CategoryTheory.SimplicialObject C)

The functor opFunctor : SimplicialObject C ⥤ SimplicialObject C is a covariant involution.

@[simp]

theorem SimplicialObject.opFunctorCompOpFunctorIso_hom_app_app {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] (X : CategoryTheory.SimplicialObject C) (n : SimplexCategoryᵒᵖ) : (opFunctorCompOpFunctorIso.hom.app X).app n = CategoryTheory.CategoryStruct.comp opObjIso.hom opObjIso.hom

@[simp]

theorem SimplicialObject.opFunctorCompOpFunctorIso_inv_app_app {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] (X : CategoryTheory.SimplicialObject C) (n : SimplexCategoryᵒᵖ) : (opFunctorCompOpFunctorIso.inv.app X).app n = CategoryTheory.CategoryStruct.comp opObjIso.inv opObjIso.inv

def SimplicialObject.opEquivalence {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] : CategoryTheory.SimplicialObject C ≌ CategoryTheory.SimplicialObject C

The functor opFunctor : SimplicialObject C ⥤ SimplicialObject C as an equivalence of categories.

@[simp]

theorem SimplicialObject.opEquivalence_functor {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] : opEquivalence.functor = opFunctor

@[simp]

theorem SimplicialObject.opEquivalence_counitIso {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] : opEquivalence.counitIso = opFunctorCompOpFunctorIso

@[simp]

theorem SimplicialObject.opEquivalence_inverse {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] : opEquivalence.inverse = opFunctor

@[simp]

theorem SimplicialObject.opEquivalence_unitIso {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] : opEquivalence.unitIso = opFunctorCompOpFunctorIso.symm