isIso_homologyMap_of_iso

Mathlib.Algebra.Homology.ShortComplex.Homology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.isIso_homologyMap_of_iso

← MathLib Explorer

English

If φ is an isomorphism, then homologyMap φ is an isomorphism.

Русский

Если φ — изоморфизм, то homologyMap φ — изоморфизм.

LaTeX

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

Lean4

instance isIso_homologyMap_of_iso (φ : S₁ ⟶ S₂) [IsIso φ] [S₁.HasHomology] [S₂.HasHomology] : IsIso (homologyMap φ) :=
  (inferInstance : IsIso (homologyMapIso (asIso φ)).hom)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru