English
If an initial object I exists in a CCC, then any morphism from an exponentiable A to I is an isomorphism.
Русский
Если в CCC существует начальный объект I, то любой морфизм A ⟶ I (где A экспоненцируем) является изоморфизмом.
LaTeX
$$$\forall A\; [\text{Exponentiable } A],\; \forall f: A \to I\; (I \text{ начальный}),\; \mathrm{IsIso}(f)$$$
Lean4
/-- If an initial object `I` exists in a CCC then it is a strict initial object,
i.e. any morphism to `I` is an iso.
This actually shows a slightly stronger version: any morphism to an initial object from an
exponentiable object is an isomorphism.
-/
theorem strict_initial {I : C} (t : IsInitial I) (f : A ⟶ I) : IsIso f :=
by
haveI : Mono f := by
rw [← lift_snd (𝟙 A) f, ← zeroMul_hom t]
exact mono_comp _ _
haveI : IsSplitEpi f := IsSplitEpi.mk' ⟨t.to _, t.hom_ext _ _⟩
apply isIso_of_mono_of_isSplitEpi
