isSplitMono_iff_isIso_unit — Mathlib

English

If μ is an isomorphism, then for each X, IsSplitMono(η.app X) iff IsIso(η.app X).

Русский

Если μ является изоморфизмом, то для каждого X: IsSplitMono(η.app X) эквивалично IsIso(η.app X).

LaTeX

$$$\\\\forall X, [IsIso \\\\mu] \\\\Rightarrow (IsSplitMono (T.\\\\eta\\\\.app X) \\\\iff IsIso (T.\\\\eta\\\\.app X)).$$$

Lean4

theorem isSplitMono_iff_isIso_unit (T : Monad C) (X : C) [IsIso T.μ] : IsSplitMono (T.η.app X) ↔ IsIso (T.η.app X) :=
  by
  refine ⟨fun _ ↦ ⟨retraction (T.η.app X), by simp, ?_⟩, fun _ ↦ inferInstance⟩
  rw [← map_id, ← show T.η.app X ≫ retraction (T.η.app X) = 𝟙 X from IsSplitMono.id _, map_comp, T.map_unit_app X, ←
    T.unit_naturality]

Похожие утверждения