Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.DescentData.hom_comp

∀ {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₂ i₃ : ι⦄ (f₁ : Y ⟶ X 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) (hf₃ : CategoryTheory.CategoryStruct.comp f₃ (f i₃) = q),
  CategoryTheory.CategoryStruct.comp (self.hom q f₁ f₂ hf₁ hf₂) (self.hom q f₂ f₃ hf₂ hf₃) = self.hom q f₁ f₃ hf₁ hf₃

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentData

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category