Descent data when we have pullbacks

In this file, given a pseudofunctor F from LocallyDiscrete Cᵒᵖ to Cat, a family of maps f i : X i ⟶ S in the category C, chosen pullbacks sq and threefold wide pullbacks sq₃ for these morphisms, we define a category F.DescentData' sq sq₃ of objects over the X i equipped with a descent data relative to the morphisms f i : X i ⟶ S, where the data and compatibilities are expressed using the chosen pullbacks.

noncomputable def CategoryTheory.Pseudofunctor.DescentData'.pullHom' {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {obj obj' : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })} (hom : (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)) ⦃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 (obj i₁) ⟶ (F.map f₂.op.toLoc).toFunctor.obj (obj' i₂)

Variant of Pseudofunctor.LocallyDiscreteOpToCat.pullHom when we have chosen pullbacks.

Equations

• CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom q f₁ f₂ hf₁ hf₂ = CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom (hom i₁ i₂) (⋯.lift f₁ f₂ ⋯) f₁ f₂ ⋯ ⋯

theorem CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {obj obj' : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })} (hom : (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)) ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (p : Y ⟶ (sq i₁ i₂).pullback) (hf₁ : CategoryStruct.comp f₁ (f i₁) = q := by cat_disch) (hf₂ : CategoryStruct.comp f₂ (f i₂) = q := by cat_disch) (hp₁ : CategoryStruct.comp p (sq i₁ i₂).p₁ = f₁ := by cat_disch) (hp₂ : CategoryStruct.comp p (sq i₁ i₂).p₂ = f₂ := by cat_disch) : pullHom' hom q f₁ f₂ hf₁ hf₂ = LocallyDiscreteOpToCat.pullHom (hom i₁ i₂) p f₁ f₂ ⋯ ⋯

theorem CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom_assoc {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {obj obj' : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })} (hom : (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)) ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (p : Y ⟶ (sq i₁ i₂).pullback) (hf₁ : CategoryStruct.comp f₁ (f i₁) = q := by cat_disch) (hf₂ : CategoryStruct.comp f₂ (f i₂) = q := by cat_disch) (hp₁ : CategoryStruct.comp p (sq i₁ i₂).p₁ = f₁ := by cat_disch) (hp₂ : CategoryStruct.comp p (sq i₁ i₂).p₂ = f₂ := by cat_disch) {Z : ↑(F.obj { as := Opposite.op Y })} (h : (F.map f₂.op.toLoc).toFunctor.obj (obj' i₂) ⟶ Z) : CategoryStruct.comp (pullHom' hom q f₁ f₂ hf₁ hf₂) h = CategoryStruct.comp (LocallyDiscreteOpToCat.pullHom (hom i₁ i₂) p f₁ f₂ ⋯ ⋯) h

theorem CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃ {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} (sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) {obj obj' : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })} (hom : (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)) (i₁ i₂ i₃ : ι) : pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯ = LocallyDiscreteOpToCat.pullHom (hom i₁ i₂) (sq₃ i₁ i₂ i₃).p₁₂ (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯

theorem CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃_assoc {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} (sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) {obj obj' : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })} (hom : (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)) (i₁ i₂ i₃ : ι) {Z : ↑(F.obj { as := Opposite.op (sq₃ i₁ i₂ i₃).chosenPullback.pullback })} (h : (F.map (sq₃ i₁ i₂ i₃).p₂.op.toLoc).toFunctor.obj (obj' i₂) ⟶ Z) : CategoryStruct.comp (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯) h = CategoryStruct.comp (LocallyDiscreteOpToCat.pullHom (hom i₁ i₂) (sq₃ i₁ i₂ i₃).p₁₂ (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯) h

theorem CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃ {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} (sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) {obj obj' : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })} (hom : (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)) (i₁ i₂ i₃ : ι) : pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯ = LocallyDiscreteOpToCat.pullHom (hom i₁ i₃) (sq₃ i₁ i₂ i₃).p₁₃ (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯

theorem CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃_assoc {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} (sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) {obj obj' : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })} (hom : (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)) (i₁ i₂ i₃ : ι) {Z : ↑(F.obj { as := Opposite.op (sq₃ i₁ i₂ i₃).chosenPullback.pullback })} (h : (F.map (sq₃ i₁ i₂ i₃).p₃.op.toLoc).toFunctor.obj (obj' i₃) ⟶ Z) : CategoryStruct.comp (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) h = CategoryStruct.comp (LocallyDiscreteOpToCat.pullHom (hom i₁ i₃) (sq₃ i₁ i₂ i₃).p₁₃ (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) h

theorem CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃ {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} (sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) {obj obj' : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })} (hom : (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)) (i₁ i₂ i₃ : ι) : pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯ = LocallyDiscreteOpToCat.pullHom (hom i₂ i₃) (sq₃ i₁ i₂ i₃).p₂₃ (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯

theorem CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃_assoc {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} (sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) {obj obj' : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })} (hom : (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)) (i₁ i₂ i₃ : ι) {Z : ↑(F.obj { as := Opposite.op (sq₃ i₁ i₂ i₃).chosenPullback.pullback })} (h : (F.map (sq₃ i₁ i₂ i₃).p₃.op.toLoc).toFunctor.obj (obj' i₃) ⟶ Z) : CategoryStruct.comp (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) h = CategoryStruct.comp (LocallyDiscreteOpToCat.pullHom (hom i₂ i₃) (sq₃ i₁ i₂ i₃).p₂₃ (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) h

theorem CategoryTheory.Pseudofunctor.DescentData'.pullHom_pullHom' {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {obj obj' : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })} (hom : (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)) ⦃Y Y' : C⦄ (g : Y' ⟶ Y) (q : Y ⟶ S) (q' : Y' ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (gf₁ : Y' ⟶ X i₁) (gf₂ : Y' ⟶ X i₂) (hq : CategoryStruct.comp g q = q' := by cat_disch) (hf₁ : CategoryStruct.comp f₁ (f i₁) = q := by cat_disch) (hf₂ : CategoryStruct.comp f₂ (f i₂) = q := by cat_disch) (hgf₁ : CategoryStruct.comp g f₁ = gf₁ := by cat_disch) (hgf₂ : CategoryStruct.comp g f₂ = gf₂ := by cat_disch) : LocallyDiscreteOpToCat.pullHom (pullHom' hom q f₁ f₂ hf₁ hf₂) g gf₁ gf₂ ⋯ ⋯ = pullHom' hom q' gf₁ gf₂ ⋯ ⋯

theorem CategoryTheory.Pseudofunctor.DescentData'.pullHom_pullHom'_assoc {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {obj obj' : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })} (hom : (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)) ⦃Y Y' : C⦄ (g : Y' ⟶ Y) (q : Y ⟶ S) (q' : Y' ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (gf₁ : Y' ⟶ X i₁) (gf₂ : Y' ⟶ X i₂) (hq : CategoryStruct.comp g q = q' := by cat_disch) (hf₁ : CategoryStruct.comp f₁ (f i₁) = q := by cat_disch) (hf₂ : CategoryStruct.comp f₂ (f i₂) = q := by cat_disch) (hgf₁ : CategoryStruct.comp g f₁ = gf₁ := by cat_disch) (hgf₂ : CategoryStruct.comp g f₂ = gf₂ := by cat_disch) {Z : ↑(F.obj { as := Opposite.op Y' })} (h : (F.map gf₂.op.toLoc).toFunctor.obj (obj' i₂) ⟶ Z) : CategoryStruct.comp (LocallyDiscreteOpToCat.pullHom (pullHom' hom q f₁ f₂ hf₁ hf₂) g gf₁ gf₂ ⋯ ⋯) h = CategoryStruct.comp (pullHom' hom q' gf₁ gf₂ ⋯ ⋯) h

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData'.pullHom'_p₁_p₂ {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {obj : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })} (hom : (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj j)) (i₁ i₂ : ι) : pullHom' hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯ = hom i₁ i₂

theorem CategoryTheory.Pseudofunctor.DescentData'.pullHom'_self' {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {obj : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })} (hom : (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj j)) (hom_self : ∀ (i : ι), pullHom' hom (f i) (CategoryStruct.id (X i)) (CategoryStruct.id (X i)) ⋯ ⋯ = CategoryStruct.id ((F.map (CategoryStruct.id (X i)).op.toLoc).toFunctor.obj (obj i))) ⦃Y : C⦄ (q : Y ⟶ S) ⦃i : ι⦄ (g : Y ⟶ X i) (hg : CategoryStruct.comp g (f i) = q := by cat_disch) : pullHom' hom q g g hg hg = CategoryStruct.id ((F.map g.op.toLoc).toFunctor.obj (obj i))

theorem CategoryTheory.Pseudofunctor.DescentData'.comp_pullHom'' {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} {obj : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })} (hom : (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj j)) (hom_comp : ∀ (i₁ i₂ i₃ : ι), CategoryStruct.comp (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯) (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) = pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) ⦃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 (pullHom' hom q f₁ f₂ ⋯ ⋯) (pullHom' hom q f₂ f₃ ⋯ ⋯) = pullHom' hom q f₁ f₃ ⋯ ⋯

theorem CategoryTheory.Pseudofunctor.DescentData'.comp_pullHom''_assoc {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} {obj : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })} (hom : (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj j)) (hom_comp : ∀ (i₁ i₂ i₃ : ι), CategoryStruct.comp (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯) (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) = pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) ⦃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 (obj i₃) ⟶ Z) : CategoryStruct.comp (pullHom' hom q f₁ f₂ ⋯ ⋯) (CategoryStruct.comp (pullHom' hom q f₂ f₃ ⋯ ⋯) h) = CategoryStruct.comp (pullHom' hom q f₁ f₃ ⋯ ⋯) h

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} (sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)) (sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) : Type (max (max t u') v')

Given a pseudofunctor F from LocallyDiscrete Cᵒᵖ to Cat, a family of morphisms f i : X i ⟶ S, chosen pullbacks sq i j of f i and f j for all i and j, and chosen threefold wide pullbacks sq₃, this structure contains a description of objects over the X i equipped with a descent data relative to the morphisms f i, where the (iso)morphisms are compatibilities are considered over the chosen pullbacks.

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

  The objects over X i for all i

• hom (i j : ι) : (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (self.obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (self.obj j)

  The compatibility morphisms after pulling back to the chosen pullbacks. It follows from the conditions pullHom'_hom_self and pullHom'_hom_comp that these morphisms are isomorphisms.

• pullHom'_hom_self (i : ι) : pullHom' self.hom (f i) (CategoryStruct.id (X i)) (CategoryStruct.id (X i)) ⋯ ⋯ = CategoryStruct.id ((F.map (CategoryStruct.id (X i)).op.toLoc).toFunctor.obj (self.obj i))
• pullHom'_hom_comp (i₁ i₂ i₃ : ι) : CategoryStruct.comp (pullHom' self.hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯) (pullHom' self.hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) = pullHom' self.hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯

theorem CategoryTheory.Pseudofunctor.DescentData'.pullHom'_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} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} (self : F.DescentData' sq sq₃) (i₁ i₂ i₃ : ι) {Z : ↑(F.obj { as := Opposite.op (sq₃ i₁ i₂ i₃).chosenPullback.pullback })} (h : (F.map (sq₃ i₁ i₂ i₃).p₃.op.toLoc).toFunctor.obj (self.obj i₃) ⟶ Z) : CategoryStruct.comp (pullHom' self.hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯) (CategoryStruct.comp (pullHom' self.hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) h) = CategoryStruct.comp (pullHom' self.hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) h

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData'.pullHom'_self {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} (D : F.DescentData' sq sq₃) ⦃Y : C⦄ (q : Y ⟶ S) ⦃i : ι⦄ (g : Y ⟶ X i) (hg : CategoryStruct.comp g (f i) = q := by cat_disch) : pullHom' D.hom q g g hg hg = CategoryStruct.id ((F.map g.op.toLoc).toFunctor.obj (D.obj i))

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData'.comp_pullHom' {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} (D : F.DescentData' sq sq₃) ⦃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 := by cat_disch) (hf₂ : CategoryStruct.comp f₂ (f i₂) = q := by cat_disch) (hf₃ : CategoryStruct.comp f₃ (f i₃) = q := by cat_disch) : CategoryStruct.comp (pullHom' D.hom q f₁ f₂ hf₁ hf₂) (pullHom' D.hom q f₂ f₃ hf₂ hf₃) = pullHom' D.hom q f₁ f₃ hf₁ hf₃

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData'.comp_pullHom'_assoc {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} (D : F.DescentData' sq sq₃) ⦃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 := by cat_disch) (hf₂ : CategoryStruct.comp f₂ (f i₂) = q := by cat_disch) (hf₃ : CategoryStruct.comp f₃ (f i₃) = q := by cat_disch) {Z : ↑(F.obj { as := Opposite.op Y })} (h : (F.map f₃.op.toLoc).toFunctor.obj (D.obj i₃) ⟶ Z) : CategoryStruct.comp (pullHom' D.hom q f₁ f₂ hf₁ hf₂) (CategoryStruct.comp (pullHom' D.hom q f₂ f₃ hf₂ hf₃) h) = CategoryStruct.comp (pullHom' D.hom q f₁ f₃ hf₁ hf₃) h

instance CategoryTheory.Pseudofunctor.DescentData'.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullHom'Hom {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} (D : F.DescentData' sq sq₃) {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 (pullHom' D.hom q f₁ f₂ hf₁ hf₂)

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

instance CategoryTheory.Pseudofunctor.DescentData'.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullbackHom {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} (D : F.DescentData' sq sq₃) (i₁ i₂ : ι) : IsIso (D.hom i₁ i₂)

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} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} (D₁ D₂ : F.DescentData' sq sq₃) : Type (max t v')

The type of morphisms in the category F.DescentData' sq sq₃.

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

  The morphisms between the obj fields of descent data.

• comm (i₁ i₂ : ι) : CategoryStruct.comp ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (self.hom i₁)) (D₂.hom i₁ i₂) = CategoryStruct.comp (D₁.hom i₁ i₂) ((F.map (sq i₁ i₂).p₂.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} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} {D₁ D₂ : F.DescentData' sq sq₃} {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} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} {D₁ D₂ : F.DescentData' sq sq₃} {x y : D₁.Hom D₂} : x = y ↔ x.hom = y.hom

@[simp]

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} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} {D₁ D₂ : F.DescentData' sq sq₃} (self : D₁.Hom D₂) (i₁ i₂ : ι) {Z : ↑(F.obj { as := Opposite.op (sq i₁ i₂).pullback })} (h : (F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.obj (D₂.obj i₂) ⟶ Z) : CategoryStruct.comp ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (self.hom i₁)) (CategoryStruct.comp (D₂.hom i₁ i₂) h) = CategoryStruct.comp (D₁.hom i₁ i₂) (CategoryStruct.comp ((F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (self.hom i₂)) h)

@[implicit_reducible]

instance CategoryTheory.Pseudofunctor.DescentData'.instQuiver {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} : Quiver (F.DescentData' sq sq₃)

Equations

• CategoryTheory.Pseudofunctor.DescentData'.instQuiver = { Hom := CategoryTheory.Pseudofunctor.DescentData'.Hom }

@[implicit_reducible]

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} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} : Category.{max t v', max (max u' v') t} (F.DescentData' sq sq₃)

Equations

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

@[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} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} (x✝ : F.DescentData' sq sq₃) (x✝¹ : ι) : (CategoryStruct.id x✝).hom x✝¹ = CategoryStruct.id (x✝.obj x✝¹)

@[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} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} {X✝ Y✝ Z✝ : F.DescentData' sq sq₃} (f✝ : X✝ ⟶ Y✝) (g : Y✝ ⟶ Z✝) (i : ι) : (CategoryStruct.comp f✝ g).hom i = CategoryStruct.comp (f✝.hom i) (g.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} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} {X✝ Y✝ Z✝ : F.DescentData' sq sq₃} (f✝ : X✝ ⟶ Y✝) (g : Y✝ ⟶ Z✝) (i : ι) {Z : ↑(F.obj { as := Opposite.op (X i) })} (h : Z✝.obj i ⟶ Z) : CategoryStruct.comp ((CategoryStruct.comp f✝ g).hom i) h = CategoryStruct.comp (f✝.hom i) (CategoryStruct.comp (g.hom i) h)

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} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} {D₁ D₂ : F.DescentData' sq sq₃} {f✝ g : D₁ ⟶ D₂} (h : ∀ (i : ι), f✝.hom i = g.hom i) : f✝ = g

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} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} {D₁ D₂ : F.DescentData' sq sq₃} {f✝ g : D₁ ⟶ D₂} : f✝ = g ↔ ∀ (i : ι), f✝.hom i = g.hom i

theorem CategoryTheory.Pseudofunctor.DescentData'.comm {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} {D₁ D₂ : F.DescentData' sq sq₃} (φ : D₁ ⟶ D₂) ⦃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) : CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (φ.hom i₁)) (pullHom' D₂.hom q f₁ f₂ hf₁ hf₂) = CategoryStruct.comp (pullHom' D₁.hom q f₁ f₂ hf₁ hf₂) ((F.map f₂.op.toLoc).toFunctor.map (φ.hom i₂))

