δ_snd

Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

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

English

Differential δ on the mapping cone application: the δ-operator at (-1,0) on inl φ equals Cochain.ofHom(φ ≫ inr φ).

Русский

Дифференциал δ на (−1,0) для inl φ равен Cochain.ofHom(φ ≫ inr φ).

LaTeX

$$$\delta_{-1,0}(inl φ) = Cochain.ofHom(φ \gg inr φ).$$$

Lean4

@[simp]
theorem δ_snd : δ 0 1 (snd φ) = -(fst φ).1.comp (Cochain.ofHom φ) (add_zero 1) :=
  by
  ext p q hpq
  simp [d_snd_v φ p q hpq]

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

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

Разделы

Аффилиация

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