Q_f_0_eq

Mathlib.AlgebraicTopology.DoldKan.Projections

URI: https://scilib.ai/kg/mathlib#AlgebraicTopology.DoldKan.Q_f_0_eq

← MathLib Explorer

English

For all q, the degree-zero component of Q q is zero.

Русский

Для всех q компонент Q q в степени 0 равен нулю.

LaTeX

$$$ (Q q).f 0 = 0 $$$

Lean4

/-- All the `Q q` coincide with `0` in degree 0. -/
@[simp]
theorem Q_f_0_eq (q : ℕ) : ((Q q).f 0 : X _⦋0⦌ ⟶ X _⦋0⦌) = 0 := by
  simp only [HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, Q, P_f_0_eq, sub_self]

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

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

Разделы

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

Аффилиация

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