isIso_p

Mathlib.Algebra.Homology.ShortComplex.RightHomology

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

← MathLib Explorer

English

If f = 0, then p is an isomorphism in the right homology data structure.

Русский

Если f = 0, то p является изоморфизмом в структуре правой гомологии.

LaTeX

$$$\text{If } S.f = 0, \text{ then } p \text{ is iso}$$$

Lean4

theorem isIso_p (hf : S.f = 0) : IsIso h.p :=
  ⟨h.descQ (𝟙 S.X₂) (by rw [hf, comp_id]), p_descQ _ _ _, by
    simp only [← cancel_epi h.p, p_descQ_assoc, id_comp, comp_id]⟩

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

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

Разделы

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

Аффилиация

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