Theorems · Definition · category theory

CategoryTheory.Presieve.FamilyOfElements.Compatible

{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 → Prop

A family of elements for the arrow set R is compatible if for any f₁ : Y₁ ⟶ X and f₂ : Y₂ ⟶ X in R, and any g₁ : Z ⟶ Y₁ and g₂ : Z ⟶ Y₂, if the square g₁ ≫ f₁ = g₂ ≫ f₂ commutes then the elements of P Z obtained by restricting the element of P Y₁ along g₁ and restricting the element of P Y₂ along g₂ are the same. In special cases, this condition can be simplified, see pullbackCompatible_iff and compatible_iff_sieveCompatible. This is referred to as a "compatible family" in Definition C2.1.2 of [Elephant], and on nlab: https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents For a more explicit version in the case where R is of the form Presieve.ofArrows, see CategoryTheory.Presieve.Arrows.Compatible.

Defined in

Mathlib.CategoryTheory.Sites.IsSheafFor

Cited by

79 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category