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) : 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} : ι → Pairwise ι
• pair {ι : Type v} : ι → ι → Pairwise ι

@[implicit_reducible]

instance CategoryTheory.instFintypePairwise {ι✝ : Type u_1} [Fintype ι✝] : Fintype (Pairwise ι✝)

@[implicit_reducible]

instance CategoryTheory.instDecidableEqPairwise {ι✝ : Type u_1} [DecidableEq ι✝] : DecidableEq (Pairwise ι✝)

def CategoryTheory.instDecidableEqPairwise.decEq {ι✝ : Type u_1} [DecidableEq ι✝] (x✝ x✝¹ : Pairwise ι✝) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance CategoryTheory.Pairwise.pairwiseInhabited {ι : Type v} [Inhabited ι] : Inhabited (Pairwise ι)

inductive CategoryTheory.Pairwise.Hom {ι : Type v} : Pairwise ι → 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.

• id_single {ι : Type v} (i : ι) : (single i).Hom (single i)
• id_pair {ι : Type v} (i j : ι) : (pair i j).Hom (pair i j)
• left {ι : Type v} (i j : ι) : (pair i j).Hom (single i)
• right {ι : Type v} (i j : ι) : (pair i j).Hom (single j)

@[implicit_reducible]

instance CategoryTheory.Pairwise.instDecidableEqHom {ι✝ : Type u_1} {a✝ a✝¹ : Pairwise ι✝} [DecidableEq ι✝] : DecidableEq (a✝.Hom a✝¹)

def CategoryTheory.Pairwise.instDecidableEqHom.decEq {ι✝ : Type u_1} {a✝ a✝¹ : Pairwise ι✝} [DecidableEq ι✝] (x✝ x✝¹ : a✝.Hom a✝¹) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance CategoryTheory.Pairwise.homInhabited {ι : Type v} [Inhabited ι] : Inhabited ((single default).Hom (single default))

def CategoryTheory.Pairwise.id {ι : Type v} (o : Pairwise ι) : o.Hom o

The identity morphism in Pairwise ι.

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

Composition of morphisms in Pairwise ι.

@[implicit_reducible]

instance CategoryTheory.Pairwise.instCategoryStruct {ι : Type v} : CategoryStruct.{v, v} (Pairwise ι)

def CategoryTheory.Pairwise.pairwiseCases : Lean.Elab.Tactic.TacticM Unit

A helper tactic for cat_disch and Pairwise.

@[implicit_reducible]

instance CategoryTheory.Pairwise.instCategory {ι : Type v} : Category.{v, v} (Pairwise ι)

@[implicit_reducible]

instance CategoryTheory.Pairwise.instDecidableEqHom_1 {ι : Type v} {i j : Pairwise ι} [DecidableEq ι] : DecidableEq (i ⟶ j)

@[implicit_reducible]

instance CategoryTheory.Pairwise.instFinCategoryOfFintypeOfDecidableEq {ι : Type v} [Fintype ι] [DecidableEq ι] : FinCategory (Pairwise ι)

def CategoryTheory.Pairwise.diagramObj {ι : Type v} {α : Type u} (U : ι → α) [SemilatticeInf α] : Pairwise ι → α

Auxiliary definition for diagram.

def CategoryTheory.Pairwise.diagramMap {ι : Type v} {α : Type u} (U : ι → α) [SemilatticeInf α] {o₁ o₂ : Pairwise ι} : (o₁ ⟶ o₂) → (diagramObj U o₁ ⟶ diagramObj U o₂)

Auxiliary definition for diagram.

def CategoryTheory.Pairwise.diagram {ι : Type v} {α : Type u} (U : ι → α) [SemilatticeInf α] : Functor (Pairwise ι) α

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.

@[simp]

theorem CategoryTheory.Pairwise.diagram_obj {ι : Type v} {α : Type u} (U : ι → α) [SemilatticeInf α] (a✝ : Pairwise ι) : (diagram U).obj a✝ = diagramObj U a✝

@[simp]

theorem CategoryTheory.Pairwise.diagram_map {ι : Type v} {α : Type u} (U : ι → α) [SemilatticeInf α] {X✝ Y✝ : Pairwise ι} (x✝ : X✝ ⟶ Y✝) : (diagram U).map x✝ = diagramMap U x✝

def CategoryTheory.Pairwise.coconeιApp {ι : Type v} {α : Type u} (U : ι → α) [CompleteLattice α] (o : Pairwise ι) : diagramObj U o ⟶ iSup U

Auxiliary definition for cocone.

def CategoryTheory.Pairwise.cocone {ι : Type v} {α : Type u} (U : ι → α) [CompleteLattice α] : Limits.Cocone (diagram U)

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

@[simp]

theorem CategoryTheory.Pairwise.cocone_pt {ι : Type v} {α : Type u} (U : ι → α) [CompleteLattice α] : (cocone U).pt = iSup U

@[simp]

theorem CategoryTheory.Pairwise.cocone_ι_app {ι : Type v} {α : Type u} (U : ι → α) [CompleteLattice α] (o : Pairwise ι) : (cocone U).ι.app o = coconeιApp U o

def CategoryTheory.Pairwise.coconeIsColimit {ι : Type v} {α : Type u} (U : ι → α) [CompleteLattice α] : Limits.IsColimit (cocone U)

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