FamilyOfElements — Mathlib

Lean4
/-- A family of elements for a presheaf `P` given a collection of arrows `R` with fixed codomain `X`
consists of an element of `P Y` for every `f : Y ⟶ X` in `R`.
A presheaf is a sheaf (resp, separated) if every *compatible* family of elements has exactly one
(resp, at most one) amalgamation.

This data is referred to as a `family` in [MM92], Chapter III, Section 4. It is also a concrete
version of the elements of the middle object in the Stacks entry which is
more useful for direct calculations. It is also used implicitly in Definition C2.1.2 in [Elephant].
-/
@[stacks 00VM "This is a concrete version of the elements of the middle object there."]
def FamilyOfElements (P : Cᵒᵖ ⥤ Type w) (R : Presieve X) :=
  ∀ ⦃Y : C⦄ (f : Y ⟶ X), R f → P.obj (op Y)
Похожие утверждения