theorem CategoryTheory.Pseudofunctor.DescentData'.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} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} {D₁ D₂ : F.DescentData' sq sq₃} (φ : D₁ ⟶ D₂) ⦃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) {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 (φ.hom i₁)) (CategoryStruct.comp (pullHom' D₂.hom q f₁ f₂ hf₁ hf₂) h) = CategoryStruct.comp (pullHom' D₁.hom q f₁ f₂ hf₁ hf₂) (CategoryStruct.comp ((F.map f₂.op.toLoc).toFunctor.map (φ.hom i₂)) h)

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} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} {D₁ D₂ : F.DescentData' sq sq₃} (e : (i : ι) → D₁.obj i ≅ D₂.obj i) (comm : ∀ (i₁ i₂ : ι), CategoryStruct.comp ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (e i₁).hom) (D₂.hom i₁ i₂) = CategoryStruct.comp (D₁.hom i₁ i₂) ((F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (e i₂).hom) := by cat_disch) : D₁ ≅ D₂

Constructor for isomorphisms in the category F.DescentData' sq sq₃.

Equations

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

@[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} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} {D₁ D₂ : F.DescentData' sq sq₃} (e : (i : ι) → D₁.obj i ≅ D₂.obj i) (comm : ∀ (i₁ i₂ : ι), CategoryStruct.comp ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (e i₁).hom) (D₂.hom i₁ i₂) = CategoryStruct.comp (D₁.hom i₁ i₂) ((F.map (sq i₁ i₂).p₂.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} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} {D₁ D₂ : F.DescentData' sq sq₃} (e : (i : ι) → D₁.obj i ≅ D₂.obj i) (comm : ∀ (i₁ i₂ : ι), CategoryStruct.comp ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (e i₁).hom) (D₂.hom i₁ i₂) = CategoryStruct.comp (D₁.hom i₁ i₂) ((F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (e i₂).hom) := by cat_disch) (i : ι) : (isoMk e comm).hom.hom i = (e i).hom

