isIso_homologyMap_shortComplexTruncLE_g

English

Under certain hypotheses, the homologyMap of the shortComplexTruncLE component is an isomorphism.

Русский

При некоторых гипотезах гомологическое отображение shortComplexTruncLE-дельного компонента является изоморфизмом.

LaTeX

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

Lean4

theorem isIso_homologyMap_shortComplexTruncLE_g (i' : ι') (hi' : ∀ i, e.f i ≠ i') :
    IsIso (homologyMap (K.shortComplexTruncLE e).g i') :=
  by
  have := K.mono_homologyMap_shortComplexTruncLE_g e i' hi'
  apply isIso_of_mono_of_epi

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