Theorems · Theorem · commutative algebra

LocalizedModule.map_exact

∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M₀ : Type u_2} [inst_1 : AddCommMonoid M₀]
  [inst_2 : Module R M₀] {M₁ : Type u_3} [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] {M₂ : Type u_4}
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R M₂] (g : M₀ →ₗ[R] M₁) (h : M₁ →ₗ[R] M₂),
  Function.Exact ⇑g ⇑h →
    Function.Exact ⇑((IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M₀) (LocalizedModule.mkLinearMap S M₁)) g)
      ⇑((IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M₁) (LocalizedModule.mkLinearMap S M₂)) h)

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

Defined in

Mathlib.Algebra.Module.LocalizedModule.Exact

Cited by

1 results in Mathlib

Foundations

Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModuleAddCommMonoidModule