Theorems · Theorem · commutative algebra

Module.FaithfullyFlat.iff_exact_iff_rTensor_exact

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

Defined in

Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule