Rank of localization #
Main statements #
IsLocalizedModule.lift_rank_eq:rank_Rₚ Mₚ = rank R M.rank_quotient_add_rank_of_isDomain: The rank-nullity theorem for commutative domains.
theorem
IsLocalizedModule.lift_rank_eq
{R : Type u}
(S : Type u')
{M : Type v}
{N : Type v'}
[CommRing R]
[CommRing S]
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
[Algebra R S]
[Module S N]
[IsScalarTower R S N]
(p : Submonoid R)
[IsLocalization p S]
(f : M →ₗ[R] N)
[IsLocalizedModule p f]
(hp : p ≤ nonZeroDivisors R)
:
theorem
IsLocalizedModule.rank_eq
{R : Type u}
(S : Type u')
{M : Type v}
[CommRing R]
[CommRing S]
[AddCommGroup M]
[Module R M]
[Algebra R S]
(p : Submonoid R)
[IsLocalization p S]
(hp : p ≤ nonZeroDivisors R)
{N : Type v}
[AddCommGroup N]
[Module R N]
[Module S N]
[IsScalarTower R S N]
(f : M →ₗ[R] N)
[IsLocalizedModule p f]
:
Module.rank S N = Module.rank R M
theorem
rank_quotient_add_rank_of_isDomain
{R : Type u}
{M : Type v}
[CommRing R]
[AddCommGroup M]
[Module R M]
[IsDomain R]
(M' : Submodule R M)
:
Module.rank R (M ⧸ M') + Module.rank R ↥M' = Module.rank R M
The rank-nullity theorem for commutative domains.