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 ι

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

Equations

• CategoryTheory.Pairwise.pairwiseInhabited = { default := CategoryTheory.Pairwise.single default }

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)

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

Equations

• CategoryTheory.Pairwise.homInhabited = { default := CategoryTheory.Pairwise.Hom.id_single default }

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

The identity morphism in Pairwise ι.

Equations

• (CategoryTheory.Pairwise.single i).id = CategoryTheory.Pairwise.Hom.id_single i
• (CategoryTheory.Pairwise.pair i j).id = CategoryTheory.Pairwise.Hom.id_pair i j

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

Composition of morphisms in Pairwise ι.

Equations

• CategoryTheory.Pairwise.comp (CategoryTheory.Pairwise.Hom.id_single i) x✝ = x✝
• CategoryTheory.Pairwise.comp (CategoryTheory.Pairwise.Hom.id_pair i j) x✝ = x✝
• CategoryTheory.Pairwise.comp (CategoryTheory.Pairwise.Hom.left i j) (CategoryTheory.Pairwise.Hom.id_single i) = CategoryTheory.Pairwise.Hom.left i j
• CategoryTheory.Pairwise.comp (CategoryTheory.Pairwise.Hom.right i j) (CategoryTheory.Pairwise.Hom.id_single j) = CategoryTheory.Pairwise.Hom.right i j

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

Equations

• CategoryTheory.Pairwise.instCategoryStruct = { Hom := CategoryTheory.Pairwise.Hom, id := CategoryTheory.Pairwise.id, comp := @CategoryTheory.Pairwise.comp ι }

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

A helper tactic for aesop_cat and Pairwise.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• CategoryTheory.Pairwise.instCategory = { toCategoryStruct := CategoryTheory.Pairwise.instCategoryStruct, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

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

Auxiliary definition for diagram.

Equations

• CategoryTheory.Pairwise.diagramObj U (CategoryTheory.Pairwise.single i) = U i
• CategoryTheory.Pairwise.diagramObj U (CategoryTheory.Pairwise.pair i j) = U i ⊓ U j

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.

Equations

• CategoryTheory.Pairwise.diagramMap U (CategoryTheory.Pairwise.Hom.id_single i) = CategoryTheory.CategoryStruct.id (CategoryTheory.Pairwise.diagramObj U (CategoryTheory.Pairwise.single i))
• CategoryTheory.Pairwise.diagramMap U (CategoryTheory.Pairwise.Hom.id_pair i j) = CategoryTheory.CategoryStruct.id (CategoryTheory.Pairwise.diagramObj U (CategoryTheory.Pairwise.pair i j))
• CategoryTheory.Pairwise.diagramMap U (CategoryTheory.Pairwise.Hom.left i j) = CategoryTheory.homOfLE ⋯
• CategoryTheory.Pairwise.diagramMap U (CategoryTheory.Pairwise.Hom.right i j) = CategoryTheory.homOfLE ⋯

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.

Equations

• One or more equations did not get rendered due to their size.

@[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✝

@[simp]

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

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

Auxiliary definition for cocone.

Equations

• CategoryTheory.Pairwise.coconeιApp U (CategoryTheory.Pairwise.single i) = CategoryTheory.homOfLE ⋯
• CategoryTheory.Pairwise.coconeιApp U (CategoryTheory.Pairwise.pair i j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯)

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.

Equations

• CategoryTheory.Pairwise.cocone U = { pt := iSup U, ι := { app := CategoryTheory.Pairwise.coconeιApp U, naturality := ⋯ } }

@[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.

Equations

• CategoryTheory.Pairwise.coconeIsColimit U = { desc := fun (s : CategoryTheory.Limits.Cocone (CategoryTheory.Pairwise.diagram U)) => CategoryTheory.homOfLE ⋯, fac := ⋯, uniq := ⋯ }