FiniteDimensional.finrank_of_not_finite
theorem FiniteDimensional.finrank_of_not_finite :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : StrongRankCondition R] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : Module.Free R M], ¬Module.Finite R M → FiniteDimensional.finrank R M = 0
This theorem states that for any ring `R` that satisfies the strong rank condition, and any additive commutative group `M` that is also a module over `R` and is freely generated, if `M` is not a finite `R`-module, then the rank of `M` as a `R`-module, as defined by `FiniteDimensional.finrank`, is zero. Essentially, if a vector space `M` over a field `R` has infinite dimension, then its "finite rank" is conventionally defined to be zero.
More concisely: For any commutative ring `R` satisfying the strong rank condition, if `M` is an additive commutative group freely generated as an `R`-module and infinite as a set, then `FiniteDimensional.finrank R M = 0`.
|
Module.Free.rank_eq_card_chooseBasisIndex
theorem Module.Free.rank_eq_card_chooseBasisIndex :
∀ (R : Type u) (M : Type v) [inst : Ring R] [inst_1 : StrongRankCondition R] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : Module.Free R M],
Module.rank R M = Cardinal.mk (Module.Free.ChooseBasisIndex R M)
The theorem `Module.Free.rank_eq_card_chooseBasisIndex` states that for any ring `R` and any free module `M` over `R`, given that `R` satisfies the strong rank condition and `M` is an additive commutative group and a module over `R`, the rank of the module `M` is equal to the cardinality of the set `ChooseBasisIndex R M`. In other words, the rank of a free module is the cardinality of the type that indexes its basis.
More concisely: For any free module M over a ring R satisfying the strong rank condition, the rank of M equals the cardinality of a basis for M.
|
nonempty_linearEquiv_of_rank_eq
theorem nonempty_linearEquiv_of_rank_eq :
∀ {R : Type u} {M M₁ : Type v} [inst : Ring R] [inst_1 : StrongRankCondition R] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : Module.Free R M] [inst_5 : AddCommGroup M₁] [inst_6 : Module R M₁]
[inst_7 : Module.Free R M₁], Module.rank R M = Module.rank R M₁ → Nonempty (M ≃ₗ[R] M₁)
The theorem `nonempty_linearEquiv_of_rank_eq` states that for any ring 'R' and any two vector spaces 'M' and 'M₁' over 'R' (with certain conditions including the Strong Rank Condition and the requirement that the modules are free), if the rank of 'M' is equal to the rank of 'M₁', then there exists a nonempty linear equivalence between 'M' and 'M₁'. In other words, two vector spaces are isomorphic if they have the same dimension.
More concisely: For free modules 'M' and 'M₁' over a ring 'R' satisfying the Strong Rank Condition, if the ranks of 'M' and 'M₁' are equal, then there exists a nonempty linear equivalence between 'M' and 'M₁'.
|
FiniteDimensional.nonempty_linearEquiv_of_finrank_eq
theorem FiniteDimensional.nonempty_linearEquiv_of_finrank_eq :
∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Ring R] [inst_1 : StrongRankCondition R]
[inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : Module.Free R M] [inst_5 : AddCommGroup M']
[inst_6 : Module R M'] [inst_7 : Module.Free R M'] [inst_8 : Module.Finite R M] [inst_9 : Module.Finite R M'],
FiniteDimensional.finrank R M = FiniteDimensional.finrank R M' → Nonempty (M ≃ₗ[R] M')
This theorem states that for any ring `R` and any two modules `M` and `M'` over `R`, if `R` satisfies the strong rank condition, and both `M` and `M'` are free and finite modules over `R`, then if the finite rank of `M` equals the finite rank of `M'`, there exists a linear equivalence between `M` and `M'`. In other words, two finite and free modules are isomorphic if they have the same finite rank.
More concisely: For any ring `R` satisfying the strong rank condition, two free and finite `R`-modules of equal rank are isomorphic.
|
Module.rank_lt_alpeh0_iff
theorem Module.rank_lt_alpeh0_iff :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : StrongRankCondition R] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : Module.Free R M], Module.rank R M < Cardinal.aleph0 ↔ Module.Finite R M
This theorem states that for any given types `R` and `M`, where `R` is a ring, `M` is an additive commutative group, `M` is a module over `R`, and `M` is a free module over `R`, the rank of the module `M` over `R` is less than `ℵ₀` (the smallest infinite cardinal) if and only if the module `M` over `R` is finite. Here, `StrongRankCondition R` asserts that `R` satisfies the strong rank condition, i.e., every right module has a well-defined rank. Note that `Module.rank R M` refers to the rank of the module and `Module.Finite R M` indicates that the module is finite. The counterpart of this theorem for the inverse direction without the free module condition is `rank_lt_aleph0`.
More concisely: For a ring `R`, additive commutative group `M` being an `R`-module and free `R`-module, the rank of `M` over `R` is strictly less than the first infinite cardinal `ℵ₀` if and only if `M` is a finite `R`-module.
|
nonempty_linearEquiv_of_lift_rank_eq
theorem nonempty_linearEquiv_of_lift_rank_eq :
∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Ring R] [inst_1 : StrongRankCondition R]
[inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : Module.Free R M] [inst_5 : AddCommGroup M']
[inst_6 : Module R M'] [inst_7 : Module.Free R M'],
Cardinal.lift.{v', v} (Module.rank R M) = Cardinal.lift.{v, v'} (Module.rank R M') → Nonempty (M ≃ₗ[R] M')
The theorem `nonempty_linearEquiv_of_lift_rank_eq` states that for any ring `R` and two vector spaces `M` and `M'` over `R`, if the lifted cardinality of the rank (dimension) of `M` is equal to the lifted cardinality of the rank of `M'`, there exists a linear isomorphism between `M` and `M'`. The vector spaces are assumed to be free modules over `R`, which ensures the existence of a basis, and `R` is assumed to satisfy the strong rank condition, which ensures that all free modules have a well-defined rank. In other words, two vector spaces over a ring with the strong rank condition are isomorphic if they have the same dimension.
More concisely: Given free vector spaces M and M' over a ring R satisfying the strong rank condition, if the lifted ranks of M and M' are equal, then there exists a linear isomorphism from M to M'.
|
FiniteDimensional.finrank_eq_card_chooseBasisIndex
theorem FiniteDimensional.finrank_eq_card_chooseBasisIndex :
∀ (R : Type u) (M : Type v) [inst : Ring R] [inst_1 : StrongRankCondition R] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : Module.Free R M] [inst_5 : Module.Finite R M],
FiniteDimensional.finrank R M = Fintype.card (Module.Free.ChooseBasisIndex R M)
The theorem `FiniteDimensional.finrank_eq_card_chooseBasisIndex` states that for any ring `R` with a strong rank condition, any module `M` over `R` that is both free and finite, the rank of the module `M` (also known as finite dimension) is equal to the cardinality of the index set that indexes the basis of `M`. In other words, the number of basis elements of `M` is the same as the dimension of `M`. Here, the rank of a module is defined to be 0 if the module has infinite rank.
More concisely: For a free and finite module M over a ring R with a strong rank condition, the rank (or finite dimension) of M equals the cardinality of a basis for M.
|
FiniteDimensional.nonempty_linearEquiv_iff_finrank_eq
theorem FiniteDimensional.nonempty_linearEquiv_iff_finrank_eq :
∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Ring R] [inst_1 : StrongRankCondition R]
[inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : Module.Free R M] [inst_5 : AddCommGroup M']
[inst_6 : Module R M'] [inst_7 : Module.Free R M'] [inst_8 : Module.Finite R M] [inst_9 : Module.Finite R M'],
Nonempty (M ≃ₗ[R] M') ↔ FiniteDimensional.finrank R M = FiniteDimensional.finrank R M'
The theorem states that for any two finite and free modules M and M', defined over a ring R with the strong rank condition, there exists a linear equivalence between M and M', if and only if the ranks of M and M' as finite-dimensional modules over R are equal. These ranks are defined to be 0 if the modules have infinite rank. The strong rank condition is a condition on the ring R that ensures uniqueness of rank for its modules. The phrase "M ≃ₗ[R] M'" in Lean 4 denotes the linear equivalence between M and M', meaning there is a bijective linear transformation from M to M'.
More concisely: For any two finite free modules M and M' over a ring R with the strong rank condition, they are linearly equivalent if and only if they have equal rank as finite-dimensional modules.
|
LinearEquiv.nonempty_equiv_iff_lift_rank_eq
theorem LinearEquiv.nonempty_equiv_iff_lift_rank_eq :
∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Ring R] [inst_1 : StrongRankCondition R]
[inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : Module.Free R M] [inst_5 : AddCommGroup M']
[inst_6 : Module R M'] [inst_7 : Module.Free R M'],
Nonempty (M ≃ₗ[R] M') ↔ Cardinal.lift.{v', v} (Module.rank R M) = Cardinal.lift.{v, v'} (Module.rank R M')
This theorem states that for any ring `R` and two vector spaces `M` and `M'` over `R` that satisfy the strong rank condition and are free modules, there exists a linear isomorphism between `M` and `M'` if and only if the dimensions (or ranks) of `M` and `M'`, when lifted to a common universe, are equal. In other words, two vector spaces are isomorphic (can be matched one-for-one) precisely when they have equal dimension.
More concisely: For free modules `M` and `M'` over a ring `R` satisfying the strong rank condition, there exists a linear isomorphism between them if and only if their dimensions are equal.
|
FiniteDimensional.finrank_mul_finrank
theorem FiniteDimensional.finrank_mul_finrank :
∀ (F : Type u) (K : Type v) (A : Type w) [inst : Ring F] [inst_1 : Ring K] [inst_2 : AddCommGroup A]
[inst_3 : Module F K] [inst_4 : Module K A] [inst_5 : Module F A] [inst_6 : IsScalarTower F K A]
[inst_7 : StrongRankCondition F] [inst_8 : StrongRankCondition K] [inst_9 : Module.Free F K]
[inst_10 : Module.Free K A],
FiniteDimensional.finrank F K * FiniteDimensional.finrank K A = FiniteDimensional.finrank F A
This theorem, known as the Tower Law, states that for a module `A` over a field `K`, if `K` is an extension of a field `F`, then the rank of `A` with respect to `F` is equal to the product of the rank of `K` with respect to `F` and the rank of `A` with respect to `K`. Specifically, if we denote the rank as $\operatorname{rank}$, the theorem can be written as $\operatorname{rank}_F(A) = \operatorname{rank}_F(K) \times \operatorname{rank}_K(A)$. The theorem assumes that `F` and `K` satisfy the Strong Rank Condition and that `K` and `A` are free modules.
More concisely: For free modules `A` over a field `K`, the rank of `A` with respect to a subfield `F` equals the product of the rank of `K` with respect to `F` and the rank of `A` with respect to `K`.
|
LinearEquiv.nonempty_equiv_iff_rank_eq
theorem LinearEquiv.nonempty_equiv_iff_rank_eq :
∀ {R : Type u} {M M₁ : Type v} [inst : Ring R] [inst_1 : StrongRankCondition R] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : Module.Free R M] [inst_5 : AddCommGroup M₁] [inst_6 : Module R M₁]
[inst_7 : Module.Free R M₁], Nonempty (M ≃ₗ[R] M₁) ↔ Module.rank R M = Module.rank R M₁
The theorem states that for any given ring `R` and two types `M` and `M₁` that form vector spaces over `R` under addition and scalar multiplication, there exists a linear equivalence between `M` and `M₁` if and only if the rank (dimension) of the vector space `M` is equal to the rank of the vector space `M₁`. Here, the rank of a vector space is defined as the maximum size of any of its linearly independent subsets. This is operating under the condition that `R` has the strong rank condition, which ensures uniqueness of rank for each module.
More concisely: For any ring `R` with the strong rank condition, two `R`-modules `M` and `M₁` of equal rank are linearly equivalent.
|
rank_mul_rank
theorem rank_mul_rank :
∀ (F : Type u) (K : Type v) [inst : Ring F] [inst_1 : Ring K] [inst_2 : Module F K] [inst_3 : StrongRankCondition F]
[inst_4 : StrongRankCondition K] [inst_5 : Module.Free F K] (A : Type v) [inst_6 : AddCommGroup A]
[inst_7 : Module K A] [inst_8 : Module F A] [inst_9 : IsScalarTower F K A] [inst_10 : Module.Free K A],
Module.rank F K * Module.rank K A = Module.rank F A
This theorem, referred to as the tower law, states that for a `K`-module `A` where `K` is an extension of `F`, the rank of `A` over `F` is equal to the product of the rank of `K` over `F` and the rank of `A` over `K`. In other words, $\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$. This is a simpler version of another theorem `lift_rank_mul_lift_rank` where `K` and `A` are in the same universe. The theorem holds under certain conditions including `K` and `F` having strong rank conditions, `K` being a free `F`-module, and `A` being a free `K`-module with scalar tower structure over `F`, `K`, and `A`.
More concisely: The rank of a free `K`-module `A` over a field extension `K` of `F` is equal to the product of the rank of `K` over `F` and the rank of `A` over `K`.
|
Module.Free.rank_eq_mk_of_infinite_lt
theorem Module.Free.rank_eq_mk_of_infinite_lt :
∀ (R : Type u) (M : Type v) [inst : Ring R] [inst_1 : StrongRankCondition R] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : Module.Free R M] [inst_5 : Infinite R],
Cardinal.lift.{v, u} (Cardinal.mk R) < Cardinal.lift.{u, v} (Cardinal.mk M) → Module.rank R M = Cardinal.mk M
This theorem states that if we have a free module `M` over an infinite scalar ring `R`, then the rank of the module `M` is equal to the cardinality of `M` whenever the cardinality of `R` is less than the cardinality of `M`. This is denoted as `#R < #M`, where `#R` represents the cardinality of `R` and `#M` represents the cardinality of `M`. The cardinality is the number of elements in a set, and the rank of a module, in this context, broadly refers to the maximum size of any of its independent subsets.
In other words, for any types `R` and `M` where `R` is a ring with the strong rank condition, `M` is an additive commutative group and a free module over `R`, and `R` is infinite, if the lifted cardinality of `R` is less than the lifted cardinality of `M`, then the rank of the module `M` over `R` equals the cardinality of `M`.
More concisely: If `R` is an infinite ring with the strong rank condition, `M` is a free `R`-module with infinite cardinality, then the rank of `M` equals its cardinality.
|
lift_rank_mul_lift_rank
theorem lift_rank_mul_lift_rank :
∀ (F : Type u) (K : Type v) (A : Type w) [inst : Ring F] [inst_1 : Ring K] [inst_2 : AddCommGroup A]
[inst_3 : Module F K] [inst_4 : Module K A] [inst_5 : Module F A] [inst_6 : IsScalarTower F K A]
[inst_7 : StrongRankCondition F] [inst_8 : StrongRankCondition K] [inst_9 : Module.Free F K]
[inst_10 : Module.Free K A],
Cardinal.lift.{w, v} (Module.rank F K) * Cardinal.lift.{v, w} (Module.rank K A) =
Cardinal.lift.{v, w} (Module.rank F A)
This theorem, known as the "Tower Law", states that for any types `F`, `K`, and `A` -- where `F` and `K` are rings, `A` is an additive commutative group, and the module and scalar tower structure is given over these types -- the rank of the module `A` over the field `F` is equal to the product of the rank of the module `A` over the field `K` and the rank of the field `K` over the field `F`. This statement holds under the conditions that both `F` and `K` satisfy the strong rank condition, and both `K` and `A` are free modules. In formal language notation, this can be written as $\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$.
More concisely: The rank of a free module over a field is multiplicatively equal to the rank of the module over an intermediate field times the rank of that field over the base field, given both fields satisfy the strong rank condition.
|
Module.finite_of_finrank_pos
theorem Module.finite_of_finrank_pos :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : StrongRankCondition R] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : Module.Free R M], 0 < FiniteDimensional.finrank R M → Module.Finite R M
This theorem states that if a module `M` over a ring `R` has a positive finite rank (the rank is a natural number and greater than zero), and if `R` satisfies the strong rank condition (a condition related to the finiteness of bases of modules) and `M` is a free module over `R` (it has a basis), then the module `M` is a finite module. In the context of linear algebra, this essentially means that the module (which can be thought of as a vector space) has a finite basis.
More concisely: If `M` is a free module of positive finite rank over a ring `R` satisfying the strong rank condition, then `M` is a finite module.
|