# mathlib3documentation

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
@[protected, instance]
Equations
inductive category_theory.pairwise.hom {ι : Type v} :
• id_single : Π {ι : Type v} (i : ι),
• id_pair : Π {ι : Type v} (i j : ι),
• left : Π {ι : Type v} (i j : ι),
• right : Π {ι : Type v} (i j : ι),

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
@[protected, instance]
Equations

The identity morphism in pairwise ι.

Equations
def category_theory.pairwise.comp {ι : Type v} {o₁ o₂ o₃ : category_theory.pairwise ι} (f : o₁.hom o₂) (g : o₂.hom o₃) :
o₁.hom o₃

Composition of morphisms in pairwise ι.

Equations
@[protected, instance]
Equations
@[simp]
def category_theory.pairwise.diagram_obj {ι α : Type v} (U : ι α)  :

Auxiliary definition for diagram.

Equations
@[simp]
def category_theory.pairwise.diagram_map {ι α : Type v} (U : ι α) {o₁ o₂ : category_theory.pairwise ι} (f : o₁ o₂) :

Auxiliary definition for diagram.

Equations
@[simp]
theorem category_theory.pairwise.diagram_obj_2 {ι α : Type v} (U : ι α) (ᾰ : category_theory.pairwise ι) :
def category_theory.pairwise.diagram {ι α : Type v} (U : ι α)  :

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
@[simp]
theorem category_theory.pairwise.diagram_map_2 {ι α : Type v} (U : ι α) (X Y : category_theory.pairwise ι) (f : X Y) :

Auxiliary definition for cocone.

Equations
def category_theory.pairwise.cocone {ι α : Type v} (U : ι α)  :

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

Equations
@[simp]
theorem category_theory.pairwise.cocone_ι_app_2 {ι α : Type v} (U : ι α) (o : category_theory.pairwise ι) :
@[simp]
theorem category_theory.pairwise.cocone_X {ι α : Type v} (U : ι α)  :
def category_theory.pairwise.cocone_is_colimit {ι α : Type v} (U : ι α)  :

Given a function U : ι → α for [complete_lattice α], infi U provides a limit cone over diagram U.

Equations