kerι_comp

Mathlib.Algebra.Category.ModuleCat.Topology.Homology

URI: https://scilib.ai/kg/mathlib#TopModuleCat.kerι_comp

English

The kernel cone is the limit of the kernel fork, i.e., kerφ is the kernel in TopModuleCat(R).

Русский

Конус ядра является пределом ядрового разветвления, то есть ker φ является ядром в TopModuleCat(R).

LaTeX

$$$\text{isLimitKer}: IsLimit(KernelFork.ofι(\kerι φ)...)$$$

Lean4

@[simp]
theorem kerι_comp : kerι φ ≫ φ = 0 := by ext ⟨_, hm⟩; exact hm

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

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

Разделы

Аффилиация

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