lift_snd

Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

URI: https://scilib.ai/kg/mathlib#CochainComplex.mappingCone.lift_snd

English

There is a lift morphism lift φ α β eq: K ⟶ mappingCone φ in the presence of cocycle relation δ 0 1 β + α.1 . φ = 0.

Русский

Существует переход lift φ α β eq: K ⟶ mappingCone φ при условии кокцикла δ 0 1 β + α.1 φ = 0.

LaTeX

$$$\text{lift}(φ, α, β, eq) : K \to \mathrm{mappingCone}(φ)$$$

Lean4

theorem lift_snd : (Cochain.ofHom (lift φ α β eq)).comp (snd φ) (zero_add 0) = β := by simp

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

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

Разделы

Аффилиация

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