FiniteDimensional.finrank_le_finrank_of_rank_le_rank
theorem FiniteDimensional.finrank_le_finrank_of_rank_le_rank :
∀ {R : Type u} {M : Type v} {N : Type w} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : AddCommGroup N] [inst_4 : Module R N],
Cardinal.lift.{w, v} (Module.rank R M) ≤ Cardinal.lift.{v, w} (Module.rank R N) →
Module.rank R N < Cardinal.aleph0 → FiniteDimensional.finrank R M ≤ FiniteDimensional.finrank R N
The theorem states that for any ring `R` and two modules `M` and `N` over this ring, if the rank of the module `M` is less than or equal to the rank of the module `N` when considering their cardinalities in possibly different universes, and if the rank of module `N` is less than the cardinality of the smallest infinite cardinal (ℵ₀), then the finite rank of `M` is less than or equal to the finite rank of `N`. The finite rank of a module is defined to be the cardinality of the module's rank converted to a natural number and is conventionally set to `0` if the module has infinite rank.
More concisely: If `R` is a ring, `M` and `N` are `R`-modules with finite ranks, and the rank of `M` is less than or equal to the rank of `N` when considering their cardinalities in possibly different universes, and the rank of `N` is less than the smallest infinite cardinal, then the finite rank of `M` is less than or equal to the finite rank of `N`.
|
FiniteDimensional.rank_eq_ofNat_iff_finrank_eq_ofNat
theorem FiniteDimensional.rank_eq_ofNat_iff_finrank_eq_ofNat :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (n : ℕ)
[inst_3 : n.AtLeastTwo], Module.rank R M = OfNat.ofNat n ↔ FiniteDimensional.finrank R M = OfNat.ofNat n
This theorem, named `FiniteDimensional.rank_eq_ofNat_iff_finrank_eq_ofNat`, states that for any ring `R`, any additive commutative group `M`, and any natural number `n` that is at least two, the rank of the module `M` over the ring `R` being equal to `n` is equivalent to the finite rank (or dimension) of `M` over `R` being equal to `n`. In other words, in a mathematical context, it means that the rank and the finite dimensionality of a module (or vector space) over a ring (or field) are the same when the rank or dimension is at least two.
More concisely: For any additive commutative group `M` over a ring `R` and natural number `n` ≥ 2, the rank and finite dimensionality of `M` over `R` are equal if and only if they both equal `n`.
|
FiniteDimensional.finrank_eq_of_rank_eq
theorem FiniteDimensional.finrank_eq_of_rank_eq :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {n : ℕ},
Module.rank R M = ↑n → FiniteDimensional.finrank R M = n
This theorem states that for any ring `R` and any additively commutative group `M`, if `M` is also a module over `R` and the rank of `M` as a module over `R` equals `n` (where `n` is a natural number), then the finite dimension (or rank) of `M` as a module over `R` is also `n`. In other words, when the rank of the module `M` over the ring `R` is a finite natural number `n`, the rank and the finite dimension of the module coincide.
More concisely: For any ring `R` and additively commutative group `M` that is an `R`-module with finite rank `n`, the rank and finite dimension of `M` as an `R`-module are equal.
|
FiniteDimensional.lt_rank_of_lt_finrank
theorem FiniteDimensional.lt_rank_of_lt_finrank :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {n : ℕ},
n < FiniteDimensional.finrank R M → ↑n < Module.rank R M
This theorem states that for any ring `R`, additive commutative group `M`, and module `M` over `R`, if a natural number `n` is less than the finite rank of the module `M` over `R` (denoted by `FiniteDimensional.finrank R M`), then the cardinality of `n` (denoted by `↑n`) is less than the rank of the module `M` over `R` (denoted by `Module.rank R M`). In more mathematical terms, for any module over a ring, if a natural number is less than the finite dimension of the module, then its cardinality is also less than the rank of the module.
More concisely: For any ring `R`, additive commutative group `M` being an `R`-module, and natural number `n` with `n < FiniteDimensional.finrank R M`, we have `↑n < Module.rank R M`.
|
LinearEquiv.finrank_eq
theorem LinearEquiv.finrank_eq :
∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₂]
[inst_3 : Module R M] [inst_4 : Module R M₂],
(M ≃ₗ[R] M₂) → FiniteDimensional.finrank R M = FiniteDimensional.finrank R M₂
The theorem `LinearEquiv.finrank_eq` states that the dimension of a finite dimensional space is preserved under linear equivalence. More specifically, for any ring `R` and any two `R`-modules `M` and `M₂`, if there exists a linear equivalence (an invertible linear transformation) from `M` to `M₂`, then the finite rank (or dimension, in the case of vector spaces) of `M` is equal to the finite rank of `M₂`. This is a fundamental result in linear algebra, stating essentially that the dimension of a vector space (or more generally, a module) is an invariant under isomorphism.
More concisely: If two finite-dimensional modules over a ring are linearly equivalent, then they have equal dimensions.
|
LinearEquiv.finrank_map_eq
theorem LinearEquiv.finrank_map_eq :
∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₂]
[inst_3 : Module R M] [inst_4 : Module R M₂] (f : M ≃ₗ[R] M₂) (p : Submodule R M),
FiniteDimensional.finrank R ↥(Submodule.map (↑f) p) = FiniteDimensional.finrank R ↥p
The theorem `LinearEquiv.finrank_map_eq` states that for any Ring `R`, and additive commutative groups `M` and `M₂` that are modules over `R`, if we have a linear equivalence `f` between `M` and `M₂`, and a submodule `p` of `M`, then the rank of the submodule obtained by mapping `p` through `f` is the same as the rank of `p` itself. In other words, under a linear equivalence, the rank of a submodule remains the same. This is aligned with the intuition from linear algebra: a basis of a subspace gets mapped to a basis of the image subspace under a linear map, thereby preserving dimensionality (or rank in this context).
More concisely: For any Ring `R`, additive commutative groups `M` and `M₂` as `R`-modules, and a linear equivalence `f : M ≃ M₂`, if `p` is a submodule of `M`, then the rank of `f''p` (the image of `p` under `f`) equals the rank of `p`.
|
finrank_top
theorem finrank_top :
∀ (R : Type u) (M : Type v) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
FiniteDimensional.finrank R ↥⊤ = FiniteDimensional.finrank R M
This theorem, named `finrank_top`, states that for any ring `R` and any additively commutative group `M` that is also an `R`-module, the finite rank of the top submodule (denoted by `⊤`) is equal to the finite rank of the module `M` itself. In other words, the rank of the entire space is the same as the rank of the module. This essentially says that the dimension of the total module space and the module itself are the same, which is a fundamental property of vector spaces in linear algebra.
More concisely: For any additively commutative group `M` that is an `R`-module and has finite rank, the rank of the top submodule `⊤` equals the rank of `M`.
|
LinearMap.finrank_range_of_inj
theorem LinearMap.finrank_range_of_inj :
∀ {R : Type u} {M : Type v} {N : Type w} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N},
Function.Injective ⇑f → FiniteDimensional.finrank R ↥(LinearMap.range f) = FiniteDimensional.finrank R M
The theorem `LinearMap.finrank_range_of_inj` states that for any ring `R`, two modules `M` and `N` over `R`, and any linear map `f` from `M` to `N`, if `f` is injective (i.e., distinct elements in `M` map to distinct elements in `N`), then the dimension (as a natural number) of the range of `f` is equal to the dimension of `M`. Here, the dimension of a module is defined to be zero if the module has infinite rank, and the rank of a module is converted to a natural number using the `Cardinal.toNat` function.
More concisely: If `f` is an injective linear map from the module `M` to the module `N` over a ring `R`, then the dimension of the range of `f` equals the dimension of `M`.
|