Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.DescentData.pullFunctorEquivalence_unitIso

∀ {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} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} (e : S' ≅ S)
  {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)}
  (w :
    ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.CategoryStruct.comp (f' j) e.hom)
  {β : ι → ι'} {q' : (i : ι) → X i ⟶ X' (β i)}
  (w' :
    ∀ (i : ι), CategoryTheory.CategoryStruct.comp (q' i) (f' (β i)) = CategoryTheory.CategoryStruct.comp (f i) e.inv),
  (CategoryTheory.Pseudofunctor.DescentData.pullFunctorEquivalence F e w w').unitIso =
    (CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso F S).symm ≪≫
      CategoryTheory.Pseudofunctor.DescentData.pullFunctorIso F ⋯ ⋯ ≪≫
        (CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso F w w' (CategoryTheory.CategoryStruct.id S) ⋯
            ⋯).symm

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentData

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category