English
If i₁ and i₂ are injective and the corresponding modules are flat, then the induced map is injective.
Русский
Если 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)$$$
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_left_right (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₂
