Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.DescentData.Hom.mk.inj

∀ {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} {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_1 : (i : ι) → D₁.obj i ⟶ D₂.obj i}
  {comm_1 :
    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_1 i₁)) (D₂.hom q f₁ f₂ ⋯ ⋯) =
          CategoryTheory.CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯) ((F.map f₂.op.toLoc).toFunctor.map (hom_1 i₂)))
      CategoryTheory.Pseudofunctor.DescentData.Hom.comm._autoParam},
  { hom := hom, comm := comm } = { hom := hom_1, comm := comm_1 } → hom = hom_1

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentData

Cited by

1 results in Mathlib

Foundations

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