English
The specialized map_exact statement for IsLocalizedModule asserts that the localized composition preserves exactness: the composition of localized maps is exact whenever the original maps are exact.
Русский
Специализированное утверждение map_exact для IsLocalizedModule утверждает, что локализованное отображение сохраняет точность: композиция локализованных отображений точна, если исходные отображения точны.
LaTeX
$$$\text{Function.Exact}(g,h) \Rightarrow \text{Function.Exact}(\mathrm{map}\;S\;f_0\;f_1\;g, \mathrm{map}\;S\;f_1\;f_2\;h)$$$
Lean4
/-- Localization of modules is an exact functor. -/
theorem map_exact (g : M₀ →ₗ[R] M₁) (h : M₁ →ₗ[R] M₂) (ex : Function.Exact g h) :
Function.Exact (map S f₀ f₁ g) (map S f₁ f₂ h) :=
Function.Exact.of_ladder_linearEquiv_of_exact (map_iso_commute S f₀ f₁ g) (map_iso_commute S f₁ f₂ h)
(LocalizedModule.map_exact S g h ex)
