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

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

Equations

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

inductive CategoryTheory.Pairwise.Hom {ι : Type v} : CategoryTheory.Pairwise ι → CategoryTheory.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 : ι) → (CategoryTheory.Pairwise.single i).Hom (CategoryTheory.Pairwise.single i)
• id_pair: {ι : Type v} → (i j : ι) → (CategoryTheory.Pairwise.pair i j).Hom (CategoryTheory.Pairwise.pair i j)
• left: {ι : Type v} → (i j : ι) → (CategoryTheory.Pairwise.pair i j).Hom (CategoryTheory.Pairwise.single i)
• right: {ι : Type v} → (i j : ι) → (CategoryTheory.Pairwise.pair i j).Hom (CategoryTheory.Pairwise.single j)

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

Equations

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

def CategoryTheory.Pairwise.id {ι : Type v} (o : CategoryTheory.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₁ : CategoryTheory.Pairwise ι} {o₂ : CategoryTheory.Pairwise ι} {o₃ : CategoryTheory.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

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} : CategoryTheory.Category.{v, v} (CategoryTheory.Pairwise ι)

Equations

• CategoryTheory.Pairwise.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯

def CategoryTheory.Pairwise.diagramObj {ι : Type v} {α : Type v} (U : ι → α) [SemilatticeInf α] : CategoryTheory.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 v} (U : ι → α) [SemilatticeInf α] {o₁ : CategoryTheory.Pairwise ι} {o₂ : CategoryTheory.Pairwise ι} : (o₁ ⟶ o₂) → (CategoryTheory.Pairwise.diagramObj U o₁ ⟶ CategoryTheory.Pairwise.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 ⋯

@[simp]

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

@[simp]

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

def CategoryTheory.Pairwise.diagram {ι : Type v} {α : Type v} (U : ι → α) [SemilatticeInf α] : CategoryTheory.Functor (CategoryTheory.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.

def CategoryTheory.Pairwise.coconeιApp {ι : Type v} {α : Type v} (U : ι → α) [CompleteLattice α] (o : CategoryTheory.Pairwise ι) : CategoryTheory.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 ⋯)

@[simp]

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

@[simp]

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

def CategoryTheory.Pairwise.cocone {ι : Type v} {α : Type v} (U : ι → α) [CompleteLattice α] : CategoryTheory.Limits.Cocone (CategoryTheory.Pairwise.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 := ⋯ } }

def CategoryTheory.Pairwise.coconeIsColimit {ι : Type v} {α : Type v} (U : ι → α) [CompleteLattice α] : CategoryTheory.Limits.IsColimit (CategoryTheory.Pairwise.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 := ⋯ }