lTensor_preserves_injective_linearMap

English

Flat R M is equivalent to the property that f ⊗ 1_M is injective for all injective linear maps f.

Русский

Pлоскость R M эквивалентна свойству: для любого инъективного линейного отображения f, f ⊗ 1_M инъективно.

LaTeX

$$$Flat\ R\ M \iff \forall f: N \to P\ (Injective\ f)\\Injective(f\otimes M)$$

Lean4

/-- If `M` is a flat module, then `𝟙 M ⊗ f` is injective for all injective linear maps `f`. -/
theorem lTensor_preserves_injective_linearMap [Flat R M] (f : N →ₗ[R] P) (hf : Function.Injective f) :
    Function.Injective (f.lTensor M) :=
  (f.lTensor_inj_iff_rTensor_inj M).2 (rTensor_preserves_injective_linearMap f hf)

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