Theorems · Definition · category theory

CategoryTheory.Presieve.IsSheafFor.amalgamate

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      {X : C} →
        {R : CategoryTheory.Presieve X} →
          CategoryTheory.Presieve.IsSheafFor P R →
            (x : CategoryTheory.Presieve.FamilyOfElements P R) → x.Compatible → P.obj (Opposite.op X)

Get the amalgamation of the given compatible family, provided we have a sheaf.

Defined in

Mathlib.CategoryTheory.Sites.IsSheafFor

Cited by

14 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category