English
Localization of modules is an exact functor: if g: M0 → M1 and h: M1 → M2 form an exact sequence, then the corresponding localized maps yield an exact sequence after applying localization.
Русский
Локализация модулей является точной функцией: если g: M0 → M1 и h: M1 → M2 образуют точную последовательность, то после локализации соответствующие отображения образуют точную последовательность.
LaTeX
$$$\text{Exact}(g,h) \Rightarrow \text{Exact}(\mathrm{map}\;S\;\mathrm{mkLinearMap}\;g, \mathrm{map}\;S\;\mathrm{mkLinearMap}\;h)$$$
Lean4
/-- Localization of modules is an exact functor, proven here for `LocalizedModule`.
See `IsLocalizedModule.map_exact` for the more general version. -/
theorem map_exact (g : M₀ →ₗ[R] M₁) (h : M₁ →ₗ[R] M₂) (ex : Exact g h) :
Exact (map S (mkLinearMap S M₀) (mkLinearMap S M₁) g) (map S (mkLinearMap S M₁) (mkLinearMap S M₂) h) := fun y ↦
Iff.intro
(induction_on
(fun m s hy ↦ by
rw [map_LocalizedModules, ← zero_mk 1, mk_eq, one_smul, smul_zero] at hy
obtain ⟨a, aS, ha⟩ := Subtype.exists.1 hy
rw [smul_zero, mk_smul, ← LinearMap.map_smul, ex (a • m)] at ha
rcases ha with ⟨x, hx⟩
use mk x (⟨a, aS⟩ * s)
rw [map_LocalizedModules, hx, ← mk_cancel_common_left ⟨a, aS⟩ s m, mk_smul])
y)
fun ⟨x, hx⟩ ↦ by
revert hx
refine induction_on (fun m s hx ↦ ?_) x
rw [← hx, map_LocalizedModules, map_LocalizedModules, (ex (g m)).2 ⟨m, rfl⟩, zero_mk]
