English
Tensor product maps preserve injectivity under flatness: if f: P → M and g: Q → N are injective, with P,N flat, then TensorProduct.map f g is injective.
Русский
Отображения TensorProduct.map сохраняют инъективность при плоскостях: если f: P → M и g: Q → N инъективны, и P,N плоские, то TensorProduct.map f g инъективно.
LaTeX
$$$\\forall f:\\, P \\to_{R} M\\; (g:\\, Q \\to_{R} N)\\; [\\text{Module.Flat } R P]\\ [\\text{Module.Flat } R N],\\; \\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 P] [Module.Flat R N]
(hf : Function.Injective f) (hg : Function.Injective g) : Function.Injective (TensorProduct.map f g) :=
by
rw [← LinearMap.rTensor_comp_lTensor]
exact
(Module.Flat.rTensor_preserves_injective_linearMap f hf).comp
(Module.Flat.lTensor_preserves_injective_linearMap g hg)
