# 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) ≤ #s for finite s.

• rank_prod : rank M × N = rank M + rank N.
• rank_finsupp : rank (ι →₀ M) = #ι * rank M
• rank_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 LinearIndependent.sum_elim_of_quotient {R : Type u} {M : Type v} [Ring R] [] [Module R M] {M' : } {ι₁ : Type u_2} {ι₂ : Type u_3} {f : ι₁M'} (hf : ) (g : ι₂M) (hg : LinearIndependent R (Submodule.Quotient.mk g)) :
LinearIndependent R (Sum.elim (fun (x : ι₁) => (f x)) g)
theorem LinearIndependent.union_of_quotient {R : Type u} {M : Type v} [Ring R] [] [Module R M] {M' : } {s : Set M} (hs : s M') (hs' : LinearIndependent (ι := s) R Subtype.val) {t : Set M} (ht : LinearIndependent (ι := t) R (Submodule.Quotient.mk Subtype.val)) :
LinearIndependent (ι := (s t)) R Subtype.val
theorem rank_quotient_add_rank_le {R : Type u} {M : Type v} [Ring R] [] [Module R M] [] (M' : ) :
Module.rank R (M M') + Module.rank R M'
theorem rank_quotient_le {R : Type u} {M : Type v} [Ring R] [] [Module R M] (p : ) :
theorem rank_quotient_eq_of_le_torsion {R : Type u_2} {M : Type u_3} [] [] [Module R M] {M' : } (hN : M' ) :
Module.rank R (M M') =
@[simp]
theorem rank_ulift {R : Type u} {M : Type v} [Ring R] [] [Module R M] :
@[simp]
theorem finrank_ulift {R : Type u} {M : Type v} [Ring R] [] [Module R M] :
theorem lift_rank_add_lift_rank_le_rank_prod (R : Type u) (M : Type v) (M' : Type v') [Ring R] [] [] [Module R M] [Module 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] [] [] [Module R M] [Module 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] [] [] [Module R M] [Module R M'] [] [Module.Free R M'] :
Module.rank R (M × 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] [] [] [Module R M] [Module R M₁] [] [Module.Free R M₁] :
Module.rank R (M × 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] [] [] [Module R M] [Module R M'] [] [Module.Free 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] [] [Module R M] [] (ι : Type w) :
Module.rank R (ι →₀ M) = *
theorem rank_finsupp' (R : Type u) (M : Type v) [Ring R] [] [Module R M] [] (ι : Type v) :
Module.rank R (ι →₀ M) = *
theorem rank_finsupp_self (R : Type u) [Ring R] (ι : Type w) :
Module.rank R (ι →₀ R) =

The rank of (ι →₀ R) is (#ι).lift.

theorem rank_finsupp_self' (R : Type u) [Ring R] {ι : Type u} :
Module.rank R (ι →₀ R) =

If R and ι lie in the same universe, the rank of (ι →₀ R) is # ι.

@[simp]
theorem rank_directSum (R : Type u) [Ring 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] (m : Type v) (n : Type w) [] [] :
Module.rank R (Matrix m n R) = *

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] (m : Type v) (n : Type v) [] [] :
Module.rank R (Matrix m n R) =

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] (m : Type u) (n : Type u) [] [] :
Module.rank R (Matrix m n R) =

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] [] [Module R M] [] {ι : Type v} [] :
@[simp]

The finrank of (ι →₀ R) is Fintype.card ι.

@[simp]
theorem FiniteDimensional.finrank_directSum (R : Type u) [Ring R] {ι : Type v} [] (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) = i : ι,

The finrank of the direct sum is the sum of the finranks.

theorem FiniteDimensional.finrank_matrix (R : Type u) [Ring R] (m : Type u_2) (n : Type u_3) [] [] :

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] [(i : η) → AddCommGroup (φ i)] [(i : η) → Module R (φ i)] [∀ (i : η), Module.Free R (φ i)] [] :
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] {ι : Type v} [] :

The finrank of (ι → R) is Fintype.card ι.

theorem FiniteDimensional.finrank_pi_fintype (R : Type u) [Ring R] {ι : Type v} [] {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) = i : ι,

The finrank of a finite product is the sum of the finranks.

theorem rank_fun {R : Type u} [Ring R] {M : Type u} {η : Type u} [] [] [Module R M] [] :
Module.rank R (ηM) = () *
theorem rank_fun_eq_lift_mul {R : Type u} {M : Type v} {η : Type u₁'} [Ring R] [] [Module R M] [] [] :
Module.rank R (ηM) = () *
theorem rank_fun' {R : Type u} {η : Type u₁'} [Ring R] [] :
Module.rank R (ηR) = ()
theorem rank_fin_fun {R : Type u} [Ring R] (n : ) :
Module.rank R (Fin nR) = n
@[simp]
theorem FiniteDimensional.finrank_fintype_fun_eq_card (R : Type u) {η : Type u₁'} [Ring R] [] :

The vector space of functions on a Fintype ι has finrank equal to the cardinality of ι.

The vector space of functions on Fin n has finrank equal to n.

def finDimVectorspaceEquiv {R : Type u} {M : Type v} [Ring R] [] [Module R M] [] (n : ) (hn : = n) :
M ≃ₗ[R] Fin nR

An n-dimensional R-vector space is equivalent to Fin n → R.

Equations
• = let_fun this := ; let_fun hn := ;
Instances For
@[simp]
theorem rank_tensorProduct {R : Type u} {S : Type u} {M : Type v} {M' : Type v'} [Ring R] [] [] [] [Module S M] [Module S M'] [Module.Free S M'] [Algebra S R] [Module R M] [] [] :

The S-rank of M ⊗[R] M' is (Module.rank S M).lift * (Module.rank R M').lift.

theorem rank_tensorProduct' {R : Type u} {S : Type u} {M : Type v} {M₁ : Type v} [Ring R] [] [] [] [Module S M] [Module S M₁] [Module.Free S M₁] [Algebra S R] [Module R M] [] [] :

If M and M' lie in the same universe, the S-rank of M ⊗[R] M' is (Module.rank S M) * (Module.rank R M').

@[simp]
theorem FiniteDimensional.finrank_tensorProduct {R : Type u} {S : Type u} {M : Type v} {M' : Type v'} [Ring R] [] [] [] [Module S M] [Module S M'] [Module.Free S M'] [Algebra S R] [Module R M] [] [] :

The S-finrank of M ⊗[R] M' is (finrank S M) * (finrank R M').

theorem Submodule.lt_of_le_of_finrank_lt_finrank {R : Type u} {M : Type v} [Ring R] [] [Module R M] {s : } {t : } (le : s t) (lt : ) :
s < t
theorem Submodule.lt_top_of_finrank_lt_finrank {R : Type u} {M : Type v} [Ring R] [] [Module R M] {s : } (lt : ) :
s <
theorem Submodule.finrank_le {R : Type u} {M : Type v} [Ring R] [] [Module R M] [] (s : ) :

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] [] [Module R M] [] (s : ) :

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] [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') (p : ) [] :

Pushforwards of finite submodules have a smaller finrank.

theorem Submodule.finrank_le_finrank_of_le {R : Type u} {M : Type v} [Ring R] [] [Module R M] {s : } {t : } [] (hst : s t) :
theorem rank_span_le {R : Type u} {M : Type v} [Ring R] [] [Module R M] (s : Set M) :
Module.rank R ()
theorem rank_span_finset_le {R : Type u} {M : Type v} [Ring R] [] [Module R M] (s : ) :
Module.rank R () s.card
theorem rank_span_of_finset {R : Type u} {M : Type v} [Ring R] [] [Module R M] (s : ) :
noncomputable def Set.finrank (R : Type u) {M : Type v} [Ring R] [] [Module R M] (s : Set M) :

The rank of a set of vectors as a natural number.

Equations
Instances For
theorem finrank_span_le_card {R : Type u} {M : Type v} [Ring R] [] [Module R M] (s : Set M) [Fintype s] :
s.toFinset.card
theorem finrank_span_finset_le_card {R : Type u} {M : Type v} [Ring R] [] [Module R M] (s : ) :
Set.finrank R s s.card
theorem finrank_range_le_card {R : Type u} {M : Type v} [Ring R] [] [Module R M] {ι : Type u_2} [] (b : ιM) :
theorem finrank_span_eq_card {R : Type u} {M : Type v} [Ring R] [] [Module R M] [] {ι : Type u_2} [] {b : ιM} (hb : ) :
theorem finrank_span_set_eq_card {R : Type u} {M : Type v} [Ring R] [] [Module R M] {s : Set M} [Fintype s] (hs : LinearIndependent (ι := { x : M // x s }) R Subtype.val) :
= s.toFinset.card
theorem finrank_span_finset_eq_card {R : Type u} {M : Type v} [Ring R] [] [Module R M] {s : } (hs : LinearIndependent R Subtype.val) :
= s.card
theorem span_lt_of_subset_of_card_lt_finrank {R : Type u} {M : Type v} [Ring R] [] [Module R M] {s : Set M} [Fintype s] {t : } (subset : s t) (card_lt : s.toFinset.card < ) :
< t
theorem span_lt_top_of_card_lt_finrank {R : Type u} {M : Type v} [Ring R] [] [Module R M] {s : Set M} [Fintype s] (card_lt : s.toFinset.card < ) :
@[simp]
theorem Subalgebra.rank_toSubmodule {F : Type u_2} {E : Type u_3} [] [Ring E] [Algebra F E] (S : ) :
Module.rank F (Subalgebra.toSubmodule S) = Module.rank F S
@[simp]
theorem Subalgebra.finrank_toSubmodule {F : Type u_2} {E : Type u_3} [] [Ring E] [Algebra F E] (S : ) :
FiniteDimensional.finrank F (Subalgebra.toSubmodule S) =
theorem subalgebra_top_rank_eq_submodule_top_rank {F : Type u_2} {E : Type u_3} [] [Ring E] [Algebra F E] :
=
theorem Subalgebra.rank_top {F : Type u_2} {E : Type u_3} [] [Ring E] [Algebra F E] :
=
@[simp]
theorem Subalgebra.rank_bot {F : Type u_2} {E : Type u_3} [] [Ring E] [Algebra F E] [] [] :
= 1
@[simp]
theorem Subalgebra.finrank_bot {F : Type u_2} {E : Type u_3} [] [Ring E] [Algebra F E] [] [] :