nullHomotopicMap_f_eq_zero — Mathlib

English

If k₀ has no adjacent Rel-relations in either direction, then the f-component of the null-homotopic map induced by any morphism hom is zero.

Русский

Если для индекса k₀ не существуетRel-й связи ни слева, ни справа, то f-компонента нулевой гомотопической карты, порождаемой отображением hom, равна нулю.

LaTeX

$$$ (\mathrm{nullHomotopicMap} \mathrm{hom})_f k_0 = 0 $$$

Lean4

@[simp]
theorem nullHomotopicMap_f_eq_zero {k₀ : ι} (hk₀ : ∀ l : ι, ¬c.Rel k₀ l) (hk₀' : ∀ l : ι, ¬c.Rel l k₀)
    (hom : ∀ i j, C.X i ⟶ D.X j) : (nullHomotopicMap hom).f k₀ = 0 :=
  by
  dsimp [nullHomotopicMap, dNext, prevD]
  rw [C.shape, D.shape, zero_comp, comp_zero, add_zero] <;> apply_assumption

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