includeRight_injective — Mathlib

English

If B is flat over R and the map algebraMap R A is injective, then the includeRight map is injective.

Русский

Если B плосок над R и отображение algebraMap R A инъективно, тогда includeRight инъективно.

LaTeX

$$$Module.Flat R B \land Injective( algebraMap R A) \Rightarrow Injective( includeRight )$$$

Lean4

theorem includeRight_injective [Module.Flat R B] (ha : Function.Injective (algebraMap R A)) :
    Function.Injective (includeRight : B →ₐ[R] A ⊗[R] B) :=
  by
  convert
    Module.Flat.rTensor_preserves_injective_linearMap (M := B) (Algebra.linearMap R A) ha |>.comp
      (_root_.TensorProduct.lid R B).symm.injective
  ext; simp

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