English
Tensor product maps are injective under flatness when R is a domain; if f and g are injective linear maps between modules, then TensorProduct.map f g is injective.
Русский
Тензорные отображения инъективны при плоскости и R является областью; если f,g — инъективные линейные отображения, то TensorProduct.map f g инъективно.
LaTeX
$$$\\forall R \\,(M,N,P,Q),\\; [\\text{IsDomain } R]\\; (f:P\\to M) (g: Q\\to N) \\; \\Rightarrow \\text{Injective}(TensorProduct.map f g)$$$
Lean4
/-- Tensor product of injective maps over domains are injective under some flatness conditions.
Also see `TensorProduct.map_injective_of_flat_flat`
for different flatness conditions but without the domain assumption. -/
theorem map_injective_of_flat_flat_of_isDomain (f : P →ₗ[R] M) (g : Q →ₗ[R] N) [H : Module.Flat R P] [Module.Flat R Q]
(hf : Injective f) (hg : Injective g) : Injective (TensorProduct.map f g) :=
by
let K := FractionRing R
refine .of_comp (f := TensorProduct.mk R K _ 1) ?_
have H₁ :=
TensorProduct.map_injective_of_flat_flat (f.baseChange K) (g.baseChange K)
(Module.Flat.lTensor_preserves_injective_linearMap f hf) (Module.Flat.lTensor_preserves_injective_linearMap g hg)
have H₂ := (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q).symm.injective
have H₃ := (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N).injective
have H₄ := (AlgebraTensorModule.assoc R R K K P Q).symm.injective
have H₅ := (AlgebraTensorModule.assoc R R K K M N).injective
have H₆ :=
Module.Flat.rTensor_preserves_injective_linearMap (M := P ⊗[R] Q) (Algebra.linearMap R K)
(FaithfulSMul.algebraMap_injective R K)
have H₇ := (TensorProduct.lid R (P ⊗[R] Q)).symm.injective
convert H₅.comp <| H₃.comp <| H₁.comp <| H₂.comp <| H₄.comp <| H₆.comp <| H₇
dsimp only [← LinearMap.coe_comp, ← LinearEquiv.coe_toLinearMap, ← @LinearMap.coe_restrictScalars R K]
congr! 1
ext p q
change
(1 : K) ⊗ₜ[R] (f p ⊗ₜ[R] g q) =
(AlgebraTensorModule.assoc R R K K M N) (((1 : K) • (algebraMap R K) 1 ⊗ₜ[R] f p) ⊗ₜ[R] g q)
simp only [map_one, one_smul, AlgebraTensorModule.assoc_tmul]
