ofHomotopy_refl

Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

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

English

The cochain of degree −1 associated to the identity homotopy on φ is zero: ofHomotopy(Homotopy.refl φ) = 0.

Русский

Коцепр степени −1, связанный с тождественной гомотопией на φ, равен нулю: ofHomotopy(Homotopy.refl φ) = 0.

LaTeX

$$$$\mathrm{ofHomotopy}(\mathrm{Homotopy.refl}(\varphi)) = 0.$$$$

Lean4

@[simp]
theorem ofHomotopy_refl (φ : F ⟶ G) : ofHomotopy (Homotopy.refl φ) = 0 :=
  rfl

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

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

Разделы

Аффилиация

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