chainsMap_f_0_comp_chainsIso₀ — Mathlib

English

There is a map of short complexes induced by f and φ between the short complex H1 objects, built from maps τ1, τ2, and τ3 that glue to form a morphism of short complexes.

Русский

Существуют отображения между короткими комплексами, индуцируемые f и φ, построенные из τ1, τ2, τ3, образующие морфизм между короткими комплексами.

LaTeX

$$$\text{mapShortComplexH1}(f, φ) : \text{shortComplexH1}(G,A) \to \text{shortComplexH1}(H,B)$$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem chainsMap_f_0_comp_chainsIso₀ : (chainsMap f φ).f 0 ≫ (chainsIso₀ B).hom = (chainsIso₀ A).hom ≫ φ.hom :=
  by
  ext
  simp [chainsMap_f, Unique.eq_default (α := Fin 0 → G), Unique.eq_default (α := Fin 0 → H), chainsIso₀]

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