Theorems · Theorem · commutative algebra

exact_of_isLocalized_maximal

∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {L : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid L]
  [inst_6 : Module R L] (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6)
  [inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_8 : (P : Ideal R) → [inst_8 : P.IsMaximal] → Module R (Mₚ P)]
  (f : (P : Ideal R) → [inst_9 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [inst_9 : ∀ (P : Ideal R) [inst_9 : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)]
  (Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7)
  [inst_10 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)]
  [inst_11 : (P : Ideal R) → [inst_11 : P.IsMaximal] → Module R (Nₚ P)]
  (g : (P : Ideal R) → [inst_12 : P.IsMaximal] → N →ₗ[R] Nₚ P)
  [inst_12 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsLocalizedModule.AtPrime P (g P)]
  (Lₚ : (P : Ideal R) → [P.IsMaximal] → Type u_8)
  [inst_13 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Lₚ P)]
  [inst_14 : (P : Ideal R) → [inst_14 : P.IsMaximal] → Module R (Lₚ P)]
  (h : (P : Ideal R) → [inst_15 : P.IsMaximal] → L →ₗ[R] Lₚ P)
  [inst_15 : ∀ (P : Ideal R) [inst_15 : P.IsMaximal], IsLocalizedModule.AtPrime P (h P)] (F : M →ₗ[R] N)
  (G : N →ₗ[R] L),
  (∀ (J : Ideal R) [inst_16 : J.IsMaximal],
      Function.Exact ⇑((IsLocalizedModule.map J.primeCompl (f J) (g J)) F)
        ⇑((IsLocalizedModule.map J.primeCompl (g J) (h J)) G)) →
    Function.Exact ⇑F ⇑G

Defined in

Mathlib.RingTheory.LocalProperties.Exactness

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModuleAddCommMonoidModuleAddCommMonoidModuleIsLocalizedModule.AtPrimeAddCommMonoidModuleIsLocalizedModule.AtPrimeAddCommMonoidModuleIsLocalizedModule.AtPrime