Localization of modules is an exact functor

Main definitions

• LocalizedModule.map_exact: Localization of modules is an exact functor.
• IsLocalizedModule.map_exact: A variant expressed in terms of IsLocalizedModule.

theorem LocalizedModule.map_exact {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M₀ : Type u_2} [AddCommMonoid M₀] [Module R M₀] {M₁ : Type u_3} [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_4} [AddCommMonoid M₂] [Module R M₂] (g : M₀ →ₗ[R] M₁) (h : M₁ →ₗ[R] M₂) (ex : Function.Exact ⇑g ⇑h) : Function.Exact ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) ⇑((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂)) h)

Localization of modules is an exact functor, proven here for LocalizedModule. See IsLocalizedModule.map_exact for the more general version.

theorem IsLocalizedModule.map_exact {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M₀ : Type u_2} {M₀' : Type u_5} [AddCommMonoid M₀] [AddCommMonoid M₀'] [Module R M₀] [Module R M₀'] (f₀ : M₀ →ₗ[R] M₀') [IsLocalizedModule S f₀] {M₁ : Type u_3} {M₁' : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₁'] [Module R M₁] [Module R M₁'] (f₁ : M₁ →ₗ[R] M₁') [IsLocalizedModule S f₁] {M₂ : Type u_4} {M₂' : Type u_7} [AddCommMonoid M₂] [AddCommMonoid M₂'] [Module R M₂] [Module R M₂'] (f₂ : M₂ →ₗ[R] M₂') [IsLocalizedModule S f₂] (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)

Localization of modules is an exact functor.