Theorems · Theorem · category theory

CategoryTheory.Presheaf.imageSieve_cofanIsColimitDesc_shrinkYoneda_map

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {ι : Type u_2} [Small.{w, u_2} ι] {X : ι → C}
  (f : (i : ι) → X i ⟶ S) [inst_2 : CategoryTheory.LocallySmall.{w, v, u} C]
  {c : CategoryTheory.Limits.Cofan fun i => CategoryTheory.shrinkYoneda.{w, v, u}.obj (X i)}
  (hc : CategoryTheory.Limits.IsColimit c) {U : C} (g : U ⟶ S),
  CategoryTheory.Presheaf.imageSieve
      (CategoryTheory.Limits.Cofan.IsColimit.desc hc fun i => CategoryTheory.shrinkYoneda.{w, v, u}.map (f i))
      (CategoryTheory.shrinkYonedaObjObjEquiv.symm g) =
    CategoryTheory.Sieve.pullback g (CategoryTheory.Sieve.ofArrows X f)

Defined in

Mathlib.CategoryTheory.Sites.LocallySurjective

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategorySmallCategoryTheory.LocallySmall