Supplementary results on torsion modules #
theorem
Module.IsTorsion.not_disjoint_nonZeroDivisors_of_mem_support
{A : Type u_1}
[CommRing A]
{M : Type u_2}
[AddCommGroup M]
[Module A M]
(H : IsTorsion A M)
(p : PrimeSpectrum A)
:
theorem
Module.IsTorsion.one_le_primeHeight_of_mem_support
{A : Type u_1}
[CommRing A]
{M : Type u_2}
[AddCommGroup M]
[Module A M]
(H : IsTorsion A M)
(p : PrimeSpectrum A)
:
p ∈ support A M → 1 ≤ p.asIdeal.primeHeight
theorem
Module.isTorsion_iff_subsingleton_localizedModule_nonZeroDivisors
{A : Type u_1}
[CommRing A]
{M : Type u_2}
[AddCommGroup M]
[Module A M]
:
theorem
Module.IsTorsion.subsingleton_localizedModule_nonZeroDivisors
{A : Type u_1}
[CommRing A]
{M : Type u_2}
[AddCommGroup M]
[Module A M]
:
IsTorsion A M → Subsingleton (LocalizedModule (nonZeroDivisors A) M)
Alias of the forward direction of Module.isTorsion_iff_subsingleton_localizedModule_nonZeroDivisors.
theorem
Module.IsTorsion.injective
{A : Type u_1}
[CommRing A]
{M : Type u_2}
[AddCommGroup M]
[Module A M]
{M' : Type u_3}
[AddCommGroup M']
[Module A M']
(H : IsTorsion A M')
{f : M →ₗ[A] M'}
(hf : Function.Injective ⇑f)
:
IsTorsion A M
theorem
Module.IsTorsion.surjective
{A : Type u_1}
[CommRing A]
{M : Type u_2}
[AddCommGroup M]
[Module A M]
{M' : Type u_3}
[AddCommGroup M']
[Module A M']
(H : IsTorsion A M)
{f : M →ₗ[A] M'}
(hf : Function.Surjective ⇑f)
:
IsTorsion A M'
theorem
LinearEquiv.isTorsion
{A : Type u_1}
[CommRing A]
{M : Type u_2}
[AddCommGroup M]
[Module A M]
{M' : Type u_3}
[AddCommGroup M']
[Module A M']
(f : M ≃ₗ[A] M')
:
theorem
Function.Exact.subsingleton
{M : Type u_1}
{N : Type u_2}
{P : Type u_3}
{f : M → N}
{g : N → P}
[Zero P]
(H : Exact f g)
[Subsingleton M]
[Subsingleton P]
:
theorem
Module.IsTorsion.exact
{A : Type u_1}
[CommRing A]
{M : Type u_2}
[AddCommGroup M]
[Module A M]
{M' : Type u_3}
[AddCommGroup M']
[Module A M']
{M'' : Type u_4}
[AddCommGroup M'']
[Module A M'']
(h1 : IsTorsion A M)
(h2 : IsTorsion A M'')
(f : M →ₗ[A] M')
(g : M' →ₗ[A] M'')
(hfg : Function.Exact ⇑f ⇑g)
:
IsTorsion A M'
theorem
Module.IsTorsion.prod
{A : Type u_1}
[CommRing A]
{M : Type u_2}
[AddCommGroup M]
[Module A M]
{M'' : Type u_3}
[AddCommGroup M'']
[Module A M'']
(h1 : IsTorsion A M)
(h2 : IsTorsion A M'')
: