Theorems · Definition · category theory

CategoryTheory.Presheaf.homEquivAmalgamation

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {P : CategoryTheory.Functor Cᵒᵖ A} →
          {X : C} →
            {S : CategoryTheory.Sieve X} →
              {E : Aᵒᵖ} →
                {x : CategoryTheory.Presieve.FamilyOfElements (P.comp (CategoryTheory.coyoneda.obj E)) S.arrows} →
                  (hx : x.SieveCompatible) → (hx.cone ⟶ P.mapCone S.arrows.cocone.op) ≃ { t // x.IsAmalgamation t }

Cone morphisms from the cone corresponding to a SieveCompatible family to the natural cone associated to a sieve S and a presheaf P are in 1-1 correspondence with amalgamations of the family.

Defined in

Mathlib.CategoryTheory.Sites.Sheaf

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category