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_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 ⋯

@[simp]

theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_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✝) (ℱ : 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 ℱ).val.map f✝ = ℱ.val.map ((Over.map f.as.unop).map f✝.unop).op

@[simp]

theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_val_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✝).val.app X = f✝.val.app (Opposite.op ((Over.map f.as.unop).obj (Opposite.unop X)))

@[simp]

theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_val_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).val.app X✝ = X.val.map ((Over.mapId (Opposite.unop x✝.as)).hom.app (Opposite.unop X✝)).op

@[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_mapId_hom_toNatTrans_app_val_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).val.app X✝ = X.val.map ((Over.mapId (Opposite.unop x✝.as)).inv.app (Opposite.unop X✝)).op

@[simp]

theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_val_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] (b : LocallyDiscrete Cᵒᵖ) (x✝ : Sheaf (J.over (Opposite.unop b.as)) A) (X : (Over (Opposite.unop b.as))ᵒᵖ) : (CategoryStruct.id x✝).val.app X = CategoryStruct.id (x✝.val.obj X)

@[simp]

theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_val_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] (b : LocallyDiscrete Cᵒᵖ) {X✝ Y✝ Z✝ : Sheaf (J.over (Opposite.unop b.as)) A} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) (X : (Over (Opposite.unop b.as))ᵒᵖ) : (CategoryStruct.comp f g).val.app X = CategoryStruct.comp (f.val.app X) (g.val.app X)

@[simp]

theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_val_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).val.app X✝ = X.val.map ((Over.mapComp x✝¹.as.unop x✝.as.unop).inv.app (Opposite.unop X✝)).op

@[simp]

theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_val_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).val.app X✝ = X.val.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_val_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✝) (ℱ : Sheaf (J.over (Opposite.unop X✝.as)) A) (X : (Over (Opposite.unop Y✝.as))ᵒᵖ) : (((J.pseudofunctorOver A).map f).toFunctor.obj ℱ).val.obj X = ℱ.val.obj (Opposite.op ((Over.map f.as.unop).obj (Opposite.unop X)))