isIso_of_mono — Mathlib

English

If g is a morphism and f is mono, then the kernel of g together with the kernel map is an isomorphism to the domain of f.

Русский

Если g — морфизм, а f моно, то ядро g вместе с ядровой картой образуют изоморфизм к области определения f.

LaTeX

$$$\\forall {C} [\\mathcal{C}], {X,Y}\\ f:X\\to Y,\\ a,b:R\\to X,\\IsKernelPair( f,a,b)\\Rightarrow \\text{IsIso}(a).$$$

Lean4

theorem isIso_of_mono (h : IsKernelPair f a b) [Mono f] : IsIso a :=
  by
  rw [←
    show _ = a from
      (Category.comp_id _).symm.trans
        ((IsKernelPair.id_of_mono f).isLimit.conePointUniqueUpToIso_inv_comp h.isLimit WalkingCospan.left)]
  infer_instance

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