noncomputable def CategoryTheory.Pseudofunctor.DescentData'.descentData {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} (D : F.DescentData' sq sq₃) : F.DescentData f

The functor toDescentDataFunctor : F.DescentData' sq sq₃ ⥤ F.DescentData f, on objects.

Equations

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

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData'.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} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} (D : F.DescentData' sq sq₃) (x✝ : C) (x✝¹ : x✝ ⟶ S) (x✝² x✝³ : ι) (x✝⁴ : x✝ ⟶ X x✝²) (x✝⁵ : x✝ ⟶ X x✝³) (x✝⁶ : CategoryStruct.comp x✝⁴ (f x✝²) = x✝¹) (x✝⁷ : CategoryStruct.comp x✝⁵ (f x✝³) = x✝¹) : D.descentData.hom x✝¹ x✝⁴ x✝⁵ x✝⁶ x✝⁷ = pullHom' D.hom (CategoryStruct.comp x✝⁴ (f x✝²)) x✝⁴ x✝⁵ ⋯ ⋯

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData'.descentData_obj {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)} {sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} (D : F.DescentData' sq sq₃) (i : ι) : D.descentData.obj i = D.obj i

def CategoryTheory.Pseudofunctor.DescentData'.ofDescentData {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)) (sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) (D : F.DescentData f) : F.DescentData' sq sq₃

