mathlib documentation

linear_algebra.free_module.rank

Rank of free modules #

This is a basic API for the rank of free modules.

source
theorem module.free.rank_eq_card_choose_basis_index (R : Type u) (M : Type v) [ring R] [strong_rank_condition R] [add_comm_group M] [module R M] [module.free R M] :
module.rank R M = cardinal.mk (module.free.choose_basis_index R M)

The rank of a free module M over R is the cardinality of choose_basis_index R M.

source
@[simp]
theorem module.free.rank_finsupp (R : Type u) [ring R] [strong_rank_condition R] {ι : Type v} :
module.rank R (ι →₀ R) = (cardinal.mk ι).lift

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

source
theorem module.free.rank_finsupp' (R : Type u) [ring R] [strong_rank_condition 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 module.free.rank_prod (R : Type u) (M : Type v) (N : Type w) [ring R] [strong_rank_condition R] [add_comm_group M] [module R M] [module.free R M] [add_comm_group N] [module R N] [module.free R N] :
module.rank R (M × N) = (module.rank R M).lift + (module.rank R N).lift

The rank of M × N is (module.rank R M).lift + (module.rank R N).lift.

source
theorem module.free.rank_prod' (R : Type u) (M : Type v) [ring R] [strong_rank_condition R] [add_comm_group M] [module R M] [module.free R M] (N : Type v) [add_comm_group N] [module R N] [module.free R N] :
module.rank R (M × N) = module.rank R M + module.rank R N

If M and N lie in the same universe, the rank of M × N is (module.rank R M) + (module.rank R N).

source
@[simp]
theorem module.free.rank_direct_sum (R : Type u) [ring R] [strong_rank_condition R] {ι : Type v} (M : ι → Type w) [Π (i : ι), add_comm_group (M i)] [Π (i : ι), module R (M i)] [∀ (i : ι), module.free R (M i)] :
module.rank R (direct_sum ι (λ (i : ι), M i)) = cardinal.sum (λ (i : ι), module.rank R (M i))

The rank of the direct sum is the sum of the ranks.

source
@[simp]
theorem module.free.rank_pi_finite (R : Type u) [ring R] [strong_rank_condition R] {ι : Type v} [finite ι] {M : ι → Type w} [Π (i : ι), add_comm_group (M i)] [Π (i : ι), module R (M i)] [∀ (i : ι), module.free R (M i)] :
module.rank R (Π (i : ι), M i) = cardinal.sum (λ (i : ι), module.rank R (M i))

The rank of a finite product is the sum of the ranks.

source
@[simp]
theorem module.free.rank_matrix (R : Type u) [ring R] [strong_rank_condition R] (m : Type v) (n : Type w) [finite m] [finite n] :
module.rank R (matrix m n R) = (cardinal.mk m).lift * (cardinal.mk n).lift

If m and n are fintype, the rank of m × n matrices is (# m).lift * (# n).lift.

source
@[simp]
theorem module.free.rank_matrix' (R : Type u) [ring R] [strong_rank_condition R] (m n : Type v) [finite m] [finite n] :
module.rank R (matrix m n R) = (cardinal.mk m * cardinal.mk n).lift

If m and n are fintype that lie in the same universe, the rank of m × n matrices is (# n * # m).lift.

source
@[simp]
theorem module.free.rank_matrix'' (R : Type u) [ring R] [strong_rank_condition R] (m 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 module.free.rank_tensor_product (R : Type u) (M : Type v) (N : Type w) [comm_ring R] [strong_rank_condition R] [add_comm_group M] [module R M] [module.free R M] [add_comm_group N] [module R N] [module.free R N] :
module.rank R (tensor_product R M N) = (module.rank R M).lift * (module.rank R N).lift

The rank of M ⊗[R] N is (module.rank R M).lift * (module.rank R N).lift.

source
theorem module.free.rank_tensor_product' (R : Type u) (M : Type v) [comm_ring R] [strong_rank_condition R] [add_comm_group M] [module R M] [module.free R M] (N : Type v) [add_comm_group N] [module R N] [module.free R N] :
module.rank R (tensor_product R M N) = module.rank R M * module.rank R N

If M and N lie in the same universe, the rank of M ⊗[R] N is (module.rank R M) * (module.rank R N).