ι_zero_isIso

Mathlib.CategoryTheory.Limits.Shapes.Kernels

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.kernel.ι_zero_isIso

English

If h is the reflexive equality f = f, then kernelIsoOfEq h is the identity on kernel f.

Русский

Если h — тождество f = f, то kernelIsoOfEq h — тождественный изоморфизм на kernel f.

LaTeX

$$$\\text{kernelIsoOfEq}(h) = \\mathrm{Iso.refl}(\\ker f)$ when $h$ is $f=f$.$$

Lean4

/-- Every kernel of the zero morphism is an isomorphism -/
instance ι_zero_isIso : IsIso (kernel.ι (0 : X ⟶ Y)) :=
  equalizer.ι_of_self _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru