Theorems · Definition · category theory

CategoryTheory.subterminalsEquivMonoOverTerminal

(C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasTerminal C] → CategoryTheory.Subterminals C ≌ CategoryTheory.MonoOver (⊤_ C)

The category of subterminal objects is equivalent to the category of monomorphisms to the terminal object (which is in turn equivalent to the subobjects of the terminal object).

Defined in

Mathlib.CategoryTheory.Subterminal

Cited by

8 results in Mathlib

Foundations

Depth 36 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasTerminal