Theorems · Definition · category theory

CategoryTheory.Presieve.shrinkFunctorHomEquiv

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      {S : CategoryTheory.Sieve X} →
        [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] →
          {F : CategoryTheory.Functor Cᵒᵖ (Type w)} →
            ((CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F) ≃ { x // x.Compatible }

(Implementation). This is a (primarily internal) equivalence between natural transformations and compatible families. Cf the discussion after Lemma 7.47.10 in <https://stacks.math.columbia.edu/tag/00YW>. See also the proof of C2.1.4 of [Elephant], and the discussion in [MM92], Chapter III, Section 4.

Defined in

Mathlib.CategoryTheory.Sites.IsSheafFor

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.LocallySmall