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