isIso_ι — Mathlib

English

If f = 0, then the canonical map ι from the kernel fork is an isomorphism.

Русский

Если f = 0, то каноническое отображение ι ядрового вилки является изоморфизмом.

LaTeX

$$$\\forall c:\\mathrm{KernelFork}(f),\\; IsLimit c \\Rightarrow f=0 \\Rightarrow IsIso(\\mathrm{Fork.ι}(c)).$$$

Lean4

theorem isIso_ι {X Y : C} {f : X ⟶ Y} (c : KernelFork f) (hc : IsLimit c) (hf : f = 0) : IsIso c.ι :=
  isIso_limit_cone_parallelPair_of_eq hf hc

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