linear_algebra.free_module.finite.rank

@[simp]

theorem finite_dimensional.submodule.finrank_map_subtype_eq (R : Type u) (M : Type v) [ring R] [add_comm_group M] [module R M] (p : submodule R M) (q : submodule R ↥p) :

finite_dimensional.finrank R ↥(submodule.map p.subtype q) = finite_dimensional.finrank R ↥q

source

theorem finite_dimensional.rank_lt_aleph_0 (R : Type u) (M : Type v) [ring R] [strong_rank_condition R] [add_comm_group M] [module R M] [module.finite R M] :

module.rank R M < cardinal.aleph_0

The rank of a finite module is finite.

source

@[simp]

theorem finite_dimensional.finrank_eq_rank (R : Type u) (M : Type v) [ring R] [strong_rank_condition R] [add_comm_group M] [module R M] [module.finite R M] :

↑(finite_dimensional.finrank R M) = module.rank R M

If M is finite, finrank M = rank M.

source

theorem finite_dimensional.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] :

finite_dimensional.finrank R M = fintype.card (module.free.choose_basis_index R M)

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

source

@[simp]

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

source

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

source

@[simp]

theorem finite_dimensional.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 (direct_sum ι (λ (i : ι), M i)) = finset.univ.sum (λ (i : ι), finite_dimensional.finrank R (M i))

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

source

@[simp]

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

source

theorem finite_dimensional.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) = finset.univ.sum (λ (i : ι), finite_dimensional.finrank R (M i))

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

source

theorem finite_dimensional.finrank_matrix (R : Type u) [ring R] [strong_rank_condition R] (m : Type u_1) (n : Type u_2) [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).

source

theorem finite_dimensional.nonempty_linear_equiv_of_finrank_eq {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] (cond : finite_dimensional.finrank R M = finite_dimensional.finrank R N) :

nonempty (M ≃ₗ[R] N)

Two finite and free modules are isomorphic if they have the same (finite) rank.

source

theorem finite_dimensional.nonempty_linear_equiv_iff_finrank_eq {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] :

nonempty (M ≃ₗ[R] N) ↔ finite_dimensional.finrank R M = finite_dimensional.finrank R N

Two finite and free modules are isomorphic if and only if they have the same (finite) rank.

source

noncomputable def linear_equiv.of_finrank_eq {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] (cond : finite_dimensional.finrank R M = finite_dimensional.finrank R N) :

M ≃ₗ[R] N

Two finite and free modules are isomorphic if they have the same (finite) rank.

Equations

linear_equiv.of_finrank_eq M N cond = classical.choice _

source

@[simp]

theorem finite_dimensional.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 (tensor_product 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).

source

theorem linear_map.finrank_le_finrank_of_injective {R : Type u} {M : Type v} {N : Type w} [ring R] [strong_rank_condition R] [add_comm_group M] [module R M] [add_comm_group N] [module R N] [module.finite R N] {f : M →ₗ[R] N} (hf : function.injective ⇑f) :

finite_dimensional.finrank R M ≤ finite_dimensional.finrank R N

source

theorem linear_map.finrank_range_le {R : Type u} {M : Type v} {N : Type w} [ring R] [strong_rank_condition R] [add_comm_group M] [module R M] [add_comm_group N] [module R N] [module.finite R M] (f : M →ₗ[R] N) :

finite_dimensional.finrank R ↥(linear_map.range f) ≤ finite_dimensional.finrank R M

source

theorem submodule.finrank_le {R : Type u} {M : Type v} [ring R] [strong_rank_condition R] [add_comm_group M] [module R M] [module.finite R M] (s : submodule R M) :

finite_dimensional.finrank R ↥s ≤ finite_dimensional.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] [strong_rank_condition R] [add_comm_group M] [module R M] [module.finite R M] (s : submodule R M) :

finite_dimensional.finrank R (M ⧸ s) ≤ finite_dimensional.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} {N : Type w} [ring R] [strong_rank_condition R] [add_comm_group M] [module R M] [add_comm_group N] [module R N] (f : M →ₗ[R] N) (p : submodule R M) [module.finite R ↥p] :

finite_dimensional.finrank R ↥(submodule.map f p) ≤ finite_dimensional.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] [strong_rank_condition R] [add_comm_group M] [module R M] {s t : submodule R M} [module.finite R ↥t] (hst : s ≤ t) :

finite_dimensional.finrank R ↥s ≤ finite_dimensional.finrank R ↥t

mathlib3 documentation

Rank of finite free modules #