The functor fromDescentDataFunctor : F.DescentData f ⥤ F.DescentData' sq sq₃, on objects.

Equations

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

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData'.ofDescentData_obj {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)) (sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) (D : F.DescentData f) (i : ι) : (ofDescentData sq sq₃ D).obj i = D.obj i

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData'.ofDescentData_hom {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)) (sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) (D : F.DescentData f) (i₁ i₂ : ι) : (ofDescentData sq sq₃ D).hom i₁ i₂ = D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData'.pullHom'_ofDescentData_hom {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)) (sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) (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) : pullHom' (ofDescentData sq sq₃ D).hom q f₁ f₂ hf₁ hf₂ = D.hom q f₁ f₂ hf₁ hf₂

noncomputable def CategoryTheory.Pseudofunctor.DescentData'.toDescentDataFunctor {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)) (sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) : Functor (F.DescentData' sq sq₃) (F.DescentData f)

The functor F.DescentData' sq sq₃ ⥤ F.DescentData f.

Equations

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

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData'.toDescentDataFunctor_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} (sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)) (sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) {X✝ Y✝ : F.DescentData' sq sq₃} (φ : X✝ ⟶ Y✝) (i : ι) : ((toDescentDataFunctor F sq sq₃).map φ).hom i = φ.hom i

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData'.toDescentDataFunctor_obj {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)) (sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) (D : F.DescentData' sq sq₃) : (toDescentDataFunctor F sq sq₃).obj D = D.descentData

