# 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 iSup U provides a colimit cocone over this functor.

inductive CategoryTheory.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.

• single: {ι : Type v} →
• pair: {ι : Type v} → ιι
Instances For
Equations
• CategoryTheory.Pairwise.pairwiseInhabited = { default := }
inductive CategoryTheory.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.

• id_single: {ι : Type v} → (i : ι) →
• id_pair: {ι : Type v} → (i j : ι) → .Hom
• left: {ι : Type v} → (i j : ι) →
• right: {ι : Type v} → (i j : ι) →
Instances For
Equations
• CategoryTheory.Pairwise.homInhabited = { default := }
def CategoryTheory.Pairwise.id {ι : Type v} (o : ) :
o.Hom o

The identity morphism in Pairwise ι.

Equations
Instances For
def CategoryTheory.Pairwise.comp {ι : Type v} {o₁ : } {o₂ : } {o₃ : } :
o₁.Hom o₂o₂.Hom o₃o₁.Hom o₃

Composition of morphisms in Pairwise ι.

Equations
Instances For

A helper tactic for aesop_cat and Pairwise.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• CategoryTheory.Pairwise.instCategory =
def CategoryTheory.Pairwise.diagramObj {ι : Type v} {α : Type v} (U : ια) [] :

Auxiliary definition for diagram.

Equations
Instances For
def CategoryTheory.Pairwise.diagramMap {ι : Type v} {α : Type v} (U : ια) [] {o₁ : } {o₂ : } :
(o₁ o₂)

Auxiliary definition for diagram.

Equations
Instances For
@[simp]
theorem CategoryTheory.Pairwise.diagram_map {ι : Type v} {α : Type v} (U : ια) [] :
∀ {X Y : } (x : X Y),
@[simp]
theorem CategoryTheory.Pairwise.diagram_obj {ι : Type v} {α : Type v} (U : ια) [] :
∀ (a : ),
def CategoryTheory.Pairwise.diagram {ι : Type v} {α : Type v} (U : ια) [] :

Given a function U : ι → α for [SemilatticeInf α], 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
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Pairwise.coconeιApp {ι : Type v} {α : Type v} (U : ια) [] (o : ) :

Auxiliary definition for cocone.

Equations
Instances For
@[simp]
theorem CategoryTheory.Pairwise.cocone_ι_app {ι : Type v} {α : Type v} (U : ια) [] (o : ) :
@[simp]
theorem CategoryTheory.Pairwise.cocone_pt {ι : Type v} {α : Type v} (U : ια) [] :
= iSup U
def CategoryTheory.Pairwise.cocone {ι : Type v} {α : Type v} (U : ια) [] :

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

Equations
• = { pt := iSup U, ι := { app := , naturality := } }
Instances For
def CategoryTheory.Pairwise.coconeIsColimit {ι : Type v} {α : Type v} (U : ια) [] :

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

Equations
• = { desc := , fac := , uniq := }
Instances For