mathlib documentation

category_theory.category.pairwise

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 : single i ⟶ pair i j and right : single j ⟶ pair i j.

We use this later in describing 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 limit cone over this functor.

source
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.

source
@[instance]
def category_theory.pairwise.pairwise_inhabited {ι : Type v} [inhabited ι] :
inhabited (category_theory.pairwise ι)

Equations
source
inductive category_theory.pairwise.hom {ι : Type v} (a a_1 : category_theory.pairwise ι) :
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.

source
@[instance]
def category_theory.pairwise.hom_inhabited {ι : Type v} [inhabited ι] :
inhabited ((category_theory.pairwise.single (default ι)).hom (category_theory.pairwise.single (default ι)))

Equations
source
def category_theory.pairwise.id {ι : Type v} (o : category_theory.pairwise ι) :
o.hom o

The identity morphism in pairwise ι.

Equations
source
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
source
@[instance]
def category_theory.pairwise.category_theory.category {ι : Type v} :
category_theory.category (category_theory.pairwise ι)

Equations
source
@[simp]
def category_theory.pairwise.diagram_obj {ι α : Type v} (U : ι → α) [semilattice_inf α] (a : category_theory.pairwise ι) :
αᵒᵖ

Auxilliary definition for diagram.

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

Auxilliary definition for diagram.

Equations
source
@[simp]
theorem category_theory.pairwise.diagram_obj_2 {ι α : Type v} (U : ι → α) [semilattice_inf α] (a : category_theory.pairwise ι) :
(category_theory.pairwise.diagram U).obj a = category_theory.pairwise.diagram_obj U a

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

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

Equations
source
@[simp]
theorem category_theory.pairwise.diagram_map_2 {ι α : Type v} (U : ι → α) [semilattice_inf α] (X Y : category_theory.pairwise ι) (f : X ⟶ Y) :
(category_theory.pairwise.diagram U).map f = category_theory.pairwise.diagram_map U f

source
def category_theory.pairwise.cone_π_app {ι α : Type v} (U : ι → α) [complete_lattice α] (o : category_theory.pairwise ι) :
opposite.op (supr U) ⟶ category_theory.pairwise.diagram_obj U o

Auxilliary definition for cone.

Equations
source
def category_theory.pairwise.cone {ι α : Type v} (U : ι → α) [complete_lattice α] :
category_theory.limits.cone (category_theory.pairwise.diagram U)

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

Equations
source
@[simp]
theorem category_theory.pairwise.cone_X {ι α : Type v} (U : ι → α) [complete_lattice α] :
(category_theory.pairwise.cone U).X = opposite.op (supr U)

source
@[simp]
theorem category_theory.pairwise.cone_π_app_2 {ι α : Type v} (U : ι → α) [complete_lattice α] (o : category_theory.pairwise ι) :
(category_theory.pairwise.cone U).π.app o = category_theory.pairwise.cone_π_app U o

source
def category_theory.pairwise.cone_is_limit {ι α : Type v} (U : ι → α) [complete_lattice α] :
category_theory.limits.is_limit (category_theory.pairwise.cone U)

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

Equations