instEpiP

Mathlib.Algebra.Homology.ShortComplex.RightHomology

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

English

If φ.τ1 is epi, φ.τ2 is iso, and φ.τ3 is mono, then φ is a quasi-isomorphism.

Русский

Если у φ.τ1 эпиморфизм, φ.τ2 изоморфизм, φ.τ3 мономорфизм, тогда φ — квазиизоморфизм.

LaTeX

$$$\text{Epi}(φ.τ_1) \land \text{IsIso}(φ.τ_2) \land \text{Mono}(φ.τ_3) \Rightarrow \operatorname{QuasiIso}(φ)$$$

Lean4

instance : Epi h.p :=
  ⟨fun _ _ => Cofork.IsColimit.hom_ext h.hp⟩

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

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

Разделы

Аффилиация

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