Theorems · Theorem · commutative algebra

Module.FaithfullyFlat.range_le_ker_of_exact_rTensor

∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N1 : Type u_1}
  [inst_3 : AddCommGroup N1] [inst_4 : Module R N1] {N2 : Type u_2} [inst_5 : AddCommGroup N2] [inst_6 : Module R N2]
  {N3 : Type u_3} [inst_7 : AddCommGroup N3] [inst_8 : Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3)
  [fl : Module.FaithfullyFlat R M],
  Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23) → l12.range ≤ l23.ker

If M is faithfully flat, then exactness of N₁ ⊗ M -> N₂ ⊗ M -> N₃ ⊗ M implies that the composition N₁ -> N₂ -> N₃ is 0. Implementation detail, please use rTensor_reflects_exact instead.

Defined in

Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleAddCommGroupModuleAddCommGroupModuleAddCommGroupModuleModule.FaithfullyFlat