desc'

Mathlib.Algebra.Homology.ShortComplex.Exact

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.Exact.desc'

English

There exists l: S.X₃ → A with S.g ≫ l = k when S is exact and S.f ≫ k = 0.

Русский

Существует l: S.X₃ → A с S.g ≫ l = k при условии S.f ≫ k = 0 и точности S.

LaTeX

$$$\exists l : S.X_3 \to A,\ S.g \gg l = k$$$

Lean4

theorem desc' (hS : S.Exact) {A : C} (k : S.X₂ ⟶ A) (hk : S.f ≫ k = 0) [Epi S.g] : ∃ (l : S.X₃ ⟶ A), S.g ≫ l = k :=
  ⟨hS.desc k hk, by simp⟩

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

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

Разделы

Аффилиация

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