map_g' — Mathlib

English

For a functor F preserving zero morphisms, the map F.map(leftRightHomologyComparison'(h_l,h_r)) equals leftRightHomologyComparison'(h_l.map F)(h_r.map F).

Русский

Для функторa F, сохраняющего нулевые морфизмы, карта F отображает leftRightHomologyComparison'(h_l,h_r) в leftRightHomologyComparison'(h_l.map F)(h_r.map F).

LaTeX

$$$F.map\\big(\\text{leftRightHomologyComparison}'(h_l,h_r)\\big) = \\text{leftRightHomologyComparison}'\\big( h_l.map F \\,, h_r.map F \\big)$$$

Lean4

@[simp]
theorem map_g' : (h.map F).g' = F.map h.g' := by rw [← cancel_epi (h.map F).p, p_g', map_g, map_p, ← F.map_comp, p_g']

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