instIsIsoRightHomologyMapOfEpiτ₁Ofτ₂OfMonoτ₃

English

If φ is an iso on τ2 and epi on τ1, and S1,S2 have right homology, then rightHomologyMap φ is an isomorphism.

Русский

Если φ имеет изоморфизм на τ2 и эпиморфизм на τ1, и S1, S2 имеют правую гомологию, то rightHomologyMap φ — изоморфизм.

LaTeX

$$$\\text{IsIso}(\\mathrm{rightHomologyMap}\\ φ)$$$

Lean4

/-- If a morphism of short complexes `φ : S₁ ⟶ S₂` is such that `φ.τ₁` is epi, `φ.τ₂` is an iso,
and `φ.τ₃` is mono, then the induced morphism on right homology is an isomorphism. -/
instance (φ : S₁ ⟶ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] :
    IsIso (rightHomologyMap φ) := by
  dsimp only [rightHomologyMap]
  infer_instance

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