Compatible families over a terminal object, and over a meet-semilattice

For a family of maps π i : X i ⟶ B to a terminal object B, every pair of maps into two members of the family agrees after composing with π. So a family of elements x i ∈ P(X i) of a presheaf of types P is compatible exactly when, for every pair k : Fin 2 → I, the restrictions of x (k 0) and x (k 1) to the product of X (k 0) and X (k 1) agree. This is the form the compatibility condition takes in degree 1 of the Čech complex.

In a meet-semilattice, such as the opens of a topological space, there is at most one morphism between two objects, and two members X i, X j of a family have the greatest lower bound X i ⊓ X j. So a family of elements is compatible exactly when the restrictions of x i and x j to X i ⊓ X j agree.

Main results

• CategoryTheory.Presieve.Arrows.compatible_iff_of_isTerminal: the characterisation above.
• CategoryTheory.Presieve.Arrows.compatible_homOfLE_iff: compatibility in a meet-semilattice is agreement on pairwise meets.

theorem CategoryTheory.Presieve.Arrows.compatible_iff_of_isTerminal {C : Type u} [Category.{v, u} C] [Limits.HasProductsOfShape (Fin 2) C] {P : Functor Cᵒᵖ (Type w)} {I : Type t} {X : I → C} {B : C} (hB : Limits.IsTerminal B) (π : (i : I) → X i ⟶ B) (x : (i : I) → P.obj (Opposite.op (X i))) : Compatible P π x ↔ ∀ (k : Fin 2 → I), (ConcreteCategory.hom (P.map (Limits.Pi.π (fun (j : Fin 2) => X (k j)) 1).op)) (x (k 1)) = (ConcreteCategory.hom (P.map (Limits.Pi.π (fun (j : Fin 2) => X (k j)) 0).op)) (x (k 0))

A family of elements indexed by maps π i : X i ⟶ B to a terminal object is compatible exactly when its restrictions agree on the product ∏ᶜ fun j ↦ X (k j) of every pair of members k : Fin 2 → I. Unlike Presieve.Arrows.pullbackCompatible_iff, it needs only products of two objects, and the products are indexed as in the Čech complex CategoryTheory.cechComplexFunctor.

theorem CategoryTheory.Presieve.Arrows.compatible_homOfLE_iff {X : Type u} [SemilatticeInf X] {P : Functor Xᵒᵖ (Type w)} {I : Type t} {Y : I → X} {B : X} (hY : ∀ (i : I), Y i ≤ B) (x : (i : I) → P.obj (Opposite.op (Y i))) : Compatible P (fun (i : I) => homOfLE ⋯) x ↔ ∀ (i j : I), (ConcreteCategory.hom (P.map (homOfLE ⋯).op)) (x i) = (ConcreteCategory.hom (P.map (homOfLE ⋯).op)) (x j)

Compatibility in a meet-semilattice is agreement on pairwise meets. For members Y i ≤ B of a meet-semilattice, such as opens of a topological space, a family of elements x i ∈ P(Y i) of a presheaf of types is compatible exactly when, for all i and j, the restrictions of x i and x j to Y i ⊓ Y j agree.