Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_hom_app_hom

∀ {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} (X_1 : F.DescentData f) (i : ι),
  ((CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso F S).hom.app X_1).hom i =
    (F.mapId { as := Opposite.op (X i) }).hom.toNatTrans.app (X_1.obj i)

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentData

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category