surjective_of_localized_span — Mathlib

English

Exactness can be checked locally on a span; if each localized piece is exact, then the global map is exact.

Русский

Точность может проверяться локально на span; если каждая локализованная часть точна, то глобальная карта точна.

LaTeX

$$$\\forall r\\in s,\\; \\mathrm{Exact}(\\text{map}(.powers r.1)(f),\\text{map}(.powers r.1)(g)) \\Rightarrow \\mathrm{Exact}(f,g)$$$

Lean4

theorem surjective_of_localized_span (h : ∀ r : s, Function.Surjective (map (.powers r.1) f)) : Function.Surjective f :=
  surjective_of_isLocalized_span s spn _ (fun _ ↦ mkLinearMap _ _) _ (fun _ ↦ mkLinearMap _ _) f h

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