universal properties [tt-003O]
universal properties [tt-003O]
definition 1. universal arrow [kostecki2011introduction, 3.4, 3.5] [tt-001A]
definition 1. universal arrow [kostecki2011introduction, 3.4, 3.5] [tt-001A]
A universal arrow from \(X \in {\cal D}\) to \(\mathscr {F} : {\cal C} \to {\cal D}\) is a unique pair \((O , u)\) that makes the diagram
commute for any \(f \in {\cal D}\).
Conversely, a (co)universal arrow from \(\mathscr {F} : {\cal C} \to {\cal D}\) to \(X \in {\cal D}\) is a unique pair \((O , u)\) that makes the diagram
commute for any \(f \in {\cal D}\).
remark 2. universal property [leinster2016basic, sec. 1] [tt-002Z]
remark 2. universal property [leinster2016basic, sec. 1] [tt-002Z]
We say universal arrows satisfy some universal property.
The term universal property is used to describe some property (usually some equality of some compositions, or a commuting diagram in general) that is satisfied for all (hence universal) relevant objects/arrows in the "world" (i.e. in the relevant categories), by a corresponding unique object/arrow.
It's usually spell out like this:
In a context where (usually a given diagram), for all (some objects/arrows), there exists a unique (object/arrow) such that (some property).
Diagramatically,
For clarity and brevity, usually the \(\forall \) clauses are specified outside the diagram, and the \(\exists !\) clause is expressed by dashed arrows. For more elaborate diagrams, see [freyd1976properties][fong2018seven][ochs2022missing].
For the diagram above, we also say that \(f\) uniquely factors through \(u\) along \(g\) [riehl2017category, 2.3.7].
A universal property is a property of some construction which boils down to (is manifestly equivalent to) the property that an associated object is an initial object of some (auxiliary) category [nlab2020univ].
definition 3. comma category [leinster2016basic, 2.3.1] [tt-001C]
definition 3. comma category [leinster2016basic, 2.3.1] [tt-001C]
Given categories and functors
the comma category \(\mathscr {F} \downarrow \mathscr {G}\) (or \((\mathscr {F} \Rightarrow \mathscr {G})\)) is the category given by objects \((X, h, Y)\) and arrows \((f, g)\) that makes the diagram
commute.
lemma 4. universal arrow via initial/terminal object of comma category [kostecki2011introduction, 3.6] [tt-001B]
lemma 4. universal arrow via initial/terminal object of comma category [kostecki2011introduction, 3.6] [tt-001B]
A universal arrow from \(X \in {\cal D}\) to \(\mathscr {F} : {\cal C} \to {\cal D}\) is an initial object in the comma category \(X \downarrow \mathscr {F}\).
Conversely, a (co)universal arrow from \(\mathscr {F} : {\cal C} \to {\cal D}\) to \(X \in {\cal D}\) is a terminal object in the comma category \(\mathscr {F} \downarrow X\).