English
Let T be a comonad and X an object in the base category, with the counit δ of T being invertible. Then the morphism T.ε.app X is a split epimorphism if and only if it is an isomorphism.
Русский
Пусть T — комонад и X — объект в исходной категории, причём δ комонада T является обратимым. Тогда моремизм T.ε.app X является разложимым эпиморфизм тогда и только тогда, когда он является изоморфизмом.
LaTeX
$$$[\text{IsIso } \delta] \; \Rightarrow\; \bigl( \operatorname{IsSplitEpi}(T.\varepsilon_{\mathrm{app}\,X}) \;\iff\; \operatorname{IsIso}(T.\varepsilon_{\mathrm{app}\,X}) \bigr).$$$
Lean4
theorem isSplitEpi_iff_isIso_counit (T : Comonad C) (X : C) [IsIso T.δ] : IsSplitEpi (T.ε.app X) ↔ IsIso (T.ε.app X) :=
by
refine ⟨fun _ ↦ ⟨section_ (T.ε.app X), ?_, by simp⟩, fun _ ↦ inferInstance⟩
rw [← map_id, ← show section_ (T.ε.app X) ≫ T.ε.app X = 𝟙 X from IsSplitEpi.id (T.ε.app X), map_comp,
T.map_counit_app X, T.counit_naturality]
