Theorems · Definition · category theory

CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom

{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)} →
                            (∀ (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₂) →
                                          autoParam (CategoryTheory.CategoryStruct.comp f₁ (f' j₁) = q)
                                              CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom._auto_1 →
                                            autoParam (CategoryTheory.CategoryStruct.comp f₂ (f' j₂) = q)
                                                CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom._auto_3 →
                                              ((F.map f₁.op.toLoc).toFunctor.obj
                                                  ((F.map (p' j₁).op.toLoc).toFunctor.obj (D.obj (α j₁))) ⟶
                                                (F.map f₂.op.toLoc).toFunctor.obj
                                                  ((F.map (p' j₂).op.toLoc).toFunctor.obj (D.obj (α j₂))))

Auxiliary definition for pullFunctor.

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentData

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category