linearMap_comp_eq_zero — Mathlib

English

An exact sequence 0 → M → N → P splits if and only if there exists a linear isomorphism N ≅ M × P with f = e^{-1} ∘ inl and g = snd ∘ e.

Русский

Точная последовательность 0 → M → N → P распадается эквивалентно существованию линейного изоморфизма N ≅ M × P так, что f = e^{-1} ∘ inl и g = snd ∘ e.

LaTeX

$$$$ \\exists e: N \\cong M \\times P \\text{ с } f = e^{-1} \\circ \\iota, \\; g = \\pi_2 \\circ e. $$$$

Lean4

theorem linearMap_comp_eq_zero (h : Exact f g) : g.comp f = 0 :=
  DFunLike.coe_injective h.comp_eq_zero

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