English
Given a family of arrows π: X_i → B and elements x_i ∈ P(X_i), a family (x_i) is compatible if for all i,j and Z with maps gi: Z → X_i and gj: Z → X_j satisfying gi;π_i = gj;π_j, one has P.map(gi^op)(x_i) = P.map(gj^op)(x_j).
Русский
Пусть есть семейство стрелок π_i: X_i → B и элементы x_i ∈ P(X_i). Назовём совместимым семейство (x_i), если для любых i,j и любых gi: Z → X_i, gj: Z → X_j с gi;π_i = gj;π_j имеет место равенство P.map(gi^op)(x_i) = P.map(gj^op)(x_j).
LaTeX
$${C : Type u₁} → {inst : CategoryTheory.Category C} → {P : CategoryTheory.Functor (Opposite C) (Type w)} → {B : C} → {I : Type u_1} → {X : I → C} → {π : (i : I) → X i ⟶ B} → (x : (i : I) → P.obj (op (X i))) → Prop$$
Lean4
/-- A more explicit version of `FamilyOfElements.Compatible` for a `Presieve.ofArrows`.
-/
def Compatible (x : (i : I) → P.obj (op (X i))) : Prop :=
∀ i j Z (gi : Z ⟶ X i) (gj : Z ⟶ X j), gi ≫ π i = gj ≫ π j → P.map gi.op (x i) = P.map gj.op (x j)
