Theorems · Definition · category theory

CategoryTheory.Pairwise.diagram

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

Given a function U : ι → α for [SemilatticeInf α], we obtain a functor CategoryTheory.Pairwise ι ⥤ α, sending single i to U i and pair i j to U i ⊓ U j, and the morphisms to the obvious inequalities.

Defined in

Mathlib.CategoryTheory.Category.Pairwise

Cited by

30 results in Mathlib

Foundations

Depth 16 from the axioms · uses no axioms

Assumes

SemilatticeInf