Documentation

Mathlib.LinearAlgebra.Dimension.Localization

Rank of localization #

Main statements #

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.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] :
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.

Equations
  • =

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