Descent data

In this file, given a pseudofunctor F from LocallyDiscrete Cᵒᵖ to Cat, and a family of maps f i : X i ⟶ S in the category C, we define the category F.DescentData f of objects over the X i equipped with descent data relative to the morphisms f i : X i ⟶ S.

We show that up to an equivalence, the category F.DescentData f is unchanged when we replace S by an isomorphic object, or the family f i : X i ⟶ S by another family which generates the same sieve (see Pseudofunctor.DescentData.pullFunctorEquivalence).

Given a presieve R, we introduce predicates F.IsPrestackFor R and F.IsStackFor R saying the functor F.DescentData (fun (f : R.category) ↦ f.obj.hom) attached to R is respectively fully faithful or an equivalence. We show that F satisfies F.IsPrestack J for a Grothendieck topology J iff it satisfies F.IsPrestackFor R.arrows for all covering sieves R.

TODO (@joelriou, @chrisflav)

• Introduce multiple variants of DescentData (when C has pullbacks, when F also has a covariant functoriality, etc.).

structure CategoryTheory.Pseudofunctor.DescentData {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) : Type (max (max (max (max t u) u') v) v')

Given a pseudofunctor F from LocallyDiscrete Cᵒᵖ to Cat, and a family of morphisms f i : X i ⟶ S, the objects of the category of descent data for the X i relative to the morphisms f i consist of families of objects obj i in F.obj (.mk (op (X i))) together with morphisms hom between the pullbacks of obj i₁ and obj i₂ over any object Y which maps to both X i₁ and X i₂ (in a way that is compatible with the morphisms to S). The compatibilities these morphisms satisfy imply that the morphisms hom are isomorphisms.

• obj (i : ι) : ↑(F.obj { as := Opposite.op (X i) })

  The objects over X i for all i

• hom ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (_hf₁ : CategoryStruct.comp f₁ (f i₁) = q := by cat_disch) (_hf₂ : CategoryStruct.comp f₂ (f i₂) = q := by cat_disch) : (F.map f₁.op.toLoc).toFunctor.obj (self.obj i₁) ⟶ (F.map f₂.op.toLoc).toFunctor.obj (self.obj i₂)

  The compatibility morphisms after pullbacks. It follows from the conditions hom_self and hom_comp that these are isomorphisms, see CategoryTheory.Pseudofunctor.DescentData.iso below.

• pullHom_hom ⦃Y' Y : C⦄ (g : Y' ⟶ Y) (q : Y ⟶ S) (q' : Y' ⟶ S) (hq : CategoryStruct.comp g q = q') ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (hf₁ : CategoryStruct.comp f₁ (f i₁) = q) (hf₂ : CategoryStruct.comp f₂ (f i₂) = q) (gf₁ : Y' ⟶ X i₁) (gf₂ : Y' ⟶ X i₂) (hgf₁ : CategoryStruct.comp g f₁ = gf₁) (hgf₂ : CategoryStruct.comp g f₂ = gf₂) : LocallyDiscreteOpToCat.pullHom (self.hom q f₁ f₂ ⋯ ⋯) g gf₁ gf₂ ⋯ ⋯ = self.hom q' gf₁ gf₂ ⋯ ⋯
• hom_self ⦃Y : C⦄ (q : Y ⟶ S) ⦃i : ι⦄ (g : Y ⟶ X i) (x✝ : CategoryStruct.comp g (f i) = q) : self.hom q g g ⋯ ⋯ = CategoryStruct.id ((F.map g.op.toLoc).toFunctor.obj (self.obj i))
• hom_comp ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ i₃ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (f₃ : Y ⟶ X i₃) (hf₁ : CategoryStruct.comp f₁ (f i₁) = q) (hf₂ : CategoryStruct.comp f₂ (f i₂) = q) (hf₃ : CategoryStruct.comp f₃ (f i₃) = q) : CategoryStruct.comp (self.hom q f₁ f₂ hf₁ hf₂) (self.hom q f₂ f₃ hf₂ hf₃) = self.hom q f₁ f₃ hf₁ hf₃

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData.hom_comp_assoc {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (self : F.DescentData f) ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ i₃ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (f₃ : Y ⟶ X i₃) (hf₁ : CategoryStruct.comp f₁ (f i₁) = q) (hf₂ : CategoryStruct.comp f₂ (f i₂) = q) (hf₃ : CategoryStruct.comp f₃ (f i₃) = q) {Z : ↑(F.obj { as := Opposite.op Y })} (h : (F.map f₃.op.toLoc).toFunctor.obj (self.obj i₃) ⟶ Z) : CategoryStruct.comp (self.hom q f₁ f₂ hf₁ hf₂) (CategoryStruct.comp (self.hom q f₂ f₃ hf₂ hf₃) h) = CategoryStruct.comp (self.hom q f₁ f₃ hf₁ hf₃) h

def CategoryTheory.Pseudofunctor.DescentData.iso {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (D : F.DescentData f) ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (_hf₁ : CategoryStruct.comp f₁ (f i₁) = q := by cat_disch) (_hf₂ : CategoryStruct.comp f₂ (f i₂) = q := by cat_disch) : (F.map f₁.op.toLoc).toFunctor.obj (D.obj i₁) ≅ (F.map f₂.op.toLoc).toFunctor.obj (D.obj i₂)

The morphisms DescentData.hom, as isomorphisms.

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData.iso_hom {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (D : F.DescentData f) ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (_hf₁ : CategoryStruct.comp f₁ (f i₁) = q := by cat_disch) (_hf₂ : CategoryStruct.comp f₂ (f i₂) = q := by cat_disch) : (D.iso q f₁ f₂ _hf₁ _hf₂).hom = D.hom q f₁ f₂ ⋯ ⋯

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData.iso_inv {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (D : F.DescentData f) ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (_hf₁ : CategoryStruct.comp f₁ (f i₁) = q := by cat_disch) (_hf₂ : CategoryStruct.comp f₂ (f i₂) = q := by cat_disch) : (D.iso q f₁ f₂ _hf₁ _hf₂).inv = D.hom q f₂ f₁ ⋯ ⋯

instance CategoryTheory.Pseudofunctor.DescentData.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpHom {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (D : F.DescentData f) {Y : C} (q : Y ⟶ S) {i₁ i₂ : ι} (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (hf₁ : CategoryStruct.comp f₁ (f i₁) = q) (hf₂ : CategoryStruct.comp f₂ (f i₂) = q) : IsIso (D.hom q f₁ f₂ hf₁ hf₂)

structure CategoryTheory.Pseudofunctor.DescentData.Hom {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (D₁ D₂ : F.DescentData f) : Type (max t v')

The type of morphisms in the category Pseudofunctor.DescentData.

• hom (i : ι) : D₁.obj i ⟶ D₂.obj i

  The morphisms between the obj fields of descent data.

• comm ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (hf₁ : CategoryStruct.comp f₁ (f i₁) = q) (hf₂ : CategoryStruct.comp f₂ (f i₂) = q) : CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (self.hom i₁)) (D₂.hom q f₁ f₂ ⋯ ⋯) = CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯) ((F.map f₂.op.toLoc).toFunctor.map (self.hom i₂))

theorem CategoryTheory.Pseudofunctor.DescentData.Hom.ext {C : Type u} {inst✝ : Category.{v, u} C} {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentData f} {x y : D₁.Hom D₂} (hom : x.hom = y.hom) : x = y

theorem CategoryTheory.Pseudofunctor.DescentData.Hom.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentData f} {x y : D₁.Hom D₂} : x = y ↔ x.hom = y.hom

theorem CategoryTheory.Pseudofunctor.DescentData.Hom.comm_assoc {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentData f} (self : D₁.Hom D₂) ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (hf₁ : CategoryStruct.comp f₁ (f i₁) = q) (hf₂ : CategoryStruct.comp f₂ (f i₂) = q) {Z : ↑(F.obj { as := Opposite.op Y })} (h : (F.map f₂.op.toLoc).toFunctor.obj (D₂.obj i₂) ⟶ Z) : CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (self.hom i₁)) (CategoryStruct.comp (D₂.hom q f₁ f₂ ⋯ ⋯) h) = CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯) (CategoryStruct.comp ((F.map f₂.op.toLoc).toFunctor.map (self.hom i₂)) h)

instance CategoryTheory.Pseudofunctor.DescentData.instCategory {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} : Category.{max t v', max (max (max (max u u') v) v') t} (F.DescentData f)

theorem CategoryTheory.Pseudofunctor.DescentData.hom_ext {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentData f} {φ φ' : D₁ ⟶ D₂} (h : ∀ (i : ι), φ.hom i = φ'.hom i) : φ = φ'

theorem CategoryTheory.Pseudofunctor.DescentData.hom_ext_iff {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentData f} {φ φ' : D₁ ⟶ D₂} : φ = φ' ↔ ∀ (i : ι), φ.hom i = φ'.hom i

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData.id_hom {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (D : F.DescentData f) (i : ι) : (CategoryStruct.id D).hom i = CategoryStruct.id (D.obj i)

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData.comp_hom {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ D₃ : F.DescentData f} (φ : D₁ ⟶ D₂) (φ' : D₂ ⟶ D₃) (i : ι) : (CategoryStruct.comp φ φ').hom i = CategoryStruct.comp (φ.hom i) (φ'.hom i)

theorem CategoryTheory.Pseudofunctor.DescentData.comp_hom_assoc {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ D₃ : F.DescentData f} (φ : D₁ ⟶ D₂) (φ' : D₂ ⟶ D₃) (i : ι) {Z : ↑(F.obj { as := Opposite.op (X i) })} (h : D₃.obj i ⟶ Z) : CategoryStruct.comp ((CategoryStruct.comp φ φ').hom i) h = CategoryStruct.comp (φ.hom i) (CategoryStruct.comp (φ'.hom i) h)

def CategoryTheory.Pseudofunctor.DescentData.ofObj {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (M : ↑(F.obj { as := Opposite.op S })) : F.DescentData f

Given a family of morphisms f : X i ⟶ S, and M : F.obj (.mk (op S)), this is the object in F.DescentData f that is obtained by pulling back M over the X i.

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData.ofObj_hom {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (M : ↑(F.obj { as := Opposite.op S })) (Y : C) (q : Y ⟶ S) (i₁ i₂ : ι) (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (hf₁ : CategoryStruct.comp f₁ (f i₁) = q) (hf₂ : CategoryStruct.comp f₂ (f i₂) = q) : (ofObj M).hom q f₁ f₂ hf₁ hf₂ = CategoryStruct.comp ((F.mapComp' (f i₁).op.toLoc f₁.op.toLoc q.op.toLoc ⋯).inv.toNatTrans.app M) ((F.mapComp' (f i₂).op.toLoc f₂.op.toLoc q.op.toLoc ⋯).hom.toNatTrans.app M)

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData.ofObj_obj {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (M : ↑(F.obj { as := Opposite.op S })) (i : ι) : (ofObj M).obj i = (F.map (f i).op.toLoc).toFunctor.obj M

def CategoryTheory.Pseudofunctor.DescentData.isoMk {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentData f} (e : (i : ι) → D₁.obj i ≅ D₂.obj i) (comm : ∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (hf₁ : CategoryStruct.comp f₁ (f i₁) = q) (hf₂ : CategoryStruct.comp f₂ (f i₂) = q), CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (e i₁).hom) (D₂.hom q f₁ f₂ ⋯ ⋯) = CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯) ((F.map f₂.op.toLoc).toFunctor.map (e i₂).hom) := by cat_disch) : D₁ ≅ D₂

Constructor for isomorphisms in Pseudofunctor.DescentData.

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData.isoMk_inv_hom {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentData f} (e : (i : ι) → D₁.obj i ≅ D₂.obj i) (comm : ∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (hf₁ : CategoryStruct.comp f₁ (f i₁) = q) (hf₂ : CategoryStruct.comp f₂ (f i₂) = q), CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (e i₁).hom) (D₂.hom q f₁ f₂ ⋯ ⋯) = CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯) ((F.map f₂.op.toLoc).toFunctor.map (e i₂).hom) := by cat_disch) (i : ι) : (isoMk e comm).inv.hom i = (e i).inv

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData.isoMk_hom_hom {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentData f} (e : (i : ι) → D₁.obj i ≅ D₂.obj i) (comm : ∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (hf₁ : CategoryStruct.comp f₁ (f i₁) = q) (hf₂ : CategoryStruct.comp f₂ (f i₂) = q), CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (e i₁).hom) (D₂.hom q f₁ f₂ ⋯ ⋯) = CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯) ((F.map f₂.op.toLoc).toFunctor.map (e i₂).hom) := by cat_disch) (i : ι) : (isoMk e comm).hom.hom i = (e i).hom

def CategoryTheory.Pseudofunctor.toDescentData {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) : Functor (↑(F.obj { as := Opposite.op S })) (F.DescentData f)

The functor F.obj (.mk (op S)) ⥤ F.DescentData f.

@[simp]

theorem CategoryTheory.Pseudofunctor.toDescentData_map_hom {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) {M M' : ↑(F.obj { as := Opposite.op S })} (φ : M ⟶ M') (i : ι) : ((F.toDescentData f).map φ).hom i = (F.map (f i).op.toLoc).toFunctor.map φ

@[simp]

theorem CategoryTheory.Pseudofunctor.toDescentData_obj {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) (M : ↑(F.obj { as := Opposite.op S })) : (F.toDescentData f).obj M = DescentData.ofObj M

def CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = CategoryStruct.comp (f' j) p) (D : F.DescentData f) ⦃Y : C⦄ (q : Y ⟶ S') ⦃j₁ j₂ : ι'⦄ (f₁ : Y ⟶ X' j₁) (f₂ : Y ⟶ X' j₂) (hf₁ : CategoryStruct.comp f₁ (f' j₁) = q := by cat_disch) (hf₂ : CategoryStruct.comp f₂ (f' j₂) = q := by cat_disch) : (F.map f₁.op.toLoc).toFunctor.obj ((F.map (p' j₁).op.toLoc).toFunctor.obj (D.obj (α j₁))) ⟶ (F.map f₂.op.toLoc).toFunctor.obj ((F.map (p' j₂).op.toLoc).toFunctor.obj (D.obj (α j₂)))

Auxiliary definition for pullFunctor.

theorem CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = CategoryStruct.comp (f' j) p) (D : F.DescentData f) ⦃Y : C⦄ (q : Y ⟶ S') ⦃j₁ j₂ : ι'⦄ (f₁ : Y ⟶ X' j₁) (f₂ : Y ⟶ X' j₂) (q' : Y ⟶ S) (f₁' : Y ⟶ X (α j₁)) (f₂' : Y ⟶ X (α j₂)) (hf₁ : CategoryStruct.comp f₁ (f' j₁) = q := by cat_disch) (hf₂ : CategoryStruct.comp f₂ (f' j₂) = q := by cat_disch) (hq' : CategoryStruct.comp q p = q' := by cat_disch) (hf₁' : CategoryStruct.comp f₁ (p' j₁) = f₁' := by cat_disch) (hf₂' : CategoryStruct.comp f₂ (p' j₂) = f₂' := by cat_disch) : pullFunctorObjHom w D q f₁ f₂ ⋯ ⋯ = CategoryStruct.comp ((F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc f₁'.op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁))) (CategoryStruct.comp (D.hom q' f₁' f₂' ⋯ ⋯) ((F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc f₂'.op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₂))))

theorem CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq_assoc {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = CategoryStruct.comp (f' j) p) (D : F.DescentData f) ⦃Y : C⦄ (q : Y ⟶ S') ⦃j₁ j₂ : ι'⦄ (f₁ : Y ⟶ X' j₁) (f₂ : Y ⟶ X' j₂) (q' : Y ⟶ S) (f₁' : Y ⟶ X (α j₁)) (f₂' : Y ⟶ X (α j₂)) (hf₁ : CategoryStruct.comp f₁ (f' j₁) = q := by cat_disch) (hf₂ : CategoryStruct.comp f₂ (f' j₂) = q := by cat_disch) (hq' : CategoryStruct.comp q p = q' := by cat_disch) (hf₁' : CategoryStruct.comp f₁ (p' j₁) = f₁' := by cat_disch) (hf₂' : CategoryStruct.comp f₂ (p' j₂) = f₂' := by cat_disch) {Z : ↑(F.obj { as := Opposite.op Y })} (h : (F.map f₂.op.toLoc).toFunctor.obj ((F.map (p' j₂).op.toLoc).toFunctor.obj (D.obj (α j₂))) ⟶ Z) : CategoryStruct.comp (pullFunctorObjHom w D q f₁ f₂ ⋯ ⋯) h = CategoryStruct.comp ((F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc f₁'.op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁))) (CategoryStruct.comp (D.hom q' f₁' f₂' ⋯ ⋯) (CategoryStruct.comp ((F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc f₂'.op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₂))) h))

def CategoryTheory.Pseudofunctor.DescentData.pullFunctorObj {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = CategoryStruct.comp (f' j) p) (D : F.DescentData f) : F.DescentData f'

Auxiliary definition for pullFunctor.

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData.pullFunctorObj_hom {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = CategoryStruct.comp (f' j) p) (D : F.DescentData f) (Y : C) (q : Y ⟶ S') (j₁ j₂ : ι') (f₁ : Y ⟶ X' j₁) (f₂ : Y ⟶ X' j₂) (hf₁ : CategoryStruct.comp f₁ (f' j₁) = q) (hf₂ : CategoryStruct.comp f₂ (f' j₂) = q) : (pullFunctorObj w D).hom q f₁ f₂ hf₁ hf₂ = pullFunctorObjHom w D (CategoryStruct.comp f₁ (f' j₁)) f₁ f₂ ⋯ ⋯

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData.pullFunctorObj_obj {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = CategoryStruct.comp (f' j) p) (D : F.DescentData f) (j : ι') : (pullFunctorObj w D).obj j = (F.map (p' j).op.toLoc).toFunctor.obj (D.obj (α j))

def CategoryTheory.Pseudofunctor.DescentData.pullFunctor {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = CategoryStruct.comp (f' j) p) : Functor (F.DescentData f) (F.DescentData f')

Given a family of morphisms f : X i ⟶ S and f' : X' j ⟶ S', and suitable commutative diagrams p' j ≫ f (α j) = f' j ≫ p, this is the induced functor F.DescentData f ⥤ F.DescentData f'. (Up to a (unique) isomorphism, this functor only depends on f and f', see pullFunctorIso.)

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData.pullFunctor_map_hom {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = CategoryStruct.comp (f' j) p) {D₁ D₂ : F.DescentData f} (φ : D₁ ⟶ D₂) (j : ι') : ((pullFunctor F w).map φ).hom j = (F.map (p' j).op.toLoc).toFunctor.map (φ.hom (α j))

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData.pullFunctor_obj {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = CategoryStruct.comp (f' j) p) (D : F.DescentData f) : (pullFunctor F w).obj D = pullFunctorObj w D

def CategoryTheory.Pseudofunctor.DescentData.toDescentDataCompPullFunctorIso {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = CategoryStruct.comp (f' j) p) : (F.toDescentData f).comp (pullFunctor F w) ≅ (F.map p.op.toLoc).toFunctor.comp (F.toDescentData f')

Given families of morphisms f : X i ⟶ S and f' : X' j ⟶ S', suitable commutative diagrams w j : p' j ≫ f (α j) = f' j ≫ p, this is the natural isomorphism between the descent data relative to f' that are obtained either:

• by considering the obvious descent data relative to f given by an object M : F.obj (op S), followed by the application of pullFunctor F w : F.DescentData f ⥤ F.DescentData f';
• by considering the obvious descent data relative to f' given by pulling back the object M to S'.

def CategoryTheory.Pseudofunctor.DescentData.pullFunctorIso {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = CategoryStruct.comp (f' j) p) {β : ι' → ι} {p'' : (j : ι') → X' j ⟶ X (β j)} (w' : ∀ (j : ι'), CategoryStruct.comp (p'' j) (f (β j)) = CategoryStruct.comp (f' j) p) : pullFunctor F w ≅ pullFunctor F w'

Up to a (unique) isomorphism, the functor pullFunctor : F.DescentData f ⥤ F.DescentData f' does not depend on the auxiliary data.

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData.pullFunctorIso_inv_app_hom {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = CategoryStruct.comp (f' j) p) {β : ι' → ι} {p'' : (j : ι') → X' j ⟶ X (β j)} (w' : ∀ (j : ι'), CategoryStruct.comp (p'' j) (f (β j)) = CategoryStruct.comp (f' j) p) (X✝ : F.DescentData f) (i : ι') : ((pullFunctorIso F w w').inv.app X✝).hom i = X✝.hom (CategoryStruct.comp (p' i) (f (α i))) (p'' i) (p' i) ⋯ ⋯

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData.pullFunctorIso_hom_app_hom {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = CategoryStruct.comp (f' j) p) {β : ι' → ι} {p'' : (j : ι') → X' j ⟶ X (β j)} (w' : ∀ (j : ι'), CategoryStruct.comp (p'' j) (f (β j)) = CategoryStruct.comp (f' j) p) (X✝ : F.DescentData f) (i : ι') : ((pullFunctorIso F w w').hom.app X✝).hom i = X✝.hom (CategoryStruct.comp (p' i) (f (α i))) (p' i) (p'' i) ⋯ ⋯

def CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} (S : C) {X : ι → C} {f : (i : ι) → X i ⟶ S} : pullFunctor F ⋯ ≅ Functor.id (F.DescentData f)

The functor F.DescentData f ⥤ F.DescentData f corresponding to pullFunctor applied to identity morphisms is isomorphic to the identity functor.

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_hom_app_hom {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} (S : C) {X : ι → C} {f : (i : ι) → X i ⟶ S} (X✝ : F.DescentData f) (i : ι) : ((pullFunctorIdIso F S).hom.app X✝).hom i = (F.mapId { as := Opposite.op (X i) }).hom.toNatTrans.app (X✝.obj i)

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_inv_app_hom {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} (S : C) {X : ι → C} {f : (i : ι) → X i ⟶ S} (X✝ : F.DescentData f) (i : ι) : ((pullFunctorIdIso F S).inv.app X✝).hom i = (F.mapId { as := Opposite.op (X i) }).inv.toNatTrans.app (X✝.obj i)

def CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = CategoryStruct.comp (f' j) p) {S'' : C} {q : S'' ⟶ S'} {ι'' : Type t''} {X'' : ι'' → C} {f'' : (k : ι'') → X'' k ⟶ S''} {β : ι'' → ι'} {q' : (k : ι'') → X'' k ⟶ X' (β k)} (w' : ∀ (k : ι''), CategoryStruct.comp (q' k) (f' (β k)) = CategoryStruct.comp (f'' k) q) (r : S'' ⟶ S) {r' : (k : ι'') → X'' k ⟶ X (α (β k))} (hr : CategoryStruct.comp q p = r := by cat_disch) (hr' : ∀ (k : ι''), CategoryStruct.comp (q' k) (p' (β k)) = r' k := by cat_disch) : (pullFunctor F w).comp (pullFunctor F w') ≅ pullFunctor F ⋯

The composition of two functors pullFunctor is isomorphic to pullFunctor applied to the compositions.

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_hom_app_hom {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = CategoryStruct.comp (f' j) p) {S'' : C} {q : S'' ⟶ S'} {ι'' : Type t''} {X'' : ι'' → C} {f'' : (k : ι'') → X'' k ⟶ S''} {β : ι'' → ι'} {q' : (k : ι'') → X'' k ⟶ X' (β k)} (w' : ∀ (k : ι''), CategoryStruct.comp (q' k) (f' (β k)) = CategoryStruct.comp (f'' k) q) (r : S'' ⟶ S) {r' : (k : ι'') → X'' k ⟶ X (α (β k))} (hr : CategoryStruct.comp q p = r := by cat_disch) (hr' : ∀ (k : ι''), CategoryStruct.comp (q' k) (p' (β k)) = r' k := by cat_disch) (X✝ : F.DescentData f) (i : ι'') : ((pullFunctorCompIso F w w' r hr hr').hom.app X✝).hom i = (F.mapComp' (p' (β i)).op.toLoc (q' i).op.toLoc (r' i).op.toLoc ⋯).inv.toNatTrans.app (X✝.obj (α (β i)))

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_inv_app_hom {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = CategoryStruct.comp (f' j) p) {S'' : C} {q : S'' ⟶ S'} {ι'' : Type t''} {X'' : ι'' → C} {f'' : (k : ι'') → X'' k ⟶ S''} {β : ι'' → ι'} {q' : (k : ι'') → X'' k ⟶ X' (β k)} (w' : ∀ (k : ι''), CategoryStruct.comp (q' k) (f' (β k)) = CategoryStruct.comp (f'' k) q) (r : S'' ⟶ S) {r' : (k : ι'') → X'' k ⟶ X (α (β k))} (hr : CategoryStruct.comp q p = r := by cat_disch) (hr' : ∀ (k : ι''), CategoryStruct.comp (q' k) (p' (β k)) = r' k := by cat_disch) (X✝ : F.DescentData f) (i : ι'') : ((pullFunctorCompIso F w w' r hr hr').inv.app X✝).hom i = (F.mapComp' (p' (β i)).op.toLoc (q' i).op.toLoc (r' i).op.toLoc ⋯).hom.toNatTrans.app (X✝.obj (α (β i)))

def CategoryTheory.Pseudofunctor.DescentData.pullFunctorEquivalence {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} (e : S' ≅ S) {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = CategoryStruct.comp (f' j) e.hom) {β : ι → ι'} {q' : (i : ι) → X i ⟶ X' (β i)} (w' : ∀ (i : ι), CategoryStruct.comp (q' i) (f' (β i)) = CategoryStruct.comp (f i) e.inv) : F.DescentData f ≌ F.DescentData f'

Up to an equivalence, the category DescentData for a pseudofunctor F and a family of morphisms f : X i ⟶ S is unchanged when we replace S by an isomorphic object, or when we replace f by another family which generate the same sieve.

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData.pullFunctorEquivalence_counitIso {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} (e : S' ≅ S) {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = CategoryStruct.comp (f' j) e.hom) {β : ι → ι'} {q' : (i : ι) → X i ⟶ X' (β i)} (w' : ∀ (i : ι), CategoryStruct.comp (q' i) (f' (β i)) = CategoryStruct.comp (f i) e.inv) : (pullFunctorEquivalence F e w w').counitIso = pullFunctorCompIso F w' w (CategoryStruct.id S') ⋯ ⋯ ≪≫ pullFunctorIso F ⋯ ⋯ ≪≫ pullFunctorIdIso F S'

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData.pullFunctorEquivalence_functor {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} (e : S' ≅ S) {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = CategoryStruct.comp (f' j) e.hom) {β : ι → ι'} {q' : (i : ι) → X i ⟶ X' (β i)} (w' : ∀ (i : ι), CategoryStruct.comp (q' i) (f' (β i)) = CategoryStruct.comp (f i) e.inv) : (pullFunctorEquivalence F e w w').functor = pullFunctor F w

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData.pullFunctorEquivalence_inverse {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} (e : S' ≅ S) {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = CategoryStruct.comp (f' j) e.hom) {β : ι → ι'} {q' : (i : ι) → X i ⟶ X' (β i)} (w' : ∀ (i : ι), CategoryStruct.comp (q' i) (f' (β i)) = CategoryStruct.comp (f i) e.inv) : (pullFunctorEquivalence F e w w').inverse = pullFunctor F w'

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData.pullFunctorEquivalence_unitIso {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} (e : S' ≅ S) {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = CategoryStruct.comp (f' j) e.hom) {β : ι → ι'} {q' : (i : ι) → X i ⟶ X' (β i)} (w' : ∀ (i : ι), CategoryStruct.comp (q' i) (f' (β i)) = CategoryStruct.comp (f i) e.inv) : (pullFunctorEquivalence F e w w').unitIso = (pullFunctorIdIso F S).symm ≪≫ pullFunctorIso F ⋯ ⋯ ≪≫ (pullFunctorCompIso F w w' (CategoryStruct.id S) ⋯ ⋯).symm

theorem CategoryTheory.Pseudofunctor.DescentData.exists_equivalence_of_sieve_eq {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) {ι' : Type t'} {X' : ι' → C} (f' : (i' : ι') → X' i' ⟶ S) (h : Sieve.ofArrows X f = Sieve.ofArrows X' f') : ∃ (e : F.DescentData f ≌ F.DescentData f'), Nonempty ((F.toDescentData f).comp e.functor ≅ F.toDescentData f')

theorem CategoryTheory.Pseudofunctor.DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) {ι' : Type t'} {X' : ι' → C} (f' : (i' : ι') → X' i' ⟶ S) (h : Sieve.ofArrows X f = Sieve.ofArrows X' f') : Nonempty (F.toDescentData f).FullyFaithful ↔ Nonempty (F.toDescentData f').FullyFaithful

theorem CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_iff_of_sieve_eq {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) {ι' : Type t'} {X' : ι' → C} (f' : (i' : ι') → X' i' ⟶ S) (h : Sieve.ofArrows X f = Sieve.ofArrows X' f') : (F.toDescentData f).IsEquivalence ↔ (F.toDescentData f').IsEquivalence

def CategoryTheory.Pseudofunctor.DescentData.subtypeCompatibleHomEquiv {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) {M N : ↑(F.obj { as := Opposite.op S })} : Subtype (Presieve.Arrows.Compatible (F.presheafHom M N) fun (i : ι) => Over.homMk (f i) ⋯) ≃ ((F.toDescentData f).obj M ⟶ (F.toDescentData f).obj N)

Morphisms between objects in the image of the functor F.toDescentData f identify to compatible families of sections of the presheaf F.presheafHom M N on the object Over.mk (𝟙 S), relatively to the family of morphisms in Over S corresponding to the family f.

theorem CategoryTheory.Pseudofunctor.DescentData.subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) {M N : ↑(F.obj { as := Opposite.op S })} (φ : M ⟶ N) : (subtypeCompatibleHomEquiv F f) (Presieve.Arrows.toCompatible (F.presheafHom M N) (fun (i : ι) => Over.homMk (f i) ⋯) (F.presheafHomObjHomEquiv φ)) = (F.toDescentData f).map φ

structure CategoryTheory.Pseudofunctor.IsPrestackFor {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {S : C} (R : Presieve S) : Prop

The condition that a pseudofunctor satisfies the descent of morphisms relative to a presieve.

• nonempty_fullyFaithful : Nonempty (F.toDescentData fun (f : R.category) => f.obj.hom).FullyFaithful

theorem CategoryTheory.Pseudofunctor.isPrestackFor_iff {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {S : C} (R : Presieve S) : F.IsPrestackFor R ↔ Nonempty (F.toDescentData fun (f : R.category) => f.obj.hom).FullyFaithful

noncomputable def CategoryTheory.Pseudofunctor.IsPrestackFor.fullyFaithful {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {S : C} {R : Presieve S} (hF : F.IsPrestackFor R) : (F.toDescentData fun (f : R.category) => f.obj.hom).FullyFaithful

If R is a presieve such that F.IsPrestackFor R, then the functor F.toDescentData (fun (f : R.category) ↦ f.obj.hom) is fully faithful.

theorem CategoryTheory.Pseudofunctor.isPrestackFor_iff_of_sieve_eq {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {S : C} {R R' : Presieve S} (h : Sieve.generate R = Sieve.generate R') : F.IsPrestackFor R ↔ F.IsPrestackFor R'

@[simp]

theorem CategoryTheory.Pseudofunctor.IsPrestackFor_generate_iff {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {S : C} (R : Presieve S) : F.IsPrestackFor (Sieve.generate R).arrows ↔ F.IsPrestackFor R

theorem CategoryTheory.Pseudofunctor.isPrestackFor_ofArrows_iff {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) : F.IsPrestackFor (Presieve.ofArrows X f) ↔ Nonempty (F.toDescentData f).FullyFaithful

structure CategoryTheory.Pseudofunctor.IsStackFor {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {S : C} (R : Presieve S) : Prop

The condition that a pseudofunctor has effective descent relative to a presieve.

• isEquivalence : (F.toDescentData fun (f : R.category) => f.obj.hom).IsEquivalence

theorem CategoryTheory.Pseudofunctor.isStackFor_iff {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {S : C} (R : Presieve S) : F.IsStackFor R ↔ (F.toDescentData fun (f : R.category) => f.obj.hom).IsEquivalence

theorem CategoryTheory.Pseudofunctor.IsStackFor.isPrestackFor {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {S : C} {R : Presieve S} (h : F.IsStackFor R) : F.IsPrestackFor R

theorem CategoryTheory.Pseudofunctor.IsStackFor.essSurj {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {S : C} {R : Presieve S} (h : F.IsStackFor R) : (F.toDescentData fun (f : R.category) => f.obj.hom).EssSurj

theorem CategoryTheory.Pseudofunctor.isStackFor_iff_of_sieve_eq {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {S : C} {R R' : Presieve S} (h : Sieve.generate R = Sieve.generate R') : F.IsStackFor R ↔ F.IsStackFor R'

@[simp]

theorem CategoryTheory.Pseudofunctor.IsStackFor_generate_iff {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {S : C} (R : Presieve S) : F.IsStackFor (Sieve.generate R).arrows ↔ F.IsStackFor R

theorem CategoryTheory.Pseudofunctor.isStackFor_ofArrows_iff {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) : F.IsStackFor (Presieve.ofArrows X f) ↔ (F.toDescentData f).IsEquivalence

theorem CategoryTheory.Pseudofunctor.bijective_toDescentData_map_iff {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) (M N : ↑(F.obj { as := Opposite.op S })) : Function.Bijective (F.toDescentData f).map ↔ Presieve.IsSheafFor (F.presheafHom M N) (Presieve.ofArrows (fun (i : ι) => Over.mk (f i)) fun (i : ι) => Over.homMk (f i) ⋯)

theorem CategoryTheory.Pseudofunctor.isPrestackFor_iff_isSheafFor {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {S : C} (R : Sieve S) : F.IsPrestackFor R.arrows ↔ ∀ (M N : ↑(F.obj { as := Opposite.op S })), Presieve.IsSheafFor (F.presheafHom M N) ((Sieve.overEquiv (Over.mk (CategoryStruct.id S))).symm R).arrows

theorem CategoryTheory.Pseudofunctor.isPrestackFor_iff_isSheafFor' {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {S : C} (R : Sieve S) : F.IsPrestackFor R.arrows ↔ ∀ ⦃S₀ : C⦄ (M N : ↑(F.obj { as := Opposite.op S₀ })) (a : S ⟶ S₀), Presieve.IsSheafFor (F.presheafHom M N) ((Sieve.overEquiv (Over.mk a)).symm R).arrows

theorem CategoryTheory.Pseudofunctor.IsPrestackFor.isSheafFor' {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {S₀ : C} (S : Over S₀) {R : Sieve S} (hF : F.IsPrestackFor ((Sieve.overEquiv S) R).arrows) (M N : ↑(F.obj { as := Opposite.op S₀ })) : Presieve.IsSheafFor (F.presheafHom M N) R.arrows

noncomputable def CategoryTheory.Pseudofunctor.fullyFaithfulToDescentData {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) {J : GrothendieckTopology C} [F.IsPrestack J] (hf : Sieve.ofArrows X f ∈ J S) : (F.toDescentData f).FullyFaithful

If F is a prestack for a Grothendieck topology J, and f is a covering family of morphisms, then the functor F.toDescentData f is fully faithful.

theorem CategoryTheory.Pseudofunctor.isPrestackFor {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {J : GrothendieckTopology C} [F.IsPrestack J] {S : C} (R : Presieve S) (hR : Sieve.generate R ∈ J S) : F.IsPrestackFor R

theorem CategoryTheory.Pseudofunctor.isPrestackFor' {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {J : GrothendieckTopology C} [F.IsPrestack J] {S : C} (R : Sieve S) (hR : R ∈ J S) : F.IsPrestackFor R.arrows

theorem CategoryTheory.Pseudofunctor.IsPrestack.of_isPrestackFor {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {J : GrothendieckTopology C} (hF : ∀ (S : C), ∀ R ∈ J S, F.IsPrestackFor R.arrows) : F.IsPrestack J