Rank of various constructions #
Main statements #
rank_quotient_add_rank_le:rank M/N + rank N ≤ rank M.lift_rank_add_lift_rank_le_rank_prod:rank M × N ≤ rank M + rank N.rank_span_le_of_finite:rank (span s) ≤ #sfor finites.
For free modules, we have
rank_prod:rank M × N = rank M + rank N.rank_finsupp:rank (ι →₀ M) = #ι * rank Mrank_directSum:rank (⨁ Mᵢ) = ∑ rank Mᵢrank_tensorProduct:rank (M ⊗ N) = rank M * rank N.
Lemmas for ranks of submodules and subalgebras are also provided. We have finrank variants for most lemmas as well.
theorem
rank_quotient_add_rank_le
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[Nontrivial R]
(M' : Submodule R M)
:
Module.rank R (M ⧸ M') + Module.rank R ↥M' ≤ Module.rank R M
theorem
rank_quotient_le
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
(p : Submodule R M)
:
Module.rank R (M ⧸ p) ≤ Module.rank R M
theorem
rank_quotient_eq_of_le_torsion
{R : Type u_2}
{M : Type u_3}
[CommRing R]
[AddCommGroup M]
[Module R M]
{M' : Submodule R M}
(hN : M' ≤ Submodule.torsion R M)
:
Module.rank R (M ⧸ M') = Module.rank R M
@[simp]
theorem
rank_ulift
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
:
Module.rank R (ULift.{w, v} M) = Cardinal.lift.{w, v} (Module.rank R M)
@[simp]
theorem
lift_rank_add_lift_rank_le_rank_prod
(R : Type u)
(M : Type v)
(M' : Type v')
[Ring R]
[AddCommGroup M]
[AddCommGroup M']
[Module R M]
[Module R M']
[Nontrivial R]
:
Cardinal.lift.{v', v} (Module.rank R M) + Cardinal.lift.{v, v'} (Module.rank R M') ≤ Module.rank R (M × M')
theorem
rank_add_rank_le_rank_prod
(R : Type u)
(M : Type v)
{M₁ : Type v}
[Ring R]
[AddCommGroup M]
[AddCommGroup M₁]
[Module R M]
[Module R M₁]
[Nontrivial R]
:
Module.rank R M + Module.rank R M₁ ≤ Module.rank R (M × M₁)
@[simp]
theorem
rank_prod
{R : Type u}
{M : Type v}
{M' : Type v'}
[Ring R]
[AddCommGroup M]
[AddCommGroup M']
[Module R M]
[Module R M']
[StrongRankCondition R]
[Module.Free R M]
[Module.Free R M']
:
Module.rank R (M × M') = Cardinal.lift.{v', v} (Module.rank R M) + Cardinal.lift.{v, v'} (Module.rank R M')
If M and M' are free, then the rank of M × M' is
(Module.rank R M).lift + (Module.rank R M').lift.
theorem
rank_prod'
{R : Type u}
{M : Type v}
{M₁ : Type v}
[Ring R]
[AddCommGroup M]
[AddCommGroup M₁]
[Module R M]
[Module R M₁]
[StrongRankCondition R]
[Module.Free R M]
[Module.Free R M₁]
:
Module.rank R (M × M₁) = Module.rank R M + Module.rank R M₁
If M and M' are free (and lie in the same universe), the rank of M × M' is
(Module.rank R M) + (Module.rank R M').
@[simp]
theorem
FiniteDimensional.finrank_prod
{R : Type u}
{M : Type v}
{M' : Type v'}
[Ring R]
[AddCommGroup M]
[AddCommGroup M']
[Module R M]
[Module R M']
[StrongRankCondition R]
[Module.Free R M]
[Module.Free R M']
[Module.Finite R M]
[Module.Finite R M']
:
FiniteDimensional.finrank R (M × M') = FiniteDimensional.finrank R M + FiniteDimensional.finrank R M'
The finrank of M × M' is (finrank R M) + (finrank R M').
@[simp]
theorem
rank_finsupp
(R : Type u)
(M : Type v)
[Ring R]
[AddCommGroup M]
[Module R M]
[StrongRankCondition R]
[Module.Free R M]
(ι : Type w)
:
Module.rank R (ι →₀ M) = Cardinal.lift.{v, w} (Cardinal.mk ι) * Cardinal.lift.{w, v} (Module.rank R M)
theorem
rank_finsupp'
(R : Type u)
(M : Type v)
[Ring R]
[AddCommGroup M]
[Module R M]
[StrongRankCondition R]
[Module.Free R M]
(ι : Type v)
:
Module.rank R (ι →₀ M) = Cardinal.mk ι * Module.rank R M
theorem
rank_finsupp_self
(R : Type u)
[Ring R]
[StrongRankCondition R]
(ι : Type w)
:
Module.rank R (ι →₀ R) = Cardinal.lift.{u, w} (Cardinal.mk ι)
The rank of (ι →₀ R) is (#ι).lift.
theorem
rank_finsupp_self'
(R : Type u)
[Ring R]
[StrongRankCondition R]
{ι : Type u}
:
Module.rank R (ι →₀ R) = Cardinal.mk ι
If R and ι lie in the same universe, the rank of (ι →₀ R) is # ι.
@[simp]
theorem
rank_directSum
(R : Type u)
[Ring R]
[StrongRankCondition R]
{ι : Type v}
(M : ι → Type w)
[(i : ι) → AddCommGroup (M i)]
[(i : ι) → Module R (M i)]
[∀ (i : ι), Module.Free R (M i)]
:
Module.rank R (DirectSum ι fun (i : ι) => M i) = Cardinal.sum fun (i : ι) => Module.rank R (M i)
The rank of the direct sum is the sum of the ranks.
@[simp]
theorem
rank_matrix
(R : Type u)
[Ring R]
[StrongRankCondition R]
(m : Type v)
(n : Type w)
[Finite m]
[Finite n]
:
Module.rank R (Matrix m n R) = Cardinal.lift.{max v w u, v} (Cardinal.mk m) * Cardinal.lift.{max v w u, w} (Cardinal.mk n)
If m and n are Fintype, the rank of m × n matrices is (#m).lift * (#n).lift.
@[simp]
theorem
rank_matrix'
(R : Type u)
[Ring R]
[StrongRankCondition R]
(m : Type v)
(n : Type v)
[Finite m]
[Finite n]
:
Module.rank R (Matrix m n R) = Cardinal.lift.{u, v} (Cardinal.mk m * Cardinal.mk n)
If m and n are Fintype that lie in the same universe, the rank of m × n matrices is
(#n * #m).lift.
theorem
rank_matrix''
(R : Type u)
[Ring R]
[StrongRankCondition R]
(m : Type u)
(n : Type u)
[Finite m]
[Finite n]
:
Module.rank R (Matrix m n R) = Cardinal.mk m * Cardinal.mk n
If m and n are Fintype that lie in the same universe as R, the rank of m × n matrices
is # m * # n.
@[simp]
theorem
FiniteDimensional.finrank_finsupp
(R : Type u)
(M : Type v)
[Ring R]
[AddCommGroup M]
[Module R M]
[StrongRankCondition R]
[Module.Free R M]
{ι : Type v}
[Fintype ι]
:
FiniteDimensional.finrank R (ι →₀ M) = Fintype.card ι * FiniteDimensional.finrank R M
@[simp]
theorem
FiniteDimensional.finrank_finsupp_self
(R : Type u)
[Ring R]
[StrongRankCondition R]
{ι : Type v}
[Fintype ι]
:
FiniteDimensional.finrank R (ι →₀ R) = Fintype.card ι
The finrank of (ι →₀ R) is Fintype.card ι.
@[simp]
theorem
FiniteDimensional.finrank_directSum
(R : Type u)
[Ring R]
[StrongRankCondition R]
{ι : Type v}
[Fintype ι]
(M : ι → Type w)
[(i : ι) → AddCommGroup (M i)]
[(i : ι) → Module R (M i)]
[∀ (i : ι), Module.Free R (M i)]
[∀ (i : ι), Module.Finite R (M i)]
:
FiniteDimensional.finrank R (DirectSum ι fun (i : ι) => M i) = Finset.sum Finset.univ fun (i : ι) => FiniteDimensional.finrank R (M i)
The finrank of the direct sum is the sum of the finranks.
theorem
FiniteDimensional.finrank_matrix
(R : Type u)
[Ring R]
[StrongRankCondition R]
(m : Type u_2)
(n : Type u_3)
[Fintype m]
[Fintype n]
:
FiniteDimensional.finrank R (Matrix m n R) = Fintype.card m * Fintype.card n
If m and n are Fintype, the finrank of m × n matrices is
(Fintype.card m) * (Fintype.card n).
@[simp]
theorem
rank_pi
{R : Type u}
{η : Type u₁'}
{φ : η → Type u_1}
[Ring R]
[StrongRankCondition R]
[(i : η) → AddCommGroup (φ i)]
[(i : η) → Module R (φ i)]
[∀ (i : η), Module.Free R (φ i)]
[Finite η]
:
Module.rank R ((i : η) → φ i) = Cardinal.sum fun (i : η) => Module.rank R (φ i)
The rank of a finite product of free modules is the sum of the ranks.
theorem
FiniteDimensional.finrank_pi
(R : Type u)
[Ring R]
[StrongRankCondition R]
{ι : Type v}
[Fintype ι]
:
FiniteDimensional.finrank R (ι → R) = Fintype.card ι
The finrank of (ι → R) is Fintype.card ι.
theorem
FiniteDimensional.finrank_pi_fintype
(R : Type u)
[Ring R]
[StrongRankCondition R]
{ι : Type v}
[Fintype ι]
{M : ι → Type w}
[(i : ι) → AddCommGroup (M i)]
[(i : ι) → Module R (M i)]
[∀ (i : ι), Module.Free R (M i)]
[∀ (i : ι), Module.Finite R (M i)]
:
FiniteDimensional.finrank R ((i : ι) → M i) = Finset.sum Finset.univ fun (i : ι) => FiniteDimensional.finrank R (M i)
The finrank of a finite product is the sum of the finranks.
theorem
rank_fun
{R : Type u}
[Ring R]
[StrongRankCondition R]
{M : Type u}
{η : Type u}
[Fintype η]
[AddCommGroup M]
[Module R M]
[Module.Free R M]
:
Module.rank R (η → M) = ↑(Fintype.card η) * Module.rank R M
theorem
rank_fun_eq_lift_mul
{R : Type u}
{M : Type v}
{η : Type u₁'}
[Ring R]
[AddCommGroup M]
[Module R M]
[StrongRankCondition R]
[Module.Free R M]
[Fintype η]
:
Module.rank R (η → M) = ↑(Fintype.card η) * Cardinal.lift.{u₁', v} (Module.rank R M)
theorem
rank_fun'
{R : Type u}
{η : Type u₁'}
[Ring R]
[StrongRankCondition R]
[Fintype η]
:
Module.rank R (η → R) = ↑(Fintype.card η)
theorem
rank_fin_fun
{R : Type u}
[Ring R]
[StrongRankCondition R]
(n : ℕ)
:
Module.rank R (Fin n → R) = ↑n
@[simp]
theorem
FiniteDimensional.finrank_fintype_fun_eq_card
(R : Type u)
{η : Type u₁'}
[Ring R]
[StrongRankCondition R]
[Fintype η]
:
FiniteDimensional.finrank R (η → R) = Fintype.card η
The vector space of functions on a Fintype ι has finrank equal to the cardinality of ι.
theorem
FiniteDimensional.finrank_fin_fun
(R : Type u)
[Ring R]
[StrongRankCondition R]
{n : ℕ}
:
FiniteDimensional.finrank R (Fin n → R) = n
The vector space of functions on Fin n has finrank equal to n.
def
finDimVectorspaceEquiv
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[StrongRankCondition R]
[Module.Free R M]
(n : ℕ)
(hn : Module.rank R M = ↑n)
:
An n-dimensional R-vector space is equivalent to Fin n → R.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
rank_tensorProduct
{S : Type u}
{M : Type v}
{M' : Type v'}
[CommRing S]
[AddCommGroup M]
[AddCommGroup M']
[StrongRankCondition S]
[Module S M]
[Module.Free S M]
[Module S M']
[Module.Free S M']
:
Module.rank S (TensorProduct S M M') = Cardinal.lift.{v', v} (Module.rank S M) * Cardinal.lift.{v, v'} (Module.rank S M')
The rank of M ⊗[R] M' is (Module.rank R M).lift * (Module.rank R M').lift.
theorem
rank_tensorProduct'
{S : Type u}
{M : Type v}
{M₁ : Type v}
[CommRing S]
[AddCommGroup M]
[AddCommGroup M₁]
[StrongRankCondition S]
[Module S M]
[Module.Free S M]
[Module S M₁]
[Module.Free S M₁]
:
Module.rank S (TensorProduct S M M₁) = Module.rank S M * Module.rank S M₁
If M and M' lie in the same universe, the rank of M ⊗[R] M' is
(Module.rank R M) * (Module.rank R M').
@[simp]
theorem
FiniteDimensional.finrank_tensorProduct
{S : Type u}
{M : Type v}
{M' : Type v'}
[CommRing S]
[AddCommGroup M]
[AddCommGroup M']
[StrongRankCondition S]
[Module S M]
[Module.Free S M]
[Module S M']
[Module.Free S M']
:
FiniteDimensional.finrank S (TensorProduct S M M') = FiniteDimensional.finrank S M * FiniteDimensional.finrank S M'
The finrank of M ⊗[R] M' is (finrank R M) * (finrank R M').
theorem
Submodule.lt_of_le_of_finrank_lt_finrank
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Submodule R M}
{t : Submodule R M}
(le : s ≤ t)
(lt : FiniteDimensional.finrank R ↥s < FiniteDimensional.finrank R ↥t)
:
s < t
theorem
Submodule.lt_top_of_finrank_lt_finrank
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Submodule R M}
(lt : FiniteDimensional.finrank R ↥s < FiniteDimensional.finrank R M)
:
theorem
Submodule.finrank_le
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[StrongRankCondition R]
[Module.Finite R M]
(s : Submodule R M)
:
The dimension of a submodule is bounded by the dimension of the ambient space.
theorem
Submodule.finrank_quotient_le
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[StrongRankCondition R]
[Module.Finite R M]
(s : Submodule R M)
:
FiniteDimensional.finrank R (M ⧸ s) ≤ FiniteDimensional.finrank R M
The dimension of a quotient is bounded by the dimension of the ambient space.
theorem
Submodule.finrank_map_le
{R : Type u}
{M : Type v}
{M' : Type v'}
[Ring R]
[AddCommGroup M]
[AddCommGroup M']
[Module R M]
[Module R M']
[StrongRankCondition R]
(f : M →ₗ[R] M')
(p : Submodule R M)
[Module.Finite R ↥p]
:
FiniteDimensional.finrank R ↥(Submodule.map f p) ≤ FiniteDimensional.finrank R ↥p
Pushforwards of finite submodules have a smaller finrank.
theorem
Submodule.finrank_le_finrank_of_le
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[StrongRankCondition R]
{s : Submodule R M}
{t : Submodule R M}
[Module.Finite R ↥t]
(hst : s ≤ t)
:
theorem
rank_span_le
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[StrongRankCondition R]
(s : Set M)
:
Module.rank R ↥(Submodule.span R s) ≤ Cardinal.mk ↑s
theorem
rank_span_finset_le
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[StrongRankCondition R]
(s : Finset M)
:
Module.rank R ↥(Submodule.span R ↑s) ≤ ↑s.card
theorem
rank_span_of_finset
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[StrongRankCondition R]
(s : Finset M)
:
Module.rank R ↥(Submodule.span R ↑s) < Cardinal.aleph0
noncomputable def
Set.finrank
(R : Type u)
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
(s : Set M)
:
The rank of a set of vectors as a natural number.
Equations
- Set.finrank R s = FiniteDimensional.finrank R ↥(Submodule.span R s)
Instances For
theorem
finrank_span_le_card
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[StrongRankCondition R]
(s : Set M)
[Fintype ↑s]
:
FiniteDimensional.finrank R ↥(Submodule.span R s) ≤ (Set.toFinset s).card
theorem
finrank_span_finset_le_card
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[StrongRankCondition R]
(s : Finset M)
:
Set.finrank R ↑s ≤ s.card
theorem
finrank_range_le_card
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[StrongRankCondition R]
{ι : Type u_2}
[Fintype ι]
(b : ι → M)
:
Set.finrank R (Set.range b) ≤ Fintype.card ι
theorem
finrank_span_eq_card
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[StrongRankCondition R]
[Nontrivial R]
{ι : Type u_2}
[Fintype ι]
{b : ι → M}
(hb : LinearIndependent R b)
:
FiniteDimensional.finrank R ↥(Submodule.span R (Set.range b)) = Fintype.card ι
theorem
finrank_span_set_eq_card
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[StrongRankCondition R]
{s : Set M}
[Fintype ↑s]
(hs : LinearIndependent (ι := { x : M // x ∈ s }) R Subtype.val)
:
FiniteDimensional.finrank R ↥(Submodule.span R s) = (Set.toFinset s).card
theorem
finrank_span_finset_eq_card
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[StrongRankCondition R]
{s : Finset M}
(hs : LinearIndependent R Subtype.val)
:
FiniteDimensional.finrank R ↥(Submodule.span R ↑s) = s.card
theorem
span_lt_of_subset_of_card_lt_finrank
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[StrongRankCondition R]
{s : Set M}
[Fintype ↑s]
{t : Submodule R M}
(subset : s ⊆ ↑t)
(card_lt : (Set.toFinset s).card < FiniteDimensional.finrank R ↥t)
:
Submodule.span R s < t
theorem
span_lt_top_of_card_lt_finrank
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[StrongRankCondition R]
{s : Set M}
[Fintype ↑s]
(card_lt : (Set.toFinset s).card < FiniteDimensional.finrank R M)
:
Submodule.span R s < ⊤
@[simp]
theorem
Subalgebra.rank_toSubmodule
{F : Type u_2}
{E : Type u_3}
[CommRing F]
[Ring E]
[Algebra F E]
(S : Subalgebra F E)
:
Module.rank F ↥(Subalgebra.toSubmodule S) = Module.rank F ↥S
@[simp]
theorem
Subalgebra.finrank_toSubmodule
{F : Type u_2}
{E : Type u_3}
[CommRing F]
[Ring E]
[Algebra F E]
(S : Subalgebra F E)
:
FiniteDimensional.finrank F ↥(Subalgebra.toSubmodule S) = FiniteDimensional.finrank F ↥S
theorem
subalgebra_top_rank_eq_submodule_top_rank
{F : Type u_2}
{E : Type u_3}
[CommRing F]
[Ring E]
[Algebra F E]
:
Module.rank F ↥⊤ = Module.rank F ↥⊤
theorem
Subalgebra.rank_top
{F : Type u_2}
{E : Type u_3}
[CommRing F]
[Ring E]
[Algebra F E]
:
Module.rank F ↥⊤ = Module.rank F E
@[simp]
theorem
Subalgebra.rank_bot
{F : Type u_2}
{E : Type u_3}
[CommRing F]
[Ring E]
[Algebra F E]
[StrongRankCondition F]
[NoZeroSMulDivisors F E]
[Nontrivial E]
:
Module.rank F ↥⊥ = 1
@[simp]
theorem
Subalgebra.finrank_bot
{F : Type u_2}
{E : Type u_3}
[CommRing F]
[Ring E]
[Algebra F E]
[StrongRankCondition F]
[NoZeroSMulDivisors F E]
[Nontrivial E]
:
FiniteDimensional.finrank F ↥⊥ = 1