includeLeft_injective — Mathlib

English

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

Русский

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

LaTeX

$$$Flat\ R A \land Injective( algebraMap\ R B) \Rightarrow Injective( includeLeft )$$$

Lean4

theorem includeLeft_injective [Module.Flat R A] (hb : Function.Injective (algebraMap R B)) :
    Function.Injective (includeLeft : A →ₐ[S] A ⊗[R] B) :=
  by
  convert
    Module.Flat.lTensor_preserves_injective_linearMap (M := A) (Algebra.linearMap R B) hb |>.comp
      (_root_.TensorProduct.rid R A).symm.injective
  ext; simp

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