Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom.congr_simp

∀ {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 p_1 : S' ⟶ S} (e_p : p = p_1) {ι' : Type t'} {X' : ι' → C}
  {f' f'_1 : (j : ι') → X' j ⟶ S'} (e_f' : f' = f'_1) {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)}
  (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.CategoryStruct.comp (f' j) p)
  (D : F.DescentData f) ⦃Y : C⦄ (q q_1 : Y ⟶ S') (e_q : q = q_1) ⦃j₁ j₂ : ι'⦄ (f₁ : Y ⟶ X' j₁) (f₂ : Y ⟶ X' j₂)
  (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f' j₁) = q) (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f' j₂) = q),
  CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom w D q f₁ f₂ hf₁ hf₂ =
    CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom ⋯ D q_1 f₁ f₂ ⋯ ⋯

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentData

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category