Session 19: Terminal objects
In any category π, an object T is a terminal object if and only if it has the property: for each object X in π there is exactly one map from X to T.
See the earlier definition of terminal object on p. 213.
Suppose that π is any category and that both T_1 and T_2 are terminal objects in π. Then T_1 and T_2 are isomorphic; i.e. there are maps {f : T_1 \rightarrow T_2}, {g : T_2 \rightarrow T_1} such that {g \circ f} is the identity of T_1 and {f \circ g} is the identity of T_2.
To show that T_1 and T_2 are isomorphic we need first of all a map {T_1 \rightarrow T_2}. Because T_2 is terminal there is a map {f : T_1 \rightarrow T_2}. We need a map {g : T_2 \rightarrow T_1}. Again there is one because T_1 is terminal. But this does not prove yet that T_1 is isomorphic to T_2. These two maps have to be proved to be inverse to each other. Because T_1 is terminal, there is only one map from T_1 to T_1. Therefore, {g \circ f = 1_{T_1}}. [Because T_2 is terminal, there is only one map from T_2 to T_2. Therefore, {f \circ g = 1_{T_2}}.]
We provided a proof of this theorem in Article IV using the mathlib API for terminal objects. We repeat that proof here, but this time using only the book definition.
theorem uniqueness_of_terminal_objects'
{π : Type u} [Category.{v, u} π] {Tβ Tβ : π}
(hTβ : β X : π, (β f : X βΆ Tβ, (β f' : X βΆ Tβ, f = f')))
(hTβ : β X : π, (β f : X βΆ Tβ, (β f' : X βΆ Tβ, f = f')))
: Nonempty (Tβ β
Tβ) := π:Type uinstβ:Category.{v, u} πTβ:πTβ:πhTβ:β (X : π), β f, β (f' : X βΆ Tβ), f = f'hTβ:β (X : π), β f, β (f' : X βΆ Tβ), f = f'β’ Nonempty (Tβ β
Tβ)
π:Type uinstβ:Category.{v, u} πTβ:πTβ:πhTβ:β (X : π), β f, β (f' : X βΆ Tβ), f = f'hTβ:β (X : π), β f, β (f' : X βΆ Tβ), f = f'f:Tβ βΆ Tβ := Classical.choose β―β’ Nonempty (Tβ β
Tβ)
π:Type uinstβ:Category.{v, u} πTβ:πTβ:πhTβ:β (X : π), β f, β (f' : X βΆ Tβ), f = f'hTβ:β (X : π), β f, β (f' : X βΆ Tβ), f = f'f:Tβ βΆ Tβ := Classical.choose β―g:Tβ βΆ Tβ := Classical.choose β―β’ Nonempty (Tβ β
Tβ)
have hgf : g β f = π Tβ := π:Type uinstβ:Category.{v, u} πTβ:πTβ:πhTβ:β (X : π), β f, β (f' : X βΆ Tβ), f = f'hTβ:β (X : π), β f, β (f' : X βΆ Tβ), f = f'β’ Nonempty (Tβ β
Tβ)
π:Type uinstβ:Category.{v, u} πTβ:πTβ:πhTβ:β (X : π), β f, β (f' : X βΆ Tβ), f = f'hTβ:β (X : π), β f, β (f' : X βΆ Tβ), f = f'f:Tβ βΆ Tβ := Classical.choose β―g:Tβ βΆ Tβ := Classical.choose β―tβ:Tβ βΆ Tβhtβ:β (f' : Tβ βΆ Tβ), tβ = f'β’ g β f = π Tβ
All goals completed! π
have hfg : f β g = π Tβ := π:Type uinstβ:Category.{v, u} πTβ:πTβ:πhTβ:β (X : π), β f, β (f' : X βΆ Tβ), f = f'hTβ:β (X : π), β f, β (f' : X βΆ Tβ), f = f'β’ Nonempty (Tβ β
Tβ)
π:Type uinstβ:Category.{v, u} πTβ:πTβ:πhTβ:β (X : π), β f, β (f' : X βΆ Tβ), f = f'hTβ:β (X : π), β f, β (f' : X βΆ Tβ), f = f'f:Tβ βΆ Tβ := Classical.choose β―g:Tβ βΆ Tβ := Classical.choose β―hgf:g β f = π Tβ :=
Exists.casesOn (hTβ Tβ) fun tβ htβ β¦
Eq.mpr (id (congrArg (fun _a β¦ _a = π Tβ) (Eq.symm (htβ (g β f)))))
(Eq.mpr (id (congrArg (fun _a β¦ tβ = _a) (Eq.symm (htβ (π Tβ))))) (Eq.refl tβ))tβ:Tβ βΆ Tβhtβ:β (f' : Tβ βΆ Tβ), tβ = f'β’ f β g = π Tβ
All goals completed! π
π:Type uinstβ:Category.{v, u} πTβ:πTβ:πhTβ:β (X : π), β f, β (f' : X βΆ Tβ), f = f'hTβ:β (X : π), β f, β (f' : X βΆ Tβ), f = f'f:Tβ βΆ Tβ := Classical.choose β―g:Tβ βΆ Tβ := Classical.choose β―hgf:g β f = π Tβ :=
Exists.casesOn (hTβ Tβ) fun tβ htβ β¦
Eq.mpr (id (congrArg (fun _a β¦ _a = π Tβ) (Eq.symm (htβ (g β f)))))
(Eq.mpr (id (congrArg (fun _a β¦ tβ = _a) (Eq.symm (htβ (π Tβ))))) (Eq.refl tβ))hfg:f β g = π Tβ :=
Exists.casesOn (hTβ Tβ) fun tβ htβ β¦
Eq.mpr (id (congrArg (fun _a β¦ _a = π Tβ) (Eq.symm (htβ (f β g)))))
(Eq.mpr (id (congrArg (fun _a β¦ tβ = _a) (Eq.symm (htβ (π Tβ))))) (Eq.refl tβ))β’ Tβ β
Tβ
All goals completed! π