Sheaves on Over categories, as a pseudofunctor

Given a Grothendieck topology J on a category C and a category A, we define the pseudofunctor J.pseudofunctorOver A : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat which sends X : C to the category of sheaves on Over X with values in A.

def CategoryTheory.GrothendieckTopology.pseudofunctorOver {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat

Given a Grothendieck topology J on a category C and a category A, this is the pseudofunctor which sends X : C to the categories of sheaves on Over X with values in A.

Equations

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] (b : LocallyDiscrete Cᵒᵖ) : ↑((J.pseudofunctorOver A).obj b) = Sheaf (J.over (Opposite.unop b.as)) A

@[simp]

theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_map {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] {X✝ Y✝ : LocallyDiscrete Cᵒᵖ} (f : X✝ ⟶ Y✝) (X : Sheaf (J.over (Opposite.unop X✝.as)) A) {X✝¹ Y✝¹ : (Over (Opposite.unop Y✝.as))ᵒᵖ} (f✝ : X✝¹ ⟶ Y✝¹) : (((J.pseudofunctorOver A).map f).toFunctor.obj X).obj.map f✝ = X.obj.map ((Over.map f.as.unop).map f✝.unop).op

@[simp]

theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_hom_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] (b : LocallyDiscrete Cᵒᵖ) {X Y Z : ObjectProperty.FullSubcategory (Presheaf.IsSheaf (J.over (Opposite.unop b.as)))} (a✝ : X ⟶ Y) (a✝¹ : Y ⟶ Z) (X✝ : (Over (Opposite.unop b.as))ᵒᵖ) : (CategoryStruct.comp a✝ a✝¹).hom.app X✝ = CategoryStruct.comp (a✝.hom.app X✝) (a✝¹.hom.app X✝)

@[simp]

theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_hom_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] (x✝ : LocallyDiscrete Cᵒᵖ) (X : Sheaf (J.over (Opposite.unop x✝.as)) A) (X✝ : (Over (Opposite.unop x✝.as))ᵒᵖ) : (((J.pseudofunctorOver A).mapId x✝).inv.toNatTrans.app X).hom.app X✝ = X.obj.map ((Over.mapId (Opposite.unop x✝.as)).hom.app (Opposite.unop X✝)).op

@[simp]

theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_hom_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] {a✝ b✝ c✝ : LocallyDiscrete Cᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) (X : Sheaf (J.over (Opposite.unop a✝.as)) A) (X✝ : (Over (Opposite.unop c✝.as))ᵒᵖ) : (((J.pseudofunctorOver A).mapComp x✝ x✝¹).hom.toNatTrans.app X).hom.app X✝ = X.obj.map ((Over.mapComp x✝¹.as.unop x✝.as.unop).inv.app (Opposite.unop X✝)).op

@[simp]

theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_hom_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] (b : LocallyDiscrete Cᵒᵖ) (X : ObjectProperty.FullSubcategory (Presheaf.IsSheaf (J.over (Opposite.unop b.as)))) (X✝ : (Over (Opposite.unop b.as))ᵒᵖ) : (CategoryStruct.id X).hom.app X✝ = CategoryStruct.id (X.obj.obj X✝)

@[simp]

theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_hom_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] (x✝ : LocallyDiscrete Cᵒᵖ) (X : Sheaf (J.over (Opposite.unop x✝.as)) A) (X✝ : (Over (Opposite.unop x✝.as))ᵒᵖ) : (((J.pseudofunctorOver A).mapId x✝).hom.toNatTrans.app X).hom.app X✝ = X.obj.map ((Over.mapId (Opposite.unop x✝.as)).inv.app (Opposite.unop X✝)).op

@[simp]

theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_hom_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] {X✝ Y✝ : LocallyDiscrete Cᵒᵖ} (f : X✝ ⟶ Y✝) {X✝¹ Y✝¹ : Sheaf (J.over (Opposite.unop X✝.as)) A} (f✝ : X✝¹ ⟶ Y✝¹) (X : (Over (Opposite.unop Y✝.as))ᵒᵖ) : (((J.pseudofunctorOver A).map f).toFunctor.map f✝).hom.app X = f✝.hom.app (Opposite.op ((Over.map f.as.unop).obj (Opposite.unop X)))

@[simp]

theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_hom_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] {a✝ b✝ c✝ : LocallyDiscrete Cᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) (X : Sheaf (J.over (Opposite.unop a✝.as)) A) (X✝ : (Over (Opposite.unop c✝.as))ᵒᵖ) : (((J.pseudofunctorOver A).mapComp x✝ x✝¹).inv.toNatTrans.app X).hom.app X✝ = X.obj.map ((Over.mapComp x✝¹.as.unop x✝.as.unop).hom.app (Opposite.unop X✝)).op

@[simp]

theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_obj {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] {X✝ Y✝ : LocallyDiscrete Cᵒᵖ} (f : X✝ ⟶ Y✝) (X : Sheaf (J.over (Opposite.unop X✝.as)) A) (X✝¹ : (Over (Opposite.unop Y✝.as))ᵒᵖ) : (((J.pseudofunctorOver A).map f).toFunctor.obj X).obj.obj X✝¹ = X.obj.obj (Opposite.op ((Over.map f.as.unop).obj (Opposite.unop X✝¹)))

@[simp]

theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂ {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] {a✝ b✝ : LocallyDiscrete Cᵒᵖ} {f✝ g✝ : a✝ ⟶ b✝} (φ : f✝ ⟶ g✝) : (J.pseudofunctorOver A).map₂ φ = eqToHom ⋯