English
If i₁ and i₂ are injective and both modules are flat, then the induced map hf.map hg i₁ i₂ is injective.
Русский
Если i₁ и i₂ инъективны, и обе модуля плоские, то отображение hf.map hg i₁ i₂ инъективно.
LaTeX
$$$\\forall i_1,i_2,\\; \\text{Injective}(i_1)\\to\\text{Injective}(i_2)\\to\\text{Injective}(hf.map hg i_1 i_2)$ under flatness hypotheses$$
Lean4
/-- If `M₂` and `N₁` are flat `R`-modules, `i₁ : M₁ →ₗ[R] N₁` and `i₂ : M₂ →ₗ[R] N₂` are injective
linear maps, then the linear map `i : M ≅ M₁ ⊗[R] M₂ →ₗ[R] N₁ ⊗[R] N₂ ≅ N` induced by `i₁`
and `i₂` is injective.
See `IsTensorProduct.map_injective_of_flat'` for different flatness conditions. -/
theorem map_injective_of_flat_right_left (h₁ : Function.Injective i₁) (h₂ : Function.Injective i₂) [Module.Flat R M₂]
[Module.Flat R N₁] : Function.Injective (hf.map hg i₁ i₂) :=
by
have h : hf.map hg i₁ i₂ = hg.equiv ∘ TensorProduct.map i₁ i₂ ∘ hf.equiv.symm :=
funext fun x ↦ hf.inductionOn x (by simp) (by simp) (fun _ _ hx hy ↦ by simp [hx, hy])
simpa [h] using map_injective_of_flat_flat i₁ i₂ h₁ h₂
