Theorems · Theorem · category theory

CategoryTheory.Precoverage.small_subsheafify_of_small

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)},
  (∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor F R) →
    ∀ (𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))),
      (∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)) →
        CategoryTheory.FunctorToTypes.Small.{max u v, w, v, u} (K.subsheafify 𝒮).toFunctor

If 𝒮 Z is max u v-small for every Z, then the subsheaf generated by 𝒮 Z has max u v-small sections.

Defined in

Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category