nullHomotopicMap_f_of_not_rel_right

English

Extending a chain map φ along an embedding e preserves quasi-isomorphisms: QuasiIso(extendMap φ e) iff QuasiIso φ.

Русский

Расширение цепного отображения φ вдоль вложения e сохраняет квазизоморфизмы: QuasiIso(extendMap φ e) эквивалично QuasiIso φ.

LaTeX

$$$ \text{QuasiIso}(\mathrm{extendMap}(\phi,e)) \iff \text{QuasiIso}(\phi) $$$

Lean4

theorem nullHomotopicMap_f_of_not_rel_right {k₁ k₀ : ι} (r₁₀ : c.Rel k₁ k₀) (hk₁ : ∀ l : ι, ¬c.Rel l k₁)
    (hom : ∀ i j, C.X i ⟶ D.X j) : (nullHomotopicMap hom).f k₁ = C.d k₁ k₀ ≫ hom k₀ k₁ :=
  by
  dsimp only [nullHomotopicMap]
  rw [dNext_eq hom r₁₀, prevD, AddMonoidHom.mk'_apply, D.shape, comp_zero, add_zero]
  exact
    hk₁
      _
        -- Cannot be @[simp] because `k₀` cannot be inferred by `simp`.

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