iff_lTensor_preserves_injective_linearMapₛ

English

Flatness is equivalent to the property that all lTensor maps are injective iff rTensor maps are injective.

Русский

Плоскость эквивалентна свойству: все lTensor инъективны тогда и только тогда, когда все rTensor инъективны.

LaTeX

$$Flat R M ↔ ∀ ⦃N N'⦄ f : N →ₗ[R] N', Injective f → Injective (f.lTensor M)$$

Lean4

/-- `M` is flat if and only if `𝟙 M ⊗ f` is injective whenever `f` is an injective linear map
in a universe that `R` fits in. -/
theorem iff_lTensor_preserves_injective_linearMapₛ [Small.{v'} R] :
    Flat R M ↔
      ∀ ⦃N N' : Type v'⦄ [AddCommMonoid N] [AddCommMonoid 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]

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