English
If f: P → M and g: Q → N are injective linear maps between R-modules, and M,N are flat, then the induced map TensorProduct.map f g : P ⊗_R Q → M ⊗_R N is injective.
Русский
Если f: P → M и g: Q → N — инъективные линейные отображения между R-модулями, M и N плоские, то индукционное отображение TensorProduct.map f g: P ⊗ Q → M ⊗ N инъективно.
LaTeX
$$$\\forall f:\\, P \\to_{R} M\\; (g:\\, Q \\to_{R} N)\\; [\\text{Module.Flat } R M]\\ [\\text{Module.Flat } R Q],\\; \\text{Injective}(f) \\to \\text{Injective}(g) \\to \\text{Injective}(\\mathrm{TensorProduct.map}\,f\,g)$$$
Lean4
/-- Tensor product of injective maps are injective under some flatness conditions.
Also see `TensorProduct.map_injective_of_flat_flat'` and
`TensorProduct.map_injective_of_flat_flat_of_isDomain` for different flatness conditions. -/
theorem map_injective_of_flat_flat (f : P →ₗ[R] M) (g : Q →ₗ[R] N) [Module.Flat R M] [Module.Flat R Q]
(hf : Function.Injective f) (hg : Function.Injective g) : Function.Injective (TensorProduct.map f g) :=
by
rw [← LinearMap.lTensor_comp_rTensor]
exact
(Module.Flat.lTensor_preserves_injective_linearMap g hg).comp
(Module.Flat.rTensor_preserves_injective_linearMap f hf)