noncomputable def CategoryTheory.Pseudofunctor.DescentData'.fromDescentDataFunctor {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)) (sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) : Functor (F.DescentData f) (F.DescentData' sq sq₃)

The functor F.DescentData f ⥤ F.DescentData' sq sq₃.

Equations

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

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData'.fromDescentDataFunctor_obj {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)) (sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) (D : F.DescentData f) : (fromDescentDataFunctor F sq sq₃).obj D = ofDescentData sq sq₃ D

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData'.fromDescentDataFunctor_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} (sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)) (sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) {X✝ Y✝ : F.DescentData f} (φ : X✝ ⟶ Y✝) (i : ι) : ((fromDescentDataFunctor F sq sq₃).map φ).hom i = φ.hom i

noncomputable def CategoryTheory.Pseudofunctor.DescentData'.descentDataEquivalence {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)) (sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) : F.DescentData' sq sq₃ ≌ F.DescentData f

The equivalence F.DescentData' sq sq₃ ≌ F.DescentData f.

Equations

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

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData'.descentDataEquivalence_counitIso {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)) (sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) : (descentDataEquivalence F sq sq₃).counitIso = NatIso.ofComponents (fun (D : F.DescentData f) => DescentData.isoMk (fun (x : ι) => Iso.refl ((((fromDescentDataFunctor F sq sq₃).comp (toDescentDataFunctor F sq sq₃)).obj D).obj x)) ⋯) ⋯

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData'.descentDataEquivalence_functor {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)) (sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) : (descentDataEquivalence F sq sq₃).functor = toDescentDataFunctor F sq sq₃

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData'.descentDataEquivalence_inverse {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)) (sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) : (descentDataEquivalence F sq sq₃).inverse = fromDescentDataFunctor F sq sq₃

@[simp]

theorem CategoryTheory.Pseudofunctor.DescentData'.descentDataEquivalence_unitIso {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → Limits.ChosenPullback (f i) (f j)) (sq₃ : (i₁ i₂ i₃ : ι) → Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) : (descentDataEquivalence F sq sq₃).unitIso = NatIso.ofComponents (fun (D : F.DescentData' sq sq₃) => isoMk (fun (x : ι) => Iso.refl (((Functor.id (F.DescentData' sq sq₃)).obj D).obj x)) ⋯) ⋯