Theorems · Definition · category theory

CategoryTheory.Presieve.FamilyOfElements.sieveExtend

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      {X : C} →
        {R : CategoryTheory.Presieve X} →
          CategoryTheory.Presieve.FamilyOfElements P R →
            CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Sieve.generate R).arrows

Extend a family of elements to the sieve generated by an arrow set. This is the construction described as "easy" in Lemma C2.1.3 of [Elephant].

Defined in

Mathlib.CategoryTheory.Sites.IsSheafFor

Cited by

12 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category