iff_lTensor_preserves_injective_linearMap

English

Flatness is characterized by the injectivity of lTensor under injective f.

Русский

Плоскостность характеризуется инъективностью lTensor при инъективном f.

LaTeX

$$$Flat\ R\ M \iff \forall (N,N'), (f: N \to N'), Injective(f) \Rightarrow 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 generalize the universe of
  `N, N', N''` to any universe that is higher than `R` and `M`. -/
theorem iff_lTensor_preserves_injective_linearMap :
    Flat R M ↔
      ∀ ⦃N N' : Type (max u v)⦄ [AddCommGroup N] [AddCommGroup N'] [Module R N] [Module R N'] (f : N →ₗ[R] N'),
        Function.Injective f → Function.Injective (f.lTensor M) :=
  iff_lTensor_preserves_injective_linearMap'

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