Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq_assoc

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.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 : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.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₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f₁ (f' j₁) = q)
      CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq._auto_1)
  (hf₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f₂ (f' j₂) = q)
      CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq._auto_3)
  (hq' :
    autoParam (CategoryTheory.CategoryStruct.comp q p = q')
      CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq._auto_5)
  (hf₁' :
    autoParam (CategoryTheory.CategoryStruct.comp f₁ (p' j₁) = f₁')
      CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq._auto_7)
  (hf₂' :
    autoParam (CategoryTheory.CategoryStruct.comp f₂ (p' j₂) = f₂')
      CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq._auto_9)
  {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),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom w D q f₁ f₂ ⋯ ⋯) h =
    CategoryTheory.CategoryStruct.comp
      ((F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc f₁'.op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)))
      (CategoryTheory.CategoryStruct.comp (D.hom q' f₁' f₂' ⋯ ⋯)
        (CategoryTheory.CategoryStruct.comp
          ((F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc f₂'.op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₂))) h))

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentData

Cited by

0 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category