mono_homologyMap_shortComplexTruncLE_g

English

Under a certain condition on i', the morphism homologyMap (K.shortComplexTruncLE e).g i' is mono.

Русский

При условии на i' отображение homologyMap(...) .g i' является моно.

LaTeX

$$$ Mono\big( homologyMap\big( K.shortComplexTruncLE e\).g\ i' \big) $$$

Lean4

theorem mono_homologyMap_shortComplexTruncLE_g (i' : ι') (hi' : ∀ i, e.f i ≠ i') :
    Mono (homologyMap (K.shortComplexTruncLE e).g i') :=
  ((K.shortComplexTruncLE_shortExact e).homology_exact₂ i').mono_g
    (by apply ((K.truncLE e).exactAt_of_isSupported e i' hi').isZero_homology.eq_of_src)

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