mathlib3 documentation

category_theory.category.pairwise

The category of "pairwise intersections". #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

inductive category_theory.pairwise (ι : Type v) :

single : Π {ι : Type v}, ι → category_theory.pairwise ι
pair : Π {ι : Type v}, ι → ι → category_theory.pairwise ι

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.

Instances for category_theory.pairwise

category_theory.pairwise.has_sizeof_inst
category_theory.pairwise.pairwise_inhabited
category_theory.pairwise.category_theory.category

@[protected, instance]

def category_theory.pairwise.pairwise_inhabited {ι : Type v} [inhabited ι] :

inhabited (category_theory.pairwise ι)

Equations

category_theory.pairwise.pairwise_inhabited = {default := category_theory.pairwise.single inhabited.default}

inductive category_theory.pairwise.hom {ι : Type v} :

category_theory.pairwise ι → category_theory.pairwise ι → Type v

id_single : Π {ι : Type v} (i : ι), (category_theory.pairwise.single i).hom (category_theory.pairwise.single i)
id_pair : Π {ι : Type v} (i j : ι), (category_theory.pairwise.pair i j).hom (category_theory.pairwise.pair i j)
left : Π {ι : Type v} (i j : ι), (category_theory.pairwise.pair i j).hom (category_theory.pairwise.single i)
right : Π {ι : Type v} (i j : ι), (category_theory.pairwise.pair i j).hom (category_theory.pairwise.single j)

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.

Instances for category_theory.pairwise.hom

category_theory.pairwise.hom.has_sizeof_inst
category_theory.pairwise.hom_inhabited

@[protected, instance]

def category_theory.pairwise.hom_inhabited {ι : Type v} [inhabited ι] :

inhabited ((category_theory.pairwise.single inhabited.default).hom (category_theory.pairwise.single inhabited.default))

Equations

category_theory.pairwise.hom_inhabited = {default := category_theory.pairwise.hom.id_single inhabited.default}

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

o.hom o

The identity morphism in pairwise ι.

Equations

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

@[protected, instance]

def category_theory.pairwise.category_theory.category {ι : Type v} :

category_theory.category (category_theory.pairwise ι)

Equations

category_theory.pairwise.category_theory.category = {to_category_struct := {to_quiver := {hom := category_theory.pairwise.hom ι}, id := category_theory.pairwise.id ι, comp := λ (X Y Z : category_theory.pairwise ι) (f : X ⟶ Y) (g : Y ⟶ Z), category_theory.pairwise.comp f g}, id_comp' := _, comp_id' := _, assoc' := _}

@[simp]

def category_theory.pairwise.diagram_obj {ι α : Type v} (U : ι → α) [semilattice_inf α] :

category_theory.pairwise ι → α

Auxiliary definition for diagram.

Equations

category_theory.pairwise.diagram_obj U (category_theory.pairwise.pair i j) = U i ⊓ U j
category_theory.pairwise.diagram_obj U (category_theory.pairwise.single i) = U i

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

Auxiliary definition for diagram.

Equations

@[simp]

theorem category_theory.pairwise.diagram_obj_2 {ι α : Type v} (U : ι → α) [semilattice_inf α] (ᾰ : category_theory.pairwise ι) :

(category_theory.pairwise.diagram U).obj ᾰ = category_theory.pairwise.diagram_obj U ᾰ

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 U i and pair i j to U i ⊓ U j, and the morphisms to the obvious inequalities.

Equations

category_theory.pairwise.diagram U = {obj := category_theory.pairwise.diagram_obj U _inst_1, map := λ (X Y : category_theory.pairwise ι) (f : X ⟶ Y), category_theory.pairwise.diagram_map U f, map_id' := _, map_comp' := _}

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

def category_theory.pairwise.cocone_ι_app {ι α : Type v} (U : ι → α) [complete_lattice α] (o : category_theory.pairwise ι) :

category_theory.pairwise.diagram_obj U o ⟶ supr U

Auxiliary definition for cocone.

Equations

def category_theory.pairwise.cocone {ι α : Type v} (U : ι → α) [complete_lattice α] :

category_theory.limits.cocone (category_theory.pairwise.diagram U)

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

Equations

category_theory.pairwise.cocone U = {X := supr U, ι := {app := category_theory.pairwise.cocone_ι_app U _inst_1, naturality' := _}}

@[simp]

theorem category_theory.pairwise.cocone_ι_app_2 {ι α : Type v} (U : ι → α) [complete_lattice α] (o : category_theory.pairwise ι) :

(category_theory.pairwise.cocone U).ι.app o = category_theory.pairwise.cocone_ι_app U o

@[simp]

theorem category_theory.pairwise.cocone_X {ι α : Type v} (U : ι → α) [complete_lattice α] :

(category_theory.pairwise.cocone U).X = supr U

def category_theory.pairwise.cocone_is_colimit {ι α : Type v} (U : ι → α) [complete_lattice α] :

category_theory.limits.is_colimit (category_theory.pairwise.cocone U)

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

Equations

category_theory.pairwise.cocone_is_colimit U = {desc := λ (s : category_theory.limits.cocone (category_theory.pairwise.diagram U)), category_theory.hom_of_le _, fac' := _, uniq' := _}