g_desc — Mathlib

English

If S is exact with epi g, then S.g ≫ hS.desc k hk = k for any k: S.X₂ → A with S.f ≫ k = 0.

Русский

Если S точен и g эпиморфен, то S.g ∘ hS.desc k hk = k для любого k: S.X₂ → A с условием S.f ∘ k = 0.

LaTeX

$$$S.g \; \; \; hS.desc k hk = k$$$

Lean4

@[reassoc (attr := simp)]
theorem g_desc (hS : S.Exact) {A : C} (k : S.X₂ ⟶ A) (hk : S.f ≫ k = 0) [Epi S.g] : S.g ≫ hS.desc k hk = k :=
  Cofork.IsColimit.π_desc (hS.gIsCokernel)

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