Theorems · Inductive type · category theory

CategoryTheory.Limits.ColimitPresentation

{C : Type u} →
  [CategoryTheory.Category.{v, u} C] →
    (J : Type w) → [CategoryTheory.Category.{t, w} J] → C → Type (max (max (max t u) v) w)

A colimit presentation of X over J is a diagram {Dᵢ} in C and natural maps sᵢ : Dᵢ ⟶ X making X into the colimit of the Dᵢ.

Defined in

Mathlib.CategoryTheory.Limits.Presentation

Cited by

54 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Category