ι_snd

Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

URI: https://scilib.ai/kg/mathlib#CategoryTheory.kernelCokernelCompSequence.ι_snd

English

In the kernel-cokernel construction, the connecting morphism from ker f to ker(f ≫ g) is mono.

Русский

В конструировании ядра и кофоканала соединяющее отображение от ker f к ker(f ≫ g) является моно.

LaTeX

$$Mono(ι f g)$$

Lean4

@[reassoc (attr := simp)]
theorem ι_snd : ι f g ≫ biprod.snd = kernel.ι (f ≫ g) ≫ f := by simp [ι]

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

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

Разделы

Аффилиация

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