exact_of_localized_span — Mathlib

English

Exactness at all the localizations implies global exactness for a span of modules.

Русский

Точность во всех локализациях влечёт глобальную точность для полосы модулей.

LaTeX

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

Lean4

theorem exact_of_localized_span (h : ∀ r : s, Function.Exact (map (.powers r.1) f) (map (.powers r.1) g)) :
    Function.Exact f g :=
  exact_of_isLocalized_span s spn _ (fun _ ↦ mkLinearMap _ _) _ (fun _ ↦ mkLinearMap _ _) _ (fun _ ↦ mkLinearMap _ _) f
    g h

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