Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.DescentData.faithful_pullFunctor

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat)
  {J : CategoryTheory.GrothendieckTopology C} [F.IsPrestack J] {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S}
  {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)}
  (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = f' j),
  CategoryTheory.Sieve.ofArrows X' f' ∈ J S → (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).Faithful

Defined in

Mathlib.CategoryTheory.Sites.Descent.Precoverage

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Pseudofunctor.IsPrestack