Flat modules in domains

We show that the tensor product of two injective linear maps is injective if the sources are flat and the ring is an integral domain.

theorem TensorProduct.map_injective_of_flat_flat_of_isDomain {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : Type u_4} {Q : Type u_5} [AddCommGroup P] [Module R P] [AddCommGroup Q] [Module R Q] [IsDomain R] (f : P →ₗ[R] M) (g : Q →ₗ[R] N) [H : Module.Flat R P] [Module.Flat R Q] (hf : Function.Injective ⇑f) (hg : Function.Injective ⇑g) : Function.Injective ⇑(map f g)

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 LinearIndependent.tmul_of_isDomain {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsDomain R] {ι : Type u_6} {ι' : Type u_7} {v : ι → M} (hv : LinearIndependent R v) {w : ι' → N} (hw : LinearIndependent R w) : LinearIndependent R fun (i : ι × ι') => v i.1 ⊗ₜ[R] w i.2

Tensor product of linearly independent families is linearly independent over domains. This is true over non-domains if one of the modules is flat. See LinearIndependent.tmul_of_flat_left.