map_id_injective_of_flat_right — Mathlib

English

In a tensor product setting, the map hf.map hg LinearMap.id is injective under flatness on the left.

Русский

В контексте тензорного произведения отображение hf.map hg LinearMap.id инъективно при плоскости слева.

LaTeX

$$$\\text{Injective}(hf.map\\, hg\\, LinearMap.id)$ with [Module.Flat R M], [Module.Flat R N] conditions$$

Lean4

theorem map_id_injective_of_flat_right {g : N₁ →ₗ[R] M₂ →ₗ[R] N} (hg : IsTensorProduct g) (i : M₁ →ₗ[R] N₁)
    (hi : Function.Injective i) [Module.Flat R M₂] : Function.Injective (hf.map hg i LinearMap.id) :=
  by
  have h : hf.map hg i LinearMap.id = hg.equiv ∘ i.rTensor M₂ ∘ hf.equiv.symm :=
    funext fun x ↦ hf.inductionOn x (by simp) (by simp) (fun _ _ hx hy ↦ by simp [hx, hy])
  simpa [h] using Module.Flat.rTensor_preserves_injective_linearMap i hi

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