Commit 2024-06-25 09:01 0ba8580b
View on Github →feat(Algebra/Module/LocalizedModule): Prove that localization is exact (#13790) Given localizations f₀ : M₀ → M₀', f₁ : M₁ → M₁', and f₂ : M₂ → M₂', and an exact sequence consisting of g : M₀ → M₁ and h : M₁ → M₂, prove that (map S f₀ f₁ g) : M₀' → M₁' and (map S f₁ f₂ h) : M₁' → M₂' form an exact sequence. Also fix a typo in the documentation of IsLocalizedModule.lift.