map_condition

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.CokernelCofork.map_condition

English

The inverse of the kernel iso equals the cokernel comparison morphism.

Русский

Обратная часть изоморфизма ядра равна cokernel-сравнению.

LaTeX

$$$(PreservesKernel.iso G f).{\\text{inv}} = (kernelComparison f G)$$$

Lean4

@[reassoc (attr := simp)]
theorem map_condition : G.map f ≫ G.map c.π = 0 := by rw [← G.map_comp, c.condition, G.map_zero]

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

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

Разделы

Аффилиация

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