mathlib documentation


The category of "pairwise intersections".

Given ι : Type v, we build the diagram category pairwise ι with objects single i and pair i j, for i j : ι, whose only non-identity morphisms are left : pair i j ⟶ single i and right : pair i j ⟶ single j.

We use this later in describing (one formulation of) the sheaf condition.

Given any function U : ι → α, where α is some complete lattice (e.g. (opens X)ᵒᵖ), we produce a functor pairwise ι ⥤ α in the obvious way, and show that supr U provides a colimit cocone over this functor.

inductive category_theory.pairwise (ι : Type v) :
Type v

An inductive type representing either a single term of a type ι, or a pair of terms. We use this as the objects of a category to describe the sheaf condition.

inductive category_theory.pairwise.hom {ι : Type v} :

Morphisms in the category pairwise ι. The only non-identity morphisms are left i j : single i ⟶ pair i j and right i j : single j ⟶ pair i j.

def category_theory.pairwise.diagram_obj {ι α : Type v} (U : ι → α) [semilattice_inf α] :

Auxilliary definition for diagram.

def category_theory.pairwise.diagram {ι α : Type v} (U : ι → α) [semilattice_inf α] :

Given a function U : ι → α for [semilattice_inf α], we obtain a functor pairwise ι ⥤ α, sending single i to U i and pair i j to U i ⊓ U j, and the morphisms to the obvious inequalities.


Given a function U : ι → α for [complete_lattice α], supr U provides a cocone over diagram U.

theorem category_theory.pairwise.cocone_X {ι α : Type v} (U : ι → α) [complete_lattice α] :