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 uR}
{M : Type uM}
{N : Type uN}
[CommRing R]
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
(p : Submonoid R)
(f : M →ₗ[R] N)
[IsLocalizedModule p f]
(hp : p ≤ nonZeroDivisors R)
:
theorem
IsLocalizedModule.finrank_eq
{R : Type uR}
{M : Type uM}
{N : Type uN}
[CommRing R]
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
(p : Submonoid R)
(f : M →ₗ[R] N)
[IsLocalizedModule p f]
(hp : p ≤ nonZeroDivisors R)
:
theorem
IsLocalizedModule.rank_eq
{R : Type uR}
{M : Type uM}
[CommRing R]
[AddCommGroup M]
[Module R M]
(p : Submonoid R)
(hp : p ≤ nonZeroDivisors R)
{N : Type uM}
[AddCommGroup N]
[Module R N]
(f : M →ₗ[R] N)
[IsLocalizedModule p f]
:
theorem
IsLocalization.rank_eq
{R : Type uR}
(S : Type uS)
{N : Type uN}
[CommRing R]
[CommRing S]
[AddCommGroup N]
[Module R N]
[Algebra R S]
[Module S N]
[IsScalarTower R S N]
(p : Submonoid R)
[IsLocalization p S]
(hp : p ≤ nonZeroDivisors R)
:
theorem
exists_set_linearIndependent_of_isDomain
(R : Type uR)
(M : Type uM)
[CommRing R]
[AddCommGroup M]
[Module R M]
[IsDomain R]
:
∃ (s : Set M), Cardinal.mk ↑s = Module.rank R M ∧ LinearIndepOn R id s
theorem
rank_quotient_add_rank_of_isDomain
{R : Type uR}
{M : Type uM}
[CommRing R]
[AddCommGroup M]
[Module R M]
[IsDomain R]
(M' : Submodule R M)
:
The rank-nullity theorem for commutative domains. Also see rank_quotient_add_rank.
theorem
IsBaseChange.lift_rank_eq_of_le_nonZeroDivisors
{R : Type uR}
(S : Type uS)
{M : Type uM}
{N : Type uN}
[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)
[Module.Free S N]
[StrongRankCondition S]
{T : Type uT}
[CommRing T]
[Algebra R T]
(hpT : Algebra.algebraMapSubmonoid T p ≤ nonZeroDivisors T)
[StrongRankCondition (TensorProduct R S T)]
{P : Type uP}
[AddCommGroup P]
[Module R P]
[Module T P]
[IsScalarTower R T P]
{g : M →ₗ[R] P}
(bc : IsBaseChange T g)
:
theorem
IsBaseChange.finrank_eq_of_le_nonZeroDivisors
{R : Type uR}
(S : Type uS)
{M : Type uM}
{N : Type uN}
[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)
[Module.Free S N]
[StrongRankCondition S]
{T : Type uT}
[CommRing T]
[Algebra R T]
(hpT : Algebra.algebraMapSubmonoid T p ≤ nonZeroDivisors T)
[StrongRankCondition (TensorProduct R S T)]
{P : Type uP}
[AddCommGroup P]
[Module R P]
[Module T P]
[IsScalarTower R T P]
{g : M →ₗ[R] P}
(bc : IsBaseChange T g)
:
theorem
IsBaseChange.rank_eq_of_le_nonZeroDivisors
{R : Type uR}
(S : Type uS)
{M : Type uM}
{N : Type uN}
[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)
[Module.Free S N]
[StrongRankCondition S]
{T : Type uT}
[CommRing T]
[Algebra R T]
(hpT : Algebra.algebraMapSubmonoid T p ≤ nonZeroDivisors T)
[StrongRankCondition (TensorProduct R S T)]
{P : Type uM}
[AddCommGroup P]
[Module R P]
[Module T P]
[IsScalarTower R T P]
{g : M →ₗ[R] P}
(bc : IsBaseChange T g)
:
theorem
IsBaseChange.lift_rank_eq
{R : Type uR}
{M : Type uM}
[CommRing R]
[AddCommGroup M]
[Module R M]
{T : Type uT}
[CommRing T]
[NoZeroDivisors T]
[Algebra R T]
[FaithfulSMul R T]
{P : Type uP}
[AddCommGroup P]
[Module R P]
[Module T P]
[IsScalarTower R T P]
{g : M →ₗ[R] P}
(bc : IsBaseChange T g)
:
theorem
IsBaseChange.finrank_eq
{R : Type uR}
{M : Type uM}
[CommRing R]
[AddCommGroup M]
[Module R M]
{T : Type uT}
[CommRing T]
[NoZeroDivisors T]
[Algebra R T]
[FaithfulSMul R T]
{P : Type uP}
[AddCommGroup P]
[Module R P]
[Module T P]
[IsScalarTower R T P]
{g : M →ₗ[R] P}
(bc : IsBaseChange T g)
:
theorem
IsBaseChange.rank_eq
{R : Type uR}
{M : Type uM}
[CommRing R]
[AddCommGroup M]
[Module R M]
{T : Type uT}
[CommRing T]
[NoZeroDivisors T]
[Algebra R T]
[FaithfulSMul R T]
{P : Type uM}
[AddCommGroup P]
[Module R P]
[Module T P]
[IsScalarTower R T P]
{g : M →ₗ[R] P}
(bc : IsBaseChange T g)
:
theorem
aleph0_le_rank_of_isEmpty_oreSet
{R : Type u_1}
[Ring R]
[IsDomain R]
(hS : IsEmpty (OreLocalization.OreSet (nonZeroDivisors 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]
: