mapIso

Mathlib.Algebra.Homology.TotalComplex

URI: https://scilib.ai/kg/mathlib#HomologicalComplex₂.total.mapIso

Lean4

/-- The isomorphism `K.total c₁₂ ≅ L.total c₁₂` of homological complexes induced
by an isomorphism of bicomplexes `K ≅ L`. -/
@[simps]
noncomputable def mapIso : K.total c₁₂ ≅ L.total c₁₂
    where
  hom := map e.hom _
  inv := map e.inv _
  hom_inv_id := by rw [← map_comp, e.hom_inv_id, map_id]
  inv_hom_id := by rw [← map_comp, e.inv_hom_id, map_id]

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

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

Разделы

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

Аффилиация

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