singleObjXIsoOfEq

Mathlib.Algebra.Homology.Single

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.singleObjXIsoOfEq

Lean4

/-- The object in degree `i` of `(single V c h).obj A` is just `A` when `i = j`. -/
noncomputable def singleObjXIsoOfEq (j : ι) (A : V) (i : ι) (hi : i = j) : ((single V c j).obj A).X i ≅ A :=
  eqToIso (by subst hi; simp [single])

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

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

Разделы

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

Аффилиация

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