instIsIsoLeftHomologyMapOfEpiτ₁Ofτ₂OfMonoτ₃

English

There is a canonical instance asserting that leftHomologyMap φ is an isomorphism when φ satisfies epi/iso/mono and the source/target have left homology.

Русский

Существуют стандартные условия: leftHomologyMap φ является изоморфизмом, если φ удовлетворяет условиям эпиморфизма/изоморфизма/моно и источники/целевые имеют левую гомологию.

LaTeX

$$$IsIso\big(leftHomologyMap(\varphi)\big)$$$

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 left homology is an isomorphism. -/
instance (φ : S₁ ⟶ S₂) [S₁.HasLeftHomology] [S₂.HasLeftHomology] [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] :
    IsIso (leftHomologyMap φ) := by
  dsimp only [leftHomologyMap]
  infer_instance

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