Theorems · Definition · category theory

CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso

{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} →
              CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯ ≅ CategoryTheory.Functor.id (F.DescentData f)

The functor F.DescentData f ⥤ F.DescentData f corresponding to pullFunctor applied to identity morphisms is isomorphic to the identity functor.

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentData

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category