mapX_some

Mathlib.Algebra.Homology.Embedding.Extend

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.extend.mapX_some

Lean4

theorem mapX_some {i : Option ι} {a : ι} (hi : i = some a) : mapX φ i = (XIso K hi).hom ≫ φ.f a ≫ (XIso L hi).inv :=
  by
  subst hi
  dsimp [XIso, X]
  rw [id_comp, comp_id]
  rfl

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

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

Разделы

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

Аффилиация

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