iff_exact_iff_lTensor_exact — Mathlib

English

For M faithfully flat, Nontrivial(M ⊗R N) ↔ Nontrivial N.

Русский

Для верноподобной M: непустость M ⊗R N эквивалентна непустости N.

LaTeX

$$[simp] \forall N\ [\text{Module }R N], [\text{Module.FaithfullyFlat }R M] : \operatorname{Nontrivial}(M \otimes_R N) \iff \operatorname{Nontrivial}(N)$$

Lean4

theorem iff_exact_iff_lTensor_exact :
    FaithfullyFlat R M ↔
      (∀ {N1 : Type max u v} [AddCommGroup N1] [Module R N1] {N2 : Type max u v} [AddCommGroup N2] [Module R N2]
        {N3 : Type max u v} [AddCommGroup N3] [Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3),
        Function.Exact l12 l23 ↔ Function.Exact (l12.lTensor M) (l23.lTensor M)) :=
  by simp only [iff_exact_iff_rTensor_exact, LinearMap.rTensor_exact_iff_lTensor_exact]

Похожие утверждения