Theorems · Inductive type · category theory

CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal

{J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ → J → Type w

Given a κ-bounded diagram D in a category J, an object e : J is terminal if 𝟙 e belongs to D and for any object j of D, there is a unique morphism j ⟶ e in D, such that these unique morphisms are compatible with precomposition with morphisms in D.

Defined in

Mathlib.CategoryTheory.Presentable.Directed

Cited by

20 results in Mathlib

Foundations

Depth 20 from the axioms · uses Quot.sound

Assumes

CategoryTheory.SmallCategory