Theorems · Theorem · commutative algebra

Module.FaithfullyFlat.lTensor_reflects_exact

∀ (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.lTensor M l12) ⇑(LinearMap.lTensor M l23) → Function.Exact ⇑l12 ⇑l23

Defined in

Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleAddCommGroupModuleAddCommGroupModuleAddCommGroupModuleModule.FaithfullyFlat