Theorems · Definition · category theory

CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible

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

Compatible families of elements for a presheaf of types P and a presieve R are in 1-1 correspondence with compatible families for the same presheaf and the sieve generated by R, through extension and restriction.

Defined in

Mathlib.CategoryTheory.Sites.IsSheafFor

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category