Rank of finite free modules #
This is a basic API for the rank of finite free modules.
theorem
module.free.rank_lt_omega
(R : Type u)
(M : Type v)
[ring R]
[strong_rank_condition R]
[add_comm_group M]
[module R M]
[module.free R M]
[module.finite R M] :
module.rank R M < ω
The rank of a finite and free module is finite.
@[simp]
theorem
module.free.finrank_eq_rank
(R : Type u)
(M : Type v)
[ring R]
[strong_rank_condition R]
[add_comm_group M]
[module R M]
[module.free R M]
[module.finite R M] :
↑(finite_dimensional.finrank R M) = module.rank R M
If M is finite and free, finrank M = rank M.
theorem
module.free.finrank_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.finite R M] :
The finrank of a free module M over R is the cardinality of choose_basis_index R M.
@[simp]
theorem
module.free.finrank_finsupp
(R : Type u)
[ring R]
[strong_rank_condition R]
{ι : Type v}
[fintype ι] :
finite_dimensional.finrank R (ι →₀ R) = fintype.card ι
The finrank of (ι →₀ R) is fintype.card ι.
theorem
module.free.finrank_pi
(R : Type u)
[ring R]
[strong_rank_condition R]
{ι : Type v}
[fintype ι] :
finite_dimensional.finrank R (ι → R) = fintype.card ι
The finrank of (ι → R) is fintype.card ι.
@[simp]
theorem
module.free.finrank_direct_sum
(R : Type u)
[ring R]
[strong_rank_condition R]
{ι : Type v}
[fintype ι]
(M : ι → Type w)
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), module R (M i)]
[∀ (i : ι), module.free R (M i)]
[∀ (i : ι), module.finite R (M i)] :
finite_dimensional.finrank R (⨁ (i : ι), M i) = ∑ (i : ι), finite_dimensional.finrank R (M i)
The finrank of the direct sum is the sum of the finranks.
@[simp]
theorem
module.free.finrank_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]
[module.finite R M]
[add_comm_group N]
[module R N]
[module.free R N]
[module.finite R N] :
finite_dimensional.finrank R (M × N) = finite_dimensional.finrank R M + finite_dimensional.finrank R N
The finrank of M × N is (finrank R M) + (finrank R N).
theorem
module.free.finrank_pi_fintype
(R : Type u)
[ring R]
[strong_rank_condition R]
{ι : Type v}
[fintype ι]
{M : ι → Type w}
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), module R (M i)]
[∀ (i : ι), module.free R (M i)]
[∀ (i : ι), module.finite R (M i)] :
finite_dimensional.finrank R (Π (i : ι), M i) = ∑ (i : ι), finite_dimensional.finrank R (M i)
The finrank of a finite product is the sum of the finranks.
theorem
module.free.finrank_matrix
(R : Type u)
[ring R]
[strong_rank_condition R]
(m n : Type v)
[fintype m]
[fintype n] :
finite_dimensional.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).
theorem
module.free.finrank_linear_hom
(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]
[module.finite R M]
[add_comm_group N]
[module R N]
[module.free R N]
[module.finite R N] :
finite_dimensional.finrank R (M →ₗ[R] N) = (finite_dimensional.finrank R M) * finite_dimensional.finrank R N
The finrank of M →ₗ[R] N is (finrank R M) * (finrank R N).
@[simp]
theorem
module.free.finrank_tensor_product
(R : Type u)
[comm_ring R]
[strong_rank_condition R]
(M : Type v)
(N : Type w)
[add_comm_group M]
[module R M]
[module.free R M]
[add_comm_group N]
[module R N]
[module.free R N] :
finite_dimensional.finrank R (M ⊗ N) = (finite_dimensional.finrank R M) * finite_dimensional.finrank R N
The finrank of M ⊗[R] N is (finrank R M) * (finrank R N).