Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.isPrestackFor_iff_isSheafFor

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C}
  (R : CategoryTheory.Sieve S),
  F.IsPrestackFor R.arrows ↔
    ∀ (M N : ↑(F.obj { as := Opposite.op S })),
      CategoryTheory.Presieve.IsSheafFor (F.presheafHom M N)
        ((CategoryTheory.Sieve.overEquiv (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id S))).symm R).arrows

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentData

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category