Properties of objects in target categories of a pseudofunctor to Cat

Given F : Pseudofunctor B Cat, we introduce a type F.ObjectProperty which consists of properties P of objects for all categories F.obj X for X : B. The typeclass P.IsClosedUnderMapObj expresses that this property is preserved by the application of the functors F.map: this allows to define a sub-pseudofunctor P.fullsubcategory : Pseudofunctor B Cat.

TODO (@joelriou)

• Given a Grothendieck topology J on a category C, define a type class Pseudofunctor.ObjectProperty.IsLocal P J extending IsClosedUnderMapObj saying that if an object locally satisfies the property, then it satisfies the property. Assuming this, show that P.fullsubcategory is a stack if the original pseudofunctor was.

structure CategoryTheory.Pseudofunctor.ObjectProperty {B : Type u} [Bicategory B] (F : Pseudofunctor B Cat) : Type (max u u')

If F : Pseudofunctor B Cat, this is the data of a property of objects in all categories F.obj X for X : B.

• prop (X : B) : ObjectProperty ↑(F.obj X)

  A property of objects in the category F.obj X for all X : B.

@[reducible, inline]

abbrev CategoryTheory.Pseudofunctor.ObjectProperty.Obj {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) (X : B) : Type u'

Given F : Pseudofunctor B Cat, P : F.ObjectProperty and X : B, this is the full subcategory of F.obj X consisting of the objects satisfying the property P.

class CategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderMapObj {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) : Prop

If P is a property of objects for a pseudofunctor F to Cat, this is the condition that P is preserved by the application of the functors F.obj.

• map_obj {X Y : B} {M : ↑(F.obj X)} (hM : P.prop X M) (f : X ⟶ Y) : P.prop Y ((F.map f).toFunctor.obj M)

class CategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderIsomorphisms {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) : Prop

If P is a property of objects for a pseudofunctor F to Cat, this is the condition that all P.prop : ObjectProperty (F.obj X) for X : B are closed under isomorphisms.

• isClosedUnderIsomorphisms (X : B) : (P.prop X).IsClosedUnderIsomorphisms

def CategoryTheory.Pseudofunctor.ObjectProperty.map {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] {X Y : B} (f : X ⟶ Y) : Functor (P.Obj X) (P.Obj Y)

Given a property P of objects for F : Pseudofunctor B Cat and a morphism f : X ⟶ Y in B, this is the functor P.Obj X ⥤ P.Obj Y that is induced by F.map f.

@[simp]

theorem CategoryTheory.Pseudofunctor.ObjectProperty.map_map_hom {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] {X Y : B} (f : X ⟶ Y) {X✝ Y✝ : P.Obj X} (f✝ : X✝ ⟶ Y✝) : ((P.map f).map f✝).hom = (F.map f).toFunctor.map f✝.hom

@[simp]

theorem CategoryTheory.Pseudofunctor.ObjectProperty.map_obj_obj {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] {X Y : B} (f : X ⟶ Y) (X✝ : P.Obj X) : ((P.map f).obj X✝).obj = (F.map f).toFunctor.obj X✝.obj

def CategoryTheory.Pseudofunctor.ObjectProperty.map₂ {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] {X Y : B} {f g : X ⟶ Y} (α : f ⟶ g) : P.map f ⟶ P.map g

Given a property P of objects for F : Pseudofunctor B Cat and a 2-morphism in B, this is the induced natural transformation between the induced functors on the fullsubcategories of objects satisfying P.

@[simp]

theorem CategoryTheory.Pseudofunctor.ObjectProperty.map₂_app_hom {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] {X Y : B} {f g : X ⟶ Y} (α : f ⟶ g) (X✝ : P.Obj X) : ((P.map₂ α).app X✝).hom = (F.map₂ α).toNatTrans.app X✝.obj

def CategoryTheory.Pseudofunctor.ObjectProperty.mapId {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] (X : B) : P.map (CategoryStruct.id X) ≅ Functor.id (P.Obj X)

Auxiliary definition for fullsubcategory.

@[simp]

theorem CategoryTheory.Pseudofunctor.ObjectProperty.mapId_hom_app {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] {X : B} (M : P.Obj X) : (P.mapId X).hom.app M = ObjectProperty.homMk ((F.mapId X).hom.toNatTrans.app M.obj)

@[simp]

theorem CategoryTheory.Pseudofunctor.ObjectProperty.mapId_inv_app {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] {X : B} (M : P.Obj X) : (P.mapId X).inv.app M = ObjectProperty.homMk ((F.mapId X).inv.toNatTrans.app M.obj)

def CategoryTheory.Pseudofunctor.ObjectProperty.mapComp {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] {X Y Z : B} (f : X ⟶ Y) (g : Y ⟶ Z) : P.map (CategoryStruct.comp f g) ≅ (P.map f).comp (P.map g)

Auxiliary definition for fullsubcategory.

@[simp]

theorem CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_hom_app {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] {X Y Z : B} (f : X ⟶ Y) (g : Y ⟶ Z) (M : P.Obj X) : (P.mapComp f g).hom.app M = ObjectProperty.homMk ((F.mapComp f g).hom.toNatTrans.app M.obj)

@[simp]

theorem CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_inv_app {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] {X Y Z : B} (f : X ⟶ Y) (g : Y ⟶ Z) (M : P.Obj X) : (P.mapComp f g).inv.app M = ObjectProperty.homMk ((F.mapComp f g).inv.toNatTrans.app M.obj)

def CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] : Pseudofunctor B Cat

Given a property of objects P for a pseudofunctor from B to Cat, this is the induced pseudofunctor which sends X : B to the full subcategory of F.obj B consisting of objects satisfying P.

@[simp]

theorem CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] {X✝ Y✝ : B} (f : X✝ ⟶ Y✝) : (P.fullsubcategory.map f).toFunctor = P.map f

@[simp]

theorem CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapId {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] (X : B) : P.fullsubcategory.mapId X = Cat.Hom.isoMk (P.mapId X)

@[simp]

theorem CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] {a✝ b✝ : B} {f✝ g✝ : a✝ ⟶ b✝} (α : f✝ ⟶ g✝) : (P.fullsubcategory.map₂ α).toNatTrans = P.map₂ α

@[simp]

theorem CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapComp {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : P.fullsubcategory.mapComp f g = Cat.Hom.isoMk (P.mapComp f g)

@[simp]

theorem CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] (X : B) : P.fullsubcategory.obj X = Cat.of (P.Obj X)

def CategoryTheory.Pseudofunctor.ObjectProperty.ι {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] : P.fullsubcategory.StrongTrans F

The inclusion of P.fullsubcategory in F.

@[simp]

theorem CategoryTheory.Pseudofunctor.ObjectProperty.ι_app_toFunctor {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] (X : B) : (P.ι.app X).toFunctor = (P.prop X).ι

@[simp]

theorem CategoryTheory.Pseudofunctor.ObjectProperty.ι_naturality {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] {a✝ b✝ : B} (f : a✝ ⟶ b✝) : P.ι.naturality f = Iso.refl (CategoryStruct.comp (P.fullsubcategory.map f) { toFunctor := (P.prop b✝).ι })