Theorems · Definition · category theory

CategoryTheory.Pseudofunctor.DescentData.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} →
              (self : F.DescentData f) →
                ⦃Y : C⦄ →
                  (q : Y ⟶ S) →
                    ⦃i₁ i₂ : ι⦄ →
                      (f₁ : Y ⟶ X i₁) →
                        (f₂ : Y ⟶ X i₂) →
                          autoParam (CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
                              CategoryTheory.Pseudofunctor.DescentData._auto_1 →
                            autoParam (CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
                                CategoryTheory.Pseudofunctor.DescentData._auto_3 →
                              ((F.map f₁.op.toLoc).toFunctor.obj (self.obj i₁) ⟶
                                (F.map f₂.op.toLoc).toFunctor.obj (self.obj i₂))

The compatibility morphisms after pullbacks. It follows from the conditions hom_self and hom_comp that these are isomorphisms, see CategoryTheory.Pseudofunctor.DescentData.iso below.

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentData

Cited by

28 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category