iff_lTensor_injective' — Mathlib

English

A flat R-module M is equivalent to injectivity of all lTensor variants with I-subtype.

Русский

Плоскость M эквивалентна инъективности всех вариаций lTensor с I-subtype.

LaTeX

$$$\\text{Flat}(R,M) \\iff \\forall I, \\text{FG} \\rightarrow \\text{Injective}(\\mathrm{lTensor}(M, I.subtype))$$$

Lean4

/-- The `lTensor`-variant of `iff_rTensor_injective'`. . -/
theorem iff_lTensor_injective' : Flat R M ↔ ∀ (I : Ideal R), Function.Injective (lTensor M I.subtype) := by
  simpa [← comm_comp_rTensor_comp_comm_eq] using iff_rTensor_injective'

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