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
IsLocalization.finrank_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
IsLocalization.linearIndepOn_finsetIntegerMultiple
{R : Type uR}
{S : Type uS}
[CommRing R]
[CommRing S]
[Algebra R S]
{A : Type u_1}
[CommRing A]
[Algebra S A]
[Algebra R A]
[IsScalarTower R S A]
(M : Submonoid S)
[IsLocalization M A]
[FaithfulSMul S A]
{s : Finset A}
(hs : LinearIndepOn R id ↑s)
[DecidableEq S]
:
LinearIndepOn R id ↑(finsetIntegerMultiple M s)
theorem
IsFractionRing.rank_right_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]
[IsFractionRing R S]
:
Given IsScalarTower R S N, if S is the fraction ring of R, then the rank rank S N
of the right part of the tower equals the rank rank R N of the whole tower.
See IsFractionRing.finrank_right_eq for the finrank version.
theorem
IsFractionRing.finrank_right_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]
[IsFractionRing R S]
:
Given IsScalarTower R S N, if S is the fraction ring of R, then the finrank finrank S N
of the right part of the tower equals the finrank finrank R N of the whole tower.
See IsFractionRing.rank_right_eq for the rank version.
See IsFractionRing.finrank_left_eq for the left version.
See IsFractionRing.finrank_eq for the simultaneous version.
theorem
IsFractionRing.finrank_left_eq
(R : Type uR)
(S : Type uS)
[CommRing R]
[CommRing S]
[Algebra R S]
(A : Type u_1)
[CommRing A]
[Algebra S A]
[Algebra R A]
[IsScalarTower R S A]
[IsFractionRing S A]
:
Given IsScalarTower R S A, if A is the fraction ring of S, then the finrank finrank R S
of the left part of the tower equals the finrank finrank R A of the whole tower.
See IsFractionRing.finrank_right_eq for the right version.
See IsFractionRing.finrank_eq for the simultaneous version.
theorem
IsFractionRing.finrank_eq
(A : Type u_1)
(K : Type u_2)
(B : Type u_3)
(L : Type u_4)
[CommRing A]
[CommRing K]
[CommRing B]
[CommRing L]
[Algebra A B]
[Module K L]
[Algebra A K]
[Algebra B L]
[Algebra A L]
[IsScalarTower A K L]
[IsScalarTower A B L]
[IsFractionRing A K]
[IsFractionRing B L]
:
If K is the fraction ring of A and L is the fraction ring of B, then the finrank
finrank K L of the fraction rings equals the finrank finrank A B of the base rings.
See IsFractionRing.finrank_left_eq and IsFractionRing.finrank_right_eq for one-sided versions.
See Algebra.IsAlgebraic.rank_of_isFractionRing for a rank version with additional assumptions.
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]
: