comp_id

Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

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

← MathLib Explorer

English

Right unit law: z1 ∘ (ofHom(id_G)) = z1.

Русский

Правило правой единицы: z1 ∘ (ofHom(id_G)) = z1.

LaTeX

$$$\\forall z_1,\\ z_1 \\circ (Cochain.ofHom(\\\\mathrm{id}_G)) = z_1.$$$

Lean4

@[simp]
protected theorem comp_id {n : ℤ} (z₁ : Cochain F G n) : z₁.comp (Cochain.ofHom (𝟙 G)) (add_zero n) = z₁ :=
  by
  ext p q hpq
  simp only [comp_zero_cochain_v, ofHom_v, HomologicalComplex.id_f, comp_id]

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

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

Разделы

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

Аффилиация

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