mapMono_naturality — Mathlib

English

Naturality of the summand-wise maps with respect to a morphism f between chain complexes: the square formed by mapMono and f.f commutes up to the appropriate compositions.

Русский

Естественность отображений на сумманду по отношению к морфизму f между комплексами: квадрат из mapMono и f.f , как ожидалось, коммутирует.

LaTeX

$$$(\text{Γ₀.Obj.Termwise.mapMono})\_K(i) \circ f.f = f.f' \circ (\text{Γ₀.Obj.Termwise.mapMono})\_K'(i)$.$$

Lean4

@[reassoc (attr := simp)]
theorem mapMono_naturality (i : Δ ⟶ Δ') [Mono i] : mapMono K i ≫ f.f Δ.len = f.f Δ'.len ≫ mapMono K' i :=
  by
  unfold mapMono
  split_ifs with h
  · subst h
    simp only [id_comp, eqToHom_refl, comp_id]
  · rw [HomologicalComplex.Hom.comm]
  · rw [zero_comp, comp_zero]

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