iff_lTensor_preserves_injective_linearMap'

English

A variant of the previous result for lTensor preserves injectivity.

Русский

Вариант предыдущего результата для lTensor сохраняет инъективность.

LaTeX

$$$Flat\ R\ M \iff (\forall N,N' (f : N \to N'), \text{Injective}(f) \Rightarrow \text{Injective}(f\,\mathrm{lTensor}\ M))$$$

Lean4

/-- `M` is flat if and only if `𝟙 M ⊗ f` is injective whenever `f` is an injective linear map.
  See `Module.Flat.iff_lTensor_preserves_injective_linearMap` to specialize the universe of
  `N, N', N''` to `Type (max u v)`. -/
theorem iff_lTensor_preserves_injective_linearMap' [Small.{v'} R] :
    Flat R M ↔
      ∀ ⦃N N' : Type v'⦄ [AddCommGroup N] [AddCommGroup N'] [Module R N] [Module R N'] (f : N →ₗ[R] N'),
        Function.Injective f → Function.Injective (f.lTensor M) :=
  by simp_rw [iff_rTensor_preserves_injective_linearMap', LinearMap.lTensor_inj_iff_rTensor_inj]

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