Documentation

Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver

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.

source
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.
Instances For
    source
    @[simp]
    theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_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).map f✝).val.app X = f✝.val.app (Opposite.op ((Over.map f.as.unop).obj (Opposite.unop X)))
    source
    @[simp]
    theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_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).obj ℱ).val.map f✝ = ℱ.val.map ((Over.map f.as.unop).map f✝.unop).op
    source
    @[simp]
    theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_inv_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.app X).val.app X✝ = X.val.map ((Over.mapId (Opposite.unop x✝.as)).hom.app (Opposite.unop X✝)).op
    source
    @[simp]
    theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_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).obj ℱ).val.obj X = ℱ.val.obj (Opposite.op ((Over.map f.as.unop).obj (Opposite.unop X)))
    source
    @[simp]
    theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_hom_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.app X).val.app X✝ = X.val.map ((Over.mapId (Opposite.unop x✝.as)).inv.app (Opposite.unop X✝)).op
    source
    @[simp]
    theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_hom_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.app X).val.app X✝ = X.val.map ((Over.mapComp x✝¹.as.unop x✝.as.unop).inv.app (Opposite.unop X✝)).op
    source
    @[simp]
    theorem CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_inv_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.app X).val.app X✝ = X.val.map ((Over.mapComp x✝¹.as.unop x✝.as.unop).hom.app (Opposite.unop X✝)).op
    source
    @[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
    source
    @[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)
    source
    @[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)
    source
    @[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 ⋯