ofHom_comp

Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

URI: https://scilib.ai/kg/mathlib#CochainComplex.HomComplex.Cochain.ofHom_comp

← MathLib Explorer

English

For f: F ⟶ G and g: G ⟶ K, ofHom(f ≫ g) = (ofHom f) ∘ (ofHom g) (zero_add 0).

Русский

Для f: F ⟶ G и g: G ⟶ K, ofHom(f ≫ g) = (ofHom f) ∘ (ofHom g) (zero_add 0).

LaTeX

$$$$(ofHom(f \\circ g)) = ((ofHom f) \\circ (ofHom g)) (zero\\_add\\; 0).$$$$

Lean4

@[simp]
theorem ofHom_comp (f : F ⟶ G) (g : G ⟶ K) : ofHom (f ≫ g) = (ofHom f).comp (ofHom g) (zero_add 0) := by
  simp only [ofHom, HomologicalComplex.comp_f, ofHoms_comp]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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