exact_of_comp_of_mem_range — Mathlib

English

Let R be a semiring and M, N, P be modules with linear maps f: M → N and g: N → P. If g ∘ f = 0 and ker(g) ⊆ ran(f), then the sequence M --f--> N --g--> P is exact, i.e. ran(f) = ker(g).

Русский

Пусть R — полугруппа, M, N, P — модули и имеются линейные отображения f: M → N и g: N → P. Если g ∘ f = 0 и ker(g) ⊆ im(f), тогда последовательность M → N → P точно образована, то есть im(f) = ker(g).

LaTeX

$$$$ g\\circ f = 0 \\;\\wedge\\; \\ker g \\subseteq \\operatorname{ran} f \\quad\\Longrightarrow\\quad \\operatorname{ran} f = \\ker g $$$$

Lean4

theorem exact_of_comp_of_mem_range (h1 : g ∘ₗ f = 0) (h2 : ∀ x, g x = 0 → x ∈ range f) : Exact f g :=
  exact_of_comp_eq_zero_of_ker_le_range h1 h2

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