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.linearIndependent_lift {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) {ι : Type u_1} {v : ι → N} (hf : LinearIndependent S v) : ∃ (w : ι → M), LinearIndependent R w

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) : Cardinal.lift.{v, v'} (Module.rank S N) = Cardinal.lift.{v', v} (Module.rank R M)

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 exists_set_linearIndependent_of_isDomain (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [IsDomain R] : ∃ (s : Set M), Cardinal.mk ↑s = Module.rank R M ∧ LinearIndependent (ι := ↑s) R Subtype.val

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. Also see rank_quotient_add_rank.

instance IsDomain.hasRankNullity {R : Type u} [CommRing R] [IsDomain R] : HasRankNullity.{w, u} R

theorem aleph0_le_rank_of_isEmpty_oreSet {R : Type u_1} [Ring R] [IsDomain R] (hS : IsEmpty (OreLocalization.OreSet (nonZeroDivisors R))) : Cardinal.aleph0 ≤ Module.rank R R

A domain that is not (left) Ore is of infinite rank. See [Coh95] Proposition 1.3.6

theorem nonempty_oreSet_of_strongRankCondition {R : Type u_1} [Ring R] [IsDomain R] [StrongRankCondition R] : Nonempty (OreLocalization.OreSet (nonZeroDivisors R))