Theorems · Definition · category theory

CategoryTheory.Presheaf.imageSieve

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} A] →
        {FA : A → A → Type u_1} →
          {CA : A → Type w'} →
            [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] →
              [inst_3 : CategoryTheory.ConcreteCategory A FA] →
                {F G : CategoryTheory.Functor Cᵒᵖ A} →
                  (F ⟶ G) → {U : C} → CategoryTheory.ToType (G.obj (Opposite.op U)) → CategoryTheory.Sieve U

Given f : F ⟶ G, a morphism between presieves, and s : G.obj (op U), this is the sieve of U consisting of the i : V ⟶ U such that s restricted along i is in the image of f.

Defined in

Mathlib.CategoryTheory.Sites.LocallySurjective

Cited by

30 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategory