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 a descent data relative to the morphisms f i : X i ⟶ S.

TODO (@joelriou, @chrisflav)

• Relate the prestack condition to the fully faithfullness of Pseudofunctor.toDescentData.
• Define stacks.
• 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).obj (self.obj i₁) ⟶ (F.map f₂.op.toLoc).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).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).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).obj (D.obj i₁) ≅ (F.map f₂.op.toLoc).obj (D.obj i₂)

The morphisms DescentData.hom, as isomorphisms.

Equations

• D.iso q f₁ f₂ _hf₁ _hf₂ = { hom := D.hom q f₁ f₂ ⋯ ⋯, inv := D.hom q f₂ f₁ ⋯ ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[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₁ ⋯ ⋯

@[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₂ ⋯ ⋯

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).map (self.hom i₁)) (D₂.hom q f₁ f₂ ⋯ ⋯) = CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯) ((F.map f₂.op.toLoc).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).obj (D₂.obj i₂) ⟶ Z) : CategoryStruct.comp ((F.map f₁.op.toLoc).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).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)

Equations

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

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.

Equations

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

@[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.app M) ((F.mapComp' (f i₂).op.toLoc f₂.op.toLoc q.op.toLoc ⋯).hom.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).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).map (e i₁).hom) (D₂.hom q f₁ f₂ ⋯ ⋯) = CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯) ((F.map f₂.op.toLoc).map (e i₂).hom) := by cat_disch) : D₁ ≅ D₂

Constructor for isomorphisms in Pseudofunctor.DescentData.

Equations

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

@[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).map (e i₁).hom) (D₂.hom q f₁ f₂ ⋯ ⋯) = CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯) ((F.map f₂.op.toLoc).map (e i₂).hom) := by cat_disch) (i : ι) : (isoMk e comm).hom.hom i = (e i).hom

@[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).map (e i₁).hom) (D₂.hom q f₁ f₂ ⋯ ⋯) = CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯) ((F.map f₂.op.toLoc).map (e i₂).hom) := by cat_disch) (i : ι) : (isoMk e comm).inv.hom i = (e i).inv

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.

Equations

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