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.

For free modules, we have

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] [AddCommGroup M] [Module R M] {M' : Submodule R M} {ι₁ : Type u_2} {ι₂ : Type u_3} {f : ι₁ → ↥M'} (hf : LinearIndependent R f) (g : ι₂ → M) (hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)) :

LinearIndependent R (Sum.elim (fun (x : ι₁) => ↑(f x)) g)

source

theorem LinearIndependent.union_of_quotient {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {M' : Submodule R 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

source

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

source

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

source

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

source

@[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)

source

@[simp]

theorem finrank_ulift {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] :

FiniteDimensional.finrank R (ULift.{u_2, v} M) = FiniteDimensional.finrank R M

source

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')

source

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₁)

source

@[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.

source

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').

source

@[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').

source

@[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)

source

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

source

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.

source

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 # ι.

source

@[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.

source

@[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.

source

@[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.

source

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.

source

@[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

source

@[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 ι.

source

@[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) = ∑ i : ι, FiniteDimensional.finrank R (M i)

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

source

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).

source

@[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.

source

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 ι.

source

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) = ∑ i : ι, FiniteDimensional.finrank R (M i)

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

source

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

source

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)

source

theorem rank_fun' {R : Type u} {η : Type u₁'} [Ring R] [StrongRankCondition R] [Fintype η] :

Module.rank R (η → R) = ↑(Fintype.card η)

source

theorem rank_fin_fun {R : Type u} [Ring R] [StrongRankCondition R] (n : ℕ) :

Module.rank R (Fin n → R) = ↑n

source

@[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 ι.

source

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.

source

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) :

M ≃ₗ[R] Fin n → R

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

Equations

finDimVectorspaceEquiv n hn = let_fun this := ⋯; let_fun hn := ⋯; Classical.choice ⋯

Instances For

source

@[simp]

theorem rank_tensorProduct {R : Type u} {S : Type u} {M : Type v} {M' : Type v'} [Ring R] [CommRing S] [AddCommGroup M] [AddCommGroup M'] [StrongRankCondition R] [StrongRankCondition S] [Module S M] [Module S M'] [Module.Free S M'] [Algebra S R] [Module R M] [IsScalarTower S R M] [Module.Free R M] :

Module.rank R (TensorProduct S M M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')

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

source

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

Module.rank R (TensorProduct S M M₁) = Module.rank R M * Module.rank S 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').

source

@[simp]

theorem FiniteDimensional.finrank_tensorProduct {R : Type u} {S : Type u} {M : Type v} {M' : Type v'} [Ring R] [CommRing S] [AddCommGroup M] [AddCommGroup M'] [StrongRankCondition R] [StrongRankCondition S] [Module S M] [Module S M'] [Module.Free S M'] [Algebra S R] [Module R M] [IsScalarTower S R M] [Module.Free R M] :

FiniteDimensional.finrank R (TensorProduct S M M') = FiniteDimensional.finrank R M * FiniteDimensional.finrank S M'

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

source

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

source

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) :

s < ⊤

source

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) :

FiniteDimensional.finrank R ↥s ≤ FiniteDimensional.finrank R M

The dimension of a submodule is bounded by the dimension of the ambient space.

source

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.

source

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.

source

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) :

FiniteDimensional.finrank R ↥s ≤ FiniteDimensional.finrank R ↥t

source

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

source

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

source

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

source

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

source

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) ≤ s.toFinset.card

source

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

source

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 ι

source

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 ι

source

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) = s.toFinset.card

source

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

source

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 : s.toFinset.card < FiniteDimensional.finrank R ↥t) :

Submodule.span R s < t

source

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 : s.toFinset.card < FiniteDimensional.finrank R M) :

Submodule.span R s < ⊤

source

@[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

source

@[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

source

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 ↥⊤

source

theorem subalgebra_top_finrank_eq_submodule_top_finrank {F : Type u_2} {E : Type u_3} [CommRing F] [Ring E] [Algebra F E] :

FiniteDimensional.finrank F ↥⊤ = FiniteDimensional.finrank F ↥⊤

source

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

source

@[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

source

@[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

Documentation

Mathlib.LinearAlgebra.Dimension.Constructions

Rank of various constructions #

Main statements #