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. This functor is purposely not made implicit_reducible so as to avoid confusion between (opFunctor.obj X) _⦋n⦌ and X _⦋n⦌: use the isomorphism opObjIso.

Equations

• SimplicialObject.opFunctor = (CategoryTheory.Functor.whiskeringLeft SimplexCategoryᵒᵖ SimplexCategoryᵒᵖ C).obj SimplexCategory.rev.op

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.

Equations

• SimplicialObject.opObjIso = CategoryTheory.Iso.refl ((SimplicialObject.opFunctor.obj X).obj n)

@[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.

Equations

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

@[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.

Equations

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

@[simp]

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

@[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_functor {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] : opEquivalence.functor = opFunctor