mathlib3 documentation

category_theory.category.pairwise

The category of "pairwise intersections". #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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) :

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.

Instances for category_theory.pairwise

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.

Instances for category_theory.pairwise.hom

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.

Equations

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

Equations