Separating bilinear maps and torsion #
A module carrying a map that is linear and separating in its first argument, with values in a
torsion-free module, is itself torsion-free: if r is regular and r • x₁ = r • x₂, then
r • B (x₁ - x₂) y = B (r • x₁ - r • x₂) y = 0 forces B (x₁ - x₂) y = 0 for every y, so
x₁ = x₂. For instance, an abelian group carrying a nondegenerate integral bilinear form is
torsion-free, hence flat over ℤ.
Main results #
LinearMap.SeparatingLeft.isTorsionFree: a module with a left-separating map, linear in its first argument and semilinear in its second, into a torsion-free module is torsion-free.
theorem
LinearMap.SeparatingLeft.isTorsionFree
{R : Type u_1}
{S : Type u_2}
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
[CommSemiring R]
[CommSemiring S]
[AddCommGroup M]
[Module R M]
[AddCommMonoid N]
[Module S N]
[AddCommGroup P]
[Module R P]
[Module.IsTorsionFree R P]
{I : S →+* R}
{B : M →ₗ[R] N →ₛₗ[I] P}
(hB : B.SeparatingLeft)
:
A module carrying a map that is linear in its first argument, semilinear in its second and separates points in its first argument, with values in a torsion-free module, is torsion-free.