Theorems · Definition · category theory

CategoryTheory.Pseudofunctor.DescentData.Hom.mk.noConfusion

{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} →
              {D₁ D₂ : F.DescentData f} →
                {P : Sort u_1} →
                  {hom : (i : ι) → D₁.obj i ⟶ D₂.obj i} →
                    {comm :
                        autoParam
                          (∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂)
                            (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
                            (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q),
                            CategoryTheory.CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (hom i₁))
                                (D₂.hom q f₁ f₂ ⋯ ⋯) =
                              CategoryTheory.CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯)
                                ((F.map f₂.op.toLoc).toFunctor.map (hom i₂)))
                          CategoryTheory.Pseudofunctor.DescentData.Hom.comm._autoParam} →
                      {hom' : (i : ι) → D₁.obj i ⟶ D₂.obj i} →
                        {comm' :
                            autoParam
                              (∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂)
                                (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
                                (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q),
                                CategoryTheory.CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (hom' i₁))
                                    (D₂.hom q f₁ f₂ ⋯ ⋯) =
                                  CategoryTheory.CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯)
                                    ((F.map f₂.op.toLoc).toFunctor.map (hom' i₂)))
                              CategoryTheory.Pseudofunctor.DescentData.Hom.comm._autoParam} →
                          { hom := hom, comm := comm } = { hom := hom', comm := comm' } → (hom ≍ hom' → P) → P

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentData

Cited by

1 results in Mathlib

Foundations

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