mono_v₀₁_τ₂

Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.SnakeInput.mono_v₀₁_τ₂

English

In a balanced category, IsIso f is equivalent to IsZero X3 for a short exact S.

Русский

В балансированной категории IsIso f эквивалентно IsZero X3 для кратко точной S.

LaTeX

$$$IsIso(S.f) \iff IsZero(S.X_3)$$$

Lean4

instance mono_v₀₁_τ₂ : Mono S.v₀₁.τ₂ :=
  mono_of_isLimit_fork S.h₀τ₂

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

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

Разделы

Аффилиация

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