map_ι₀_eq_map_ι₁ — Mathlib

English

Under the assumption that every j is related to some i (hc), any functor H that inverts homotopy equivalences satisfies H.map(ι0 K) = H.map(ι1 K).

Русский

При предположении hc, что любой индекс j связан с некоторым i, любой функтор H, инвертирующий гомотопические эквивалентности, удовлетворяет H.map(ι0 K) = H.map(ι1 K).

LaTeX

$$$H.map(ι_0 K) = H.map(ι_1 K)$$$

Lean4

theorem map_ι₀_eq_map_ι₁ {D : Type*} [Category D] (H : HomologicalComplex C c ⥤ D)
    (hH : (homotopyEquivalences C c).IsInvertedBy H) : H.map (ι₀ K) = H.map (ι₁ K) :=
  by
  have : IsIso (H.map (cylinder.π K)) := hH _ ⟨homotopyEquiv K hc, rfl⟩
  simp only [← cancel_mono (H.map (cylinder.π K)), ← H.map_comp, ι₀_π, H.map_id, ι₁_π]

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