FiniteDimensional.finrank_finsupp_self
theorem FiniteDimensional.finrank_finsupp_self :
∀ (R : Type u) [inst : Ring R] [inst_1 : StrongRankCondition R] {ι : Type v} [inst_2 : Fintype ι],
FiniteDimensional.finrank R (ι →₀ R) = Fintype.card ι
This theorem states that the finite rank of the free module `(ι →₀ R)` over a ring `R`, where `R` satisfies the strong rank condition, is equal to the cardinality of the finite type `ι`. In other words, the dimension of the vector space of functions from `ι` to `R` (with finite support, hence the `finsupp`), as a module over `R`, is the same as the number of elements in the set `ι`.
More concisely: The rank of the free module of functions from a finite type `ι` to a ring `R` satisfying the strong rank condition equals the cardinality of `ι`.
|
FiniteDimensional.finrank_pi_fintype
theorem FiniteDimensional.finrank_pi_fintype :
∀ (R : Type u) [inst : Ring R] [inst_1 : StrongRankCondition R] {ι : Type v} [inst_2 : Fintype ι] {M : ι → Type w}
[inst_3 : (i : ι) → AddCommGroup (M i)] [inst_4 : (i : ι) → Module R (M i)]
[inst_5 : ∀ (i : ι), Module.Free R (M i)] [inst_6 : ∀ (i : ι), Module.Finite R (M i)],
FiniteDimensional.finrank R ((i : ι) → M i) = Finset.univ.sum fun i => FiniteDimensional.finrank R (M i)
This theorem states that, in a ring `R` with the strong rank condition and for a finite type `ι`, the rank of the direct product of a family of modules `(M i)` indexed by `ι` is equal to the sum of the ranks of the individual modules `(M i)`. Here, each `M i` is a free, finite module over the ring `R`. The sum is taken over all elements in the universal finite set of the type `ι`. In summary, the dimension of a finite direct product of vector spaces is the sum of the dimensions of the individual spaces.
More concisely: In a ring with the strong rank condition, the rank of a finite direct product of free, finite modules is equal to the sum of the ranks of the individual modules.
|
rank_fun'
theorem rank_fun' :
∀ {R : Type u} {η : Type u₁'} [inst : Ring R] [inst_1 : StrongRankCondition R] [inst_2 : Fintype η],
Module.rank R (η → R) = ↑(Fintype.card η)
The theorem `rank_fun'` states that for any type `R` with a ring structure, any type `η` that is a finite type, and given that `R` satisfies the strong rank condition, the rank of the module of functions from `η` to `R` over `R` is equal to the cardinality of `η`. In mathematical terms, if `R` is a ring and `η` is a finite set, then the dimension of the vector space of functions from `η` to `R` over `R` is the same as the number of elements in `η`. The strong rank condition is a property of the ring `R` that guarantees certain properties about the linear independence of elements in modules over `R`.
More concisely: For any finite type `η` and ring `R` satisfying the strong rank condition, the dimension of the vector space of functions from `η` to `R` equals the cardinality of `η`.
|
finrank_span_le_card
theorem finrank_span_le_card :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : StrongRankCondition R] (s : Set M) [inst_4 : Fintype ↑s],
FiniteDimensional.finrank R ↥(Submodule.span R s) ≤ s.toFinset.card
The theorem `finrank_span_le_card` states that for any type `R` with a ring structure, any type `M` with an additive commutative group structure and also a `R`-module structure, given the strong rank condition holds for `R`, and a set `s` of `M` with a finiteness condition, the finite rank of the span of set `s` as an `R`-module is less than or equal to the cardinality of the finset formed by enumerating the set `s`. In other words, the dimension of the subspace spanned by a finite set `s` is always less than or equal to the number of elements in `s` in a module over a ring with the strong rank condition.
More concisely: For any ring `R` with strong rank condition, any additive commutative group `M` with an `R`-module structure, and finite set `s` in `M`, the rank of the submodule generated by `s` is less than or equal to the cardinality of `s`.
|
rank_tensorProduct'
theorem rank_tensorProduct' :
∀ {S : Type u} {M M₁ : Type v} [inst : CommRing S] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₁]
[inst_3 : StrongRankCondition S] [inst_4 : Module S M] [inst_5 : Module.Free S M] [inst_6 : Module S M₁]
[inst_7 : Module.Free S M₁], Module.rank S (TensorProduct S M M₁) = Module.rank S M * Module.rank S M₁
The theorem `rank_tensorProduct'` states that if `M` and `M'` are two modules lying in the same universe, and `S` is a commutative ring under which `M` and `M'` are both free modules with a strong rank condition, then the rank of the tensor product of `M` and `M'` over `S`, denoted as `M ⊗[S] M'`, is equal to the product of the rank of `M` and the rank of `M'`. Here, the rank of a module is the cardinality of a basis of the module.
More concisely: If `M` and `M'` are free modules over a commutative ring `S` with a strong rank condition, then the rank of their tensor product `M ⊗[S] M'` is equal to the product of the ranks of `M` and `M'`.
|
rank_tensorProduct
theorem rank_tensorProduct :
∀ {S : Type u} {M : Type v} {M' : Type v'} [inst : CommRing S] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M']
[inst_3 : StrongRankCondition S] [inst_4 : Module S M] [inst_5 : Module.Free S M] [inst_6 : Module S M']
[inst_7 : Module.Free S M'],
Module.rank S (TensorProduct S M M') =
Cardinal.lift.{v', v} (Module.rank S M) * Cardinal.lift.{v, v'} (Module.rank S M')
The theorem `rank_tensorProduct` states that for any given type `S` with a commutative ring structure, and types `M` and `M'` both equipped with additive commutative group structures and module structures over `S`, assuming `S` satisfies the strong rank condition and both `M` and `M'` are free modules over `S`, the rank of the tensor product `M ⊗[S] M'` is the product of the ranks of `M` and `M'`, each lifted to the maximum of the universes of `M` and `M'`. This is expressed in Lean as `Module.rank S (TensorProduct S M M') = Cardinal.lift.{v', v} (Module.rank S M) * Cardinal.lift.{v, v'} (Module.rank S M')`.
More concisely: For free modules `M` and `M'` over a commutative ring `S` satisfying the strong rank condition, the rank of their tensor product `M ⊗[S] M'` is the product of their individual ranks, each lifted to the maximum universe.
|
rank_matrix'
theorem rank_matrix' :
∀ (R : Type u) [inst : Ring R] [inst_1 : StrongRankCondition R] (m n : Type v) [inst_2 : Finite m]
[inst_3 : Finite n], Module.rank R (Matrix m n R) = Cardinal.lift.{u, v} (Cardinal.mk m * Cardinal.mk n)
The theorem `rank_matrix'` asserts that for any type `R` that is a ring and satisfies a strong rank condition, and two types `m` and `n` that are finite (thus representing finite sets), the rank of the matrix with entries in `R` and indexed by `m` and `n` is equal to the lifted cardinal product of the cardinalities of `m` and `n`. This means, in essence, if `m` and `n` are sets with finite elements, then the dimension of the vector space of `m` by `n` matrices over the ring `R` is the product of the sizes of `m` and `n`.
More concisely: For any ring `R` satisfying a strong rank condition and finite types `m` and `n`, the rank of an `m` by `n` matrix over `R` equals the product of the cardinalities of `m` and `n`.
|
rank_finsupp
theorem rank_finsupp :
∀ (R : Type u) (M : Type v) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : StrongRankCondition R] [inst_4 : Module.Free R M] (ι : Type w),
Module.rank R (ι →₀ M) = Cardinal.lift.{v, w} (Cardinal.mk ι) * Cardinal.lift.{w, v} (Module.rank R M)
This theorem, `rank_finsupp`, states that for any type `R` representing a ring, any type `M` representing a module over `R`, and any type `ι`, under the conditions that `R` has the strong rank condition and `M` is a free module over `R`, the rank of the free module over `R` with basis type `ι →₀ M` is equal to the product of the cardinality of `ι` lifted to the maximum of the universes of `ι` and `M`, and the rank of `M` lifted to the maximum of the universes of `M` and `ι`. In other words, if $\text{Card}(\text{Type})$ denotes the cardinality of a type and $\text{rank}_R(M)$ denotes the rank of a module $M$ over a ring $R$, then the theorem states:
$$\text{rank}_R(\iota \rightarrow₀ M) = \text{Card}_{\text{lift}}(\iota) \times \text{Card}_{\text{lift}}(\text{rank}_R(M))$$
where the subscript 'lift' indicates that the cardinalities are lifted to the appropriate universe level.
More concisely: The rank of a free module over a ring with the strong rank condition is equal to the product of the cardinality of its basis, lifted to the maximum universe level, and the rank of the module, also lifted to the maximum universe level.
|
Submodule.finrank_map_le
theorem Submodule.finrank_map_le :
∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M']
[inst_3 : Module R M] [inst_4 : Module R M'] [inst_5 : StrongRankCondition R] (f : M →ₗ[R] M') (p : Submodule R M)
[inst_6 : Module.Finite R ↥p],
FiniteDimensional.finrank R ↥(Submodule.map f p) ≤ FiniteDimensional.finrank R ↥p
This theorem, titled `Submodule.finrank_map_le`, states that for any ring `R`, and two modules `M` and `M'` over `R`, along with a linear map `f` from `M` to `M'` and a finite submodule `p` of `M`, the rank (as a natural number) of the pushforward of `p` via `f` (denoted as `Submodule.map f p`) is less than or equal to the rank of `p`. This is under the assumption that `R` satisfies the strong rank condition, implying that the rank function behaves well under taking submodules and quotient modules.
More concisely: For any ring `R` satisfying the strong rank condition, the rank of the pushforward of a finite submodule `p` of module `M` under a linear map `f` from `M` to module `M'` is less than or equal to the rank of `p`.
|
rank_finsupp_self
theorem rank_finsupp_self :
∀ (R : Type u) [inst : Ring R] [inst_1 : StrongRankCondition R] (ι : Type w),
Module.rank R (ι →₀ R) = Cardinal.lift.{u, w} (Cardinal.mk ι)
This theorem states that for any type `R` that forms a ring and satisfies the strong rank condition, and for any type `ι`, the rank of the module `(ι →₀ R)` equals the lift of the cardinality of `ι`. In other words, the rank of the free module of the ring `R` indexed by the type `ι` equals the lift of the cardinality of `ι`. Here, the `lift` operation moves the cardinal number to a possibly higher universe, and `Cardinal.mk ι` computes the cardinality (size) of the type `ι`.
More concisely: For any ring `R` satisfying the strong rank condition and type `ι`, the rank of the free module `ι →₀ R` equals the cardinality of `ι` lifted to a higher universe.
|
rank_span_le
theorem rank_span_le :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : StrongRankCondition R] (s : Set M), Module.rank R ↥(Submodule.span R s) ≤ Cardinal.mk ↑s
This theorem states that for any given ring `R`, additive commutative group `M`, and a module structure over `R` and `M`, under the strong rank condition for `R`, the rank of the submodule spanned by a set `s` in `M` is less than or equal to the cardinality of the set `s`. In other words, the cardinality of a basis of the submodule generated by a set `s` can not exceed the cardinality of the set `s` itself.
More concisely: For any ring `R`, additive commutative group `M` with an `R`-module structure, and set `s` in `M`, under the strong rank condition for `R`, the rank of the submodule generated by `s` is less than or equal to the cardinality of `s`.
|
rank_pi
theorem rank_pi :
∀ {R : Type u} {η : Type u₁'} {φ : η → Type u_1} [inst : Ring R] [inst_1 : StrongRankCondition R]
[inst_2 : (i : η) → AddCommGroup (φ i)] [inst_3 : (i : η) → Module R (φ i)]
[inst_4 : ∀ (i : η), Module.Free R (φ i)] [inst_5 : Finite η],
Module.rank R ((i : η) → φ i) = Cardinal.sum fun i => Module.rank R (φ i)
The theorem `rank_pi` states that for any ring `R` satisfying the strong rank condition, any family of additive commutative groups `φ i` indexed by `η` that are also `R`-modules, and any `η` which is finite, if every `φ i` is a free `R`-module, then the rank of the product module - denoted as a function from `η` to `φ` - is equal to the sum of the ranks of the individual `φ i` modules. In other words, the rank of a finite product of free modules is the sum of the ranks.
More concisely: For any ring satisfying the strong rank condition, the rank of a finite product of free `R`-modules is the sum of the ranks of the individual modules.
|
FiniteDimensional.finrank_fintype_fun_eq_card
theorem FiniteDimensional.finrank_fintype_fun_eq_card :
∀ (R : Type u) {η : Type u₁'} [inst : Ring R] [inst_1 : StrongRankCondition R] [inst_2 : Fintype η],
FiniteDimensional.finrank R (η → R) = Fintype.card η
This theorem states that for any type `R` which forms a ring and satisfies the strong rank condition, and for any finite type `η`, the rank of the vector space of functions from `η` to `R` is equal to the number of elements in `η`. In other words, if you have a set `η` of elements and the set of all functions mapping these elements to a ring `R` form a vector space, the dimension (or rank) of this vector space is the same as the number of elements in the original set `η`.
More concisely: For any finite type `η` and ring `R` satisfying the strong rank condition, the dimension of the vector space of functions from `η` to `R` equals the cardinality of `η`.
|
Submodule.finrank_quotient_le
theorem Submodule.finrank_quotient_le :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : StrongRankCondition R] [inst_4 : Module.Finite R M] (s : Submodule R M),
FiniteDimensional.finrank R (M ⧸ s) ≤ FiniteDimensional.finrank R M
This theorem states that the rank (or dimension) of a quotient module (M/s) over a ring R is less than or equal to the rank of the original module M. It is applicable under the conditions that R is a ring, M is an additive commutative group and a module over R, R satisfies the Strong Rank Condition, and M is a finite module. The rank is defined to be zero if the space has infinite rank. For a vector space M over a field R, the rank is the same as the finite dimension of M over R.
More concisely: The rank of a quotient module over a ring with the Strong Rank Condition and a finite module is less than or equal to the rank of the original module.
|
FiniteDimensional.finrank_pi
theorem FiniteDimensional.finrank_pi :
∀ (R : Type u) [inst : Ring R] [inst_1 : StrongRankCondition R] {ι : Type v} [inst_2 : Fintype ι],
FiniteDimensional.finrank R (ι → R) = Fintype.card ι
The theorem `FiniteDimensional.finrank_pi` states that the rank of the function space `(ι → R)`, where `R` is a ring and `ι` is a finite type, is equal to the cardinality of `ι`. In other words, when considering the space of functions from a finite set `ι` to a ring `R`, the dimension of this vector space over the ring `R` is just the number of elements in the set `ι`. The ring `R` is assumed to satisfy the strong rank condition, which is a property that prevents certain infinite-dimensional counterexamples.
More concisely: The rank of the function space from a finite type to a ring satisfying the strong rank condition is equal to the cardinality of the type.
|
FiniteDimensional.finrank_prod
theorem FiniteDimensional.finrank_prod :
∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M']
[inst_3 : Module R M] [inst_4 : Module R M'] [inst_5 : StrongRankCondition R] [inst_6 : Module.Free R M]
[inst_7 : Module.Free R M'] [inst_8 : Module.Finite R M] [inst_9 : Module.Finite R M'],
FiniteDimensional.finrank R (M × M') = FiniteDimensional.finrank R M + FiniteDimensional.finrank R M'
The theorem `FiniteDimensional.finrank_prod` states that for any ring `R`, and any two modules `M` and `M'` over `R`, the rank of the product module `M × M'` is equal to the sum of the ranks of `M` and `M'`. This is true under the assumptions that `R` has the strong rank condition, and that `M` and `M'` are both free and finite modules over `R`. In terms of linear algebra, this states that the dimension of the direct sum of two vector spaces is the sum of the dimensions of the individual spaces.
More concisely: For any ring `R` with the strong rank condition and free, finite modules `M` and `M'` over `R`, the rank of their product `M × M'` equals the sum of the ranks of `M` and `M'`.
|
rank_finsupp_self'
theorem rank_finsupp_self' :
∀ (R : Type u) [inst : Ring R] [inst_1 : StrongRankCondition R] {ι : Type u},
Module.rank R (ι →₀ R) = Cardinal.mk ι
The theorem `rank_finsupp_self'` states that for any type `R` that is a ring and satisfies the strong rank condition, and for any type `ι` in the same universe as `R`, the rank of the free module `(ι →₀ R)` is equal to the cardinality of `ι`. In other words, it says that the rank of the free module over a ring `R` with basis indexed by `ι` is equal to the number of elements in the indexing set `ι`.
More concisely: The rank of the free module over a ring satisfying the strong rank condition is equal to the cardinality of its basis.
|
FiniteDimensional.finrank_fin_fun
theorem FiniteDimensional.finrank_fin_fun :
∀ (R : Type u) [inst : Ring R] [inst_1 : StrongRankCondition R] {n : ℕ},
FiniteDimensional.finrank R (Fin n → R) = n
This theorem states that the rank of the vector space of functions from a finite set `Fin n` to a ring `R` (denoted as `Fin n → R`) is equal to `n`. Here, `R` is any type that has a ring structure, and `StrongRankCondition R` ensures that all left modules over `R` are free. In other words, for any ring `R` satisfying the strong rank condition and any natural number `n`, the dimension (as a natural number) of the vector space of functions that map from a set with `n` elements to `R` is `n`.
More concisely: For any ring `R` satisfying the strong rank condition, the vector space of functions from a finite set with `n` elements to `R` has dimension `n`.
|
rank_matrix
theorem rank_matrix :
∀ (R : Type u) [inst : Ring R] [inst_1 : StrongRankCondition R] (m : Type v) (n : Type w) [inst_2 : Finite m]
[inst_3 : Finite n],
Module.rank R (Matrix m n R) =
Cardinal.lift.{max v w u, v} (Cardinal.mk m) * Cardinal.lift.{max v w u, w} (Cardinal.mk n)
The theorem `rank_matrix` states that for any type `R` that is a ring and satisfies the Strong Rank Condition, and two types `m` and `n` that are finite (i.e., they have a finite number of elements), the rank of the matrix with entries in `R`, rows indexed by `m` and columns indexed by `n` (denoted as `Matrix m n R`), is equal to the product of the cardinalities (number of elements) of `m` and `n`, each lifted to the maximum of the universe levels of `m`, `n`, and `R`. This means that the dimension of the vector space of such matrices over the ring `R` is determined by the number of elements in `m` and `n`.
More concisely: For any finite types `m` and `n` over a ring `R` satisfying the Strong Rank Condition, the rank of a `Matrix m n R` is equal to the product of the cardinalities of `m` and `n`, each lifted to the maximum universe level.
|
Submodule.finrank_le
theorem Submodule.finrank_le :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : StrongRankCondition R] [inst_4 : Module.Finite R M] (s : Submodule R M),
FiniteDimensional.finrank R ↥s ≤ FiniteDimensional.finrank R M
The theorem `Submodule.finrank_le` states that for any ring `R` and any `R`-module `M` (a kind of mathematical structure that generalizes vector spaces), if `M` has a finite rank and `R` has the strong rank condition (a certain technical property), then the rank (or dimension) of any submodule `s` of `M` (which can be thought of as a "subspace" of `M`) is less than or equal to the rank of `M` itself. In other words, the dimension of a subspace cannot exceed the dimension of the space that contains it.
More concisely: For any ring with the strong rank condition and a finite-rank module, the rank of any submodule is less than or equal to the rank of the module itself.
|
FiniteDimensional.finrank_matrix
theorem FiniteDimensional.finrank_matrix :
∀ (R : Type u) [inst : Ring R] [inst_1 : StrongRankCondition R] (m : Type u_2) (n : Type u_3) [inst_2 : Fintype m]
[inst_3 : Fintype n], FiniteDimensional.finrank R (Matrix m n R) = Fintype.card m * Fintype.card n
This theorem states that if `m` and `n` are types that have finite cardinalities (i.e., they are `Fintype`), then the rank of the matrix with entries in a ring `R` (which satisfies the Strong Rank Condition) and whose rows are indexed by `m` and columns are indexed by `n`, is equal to the product of cardinalities of `m` and `n`. In simpler terms, the dimension of the space of all `m × n` matrices over a ring `R` is the product of the number of elements in `m` and `n`.
More concisely: If `m` and `n` are finite types and `R` is a ring satisfying the Strong Rank Condition, then the rank of an `m × n` matrix over `R` equals the product of the cardinalities of `m` and `n`.
|
Subalgebra.rank_bot
theorem Subalgebra.rank_bot :
∀ {F : Type u_2} {E : Type u_3} [inst : CommRing F] [inst_1 : Ring E] [inst_2 : Algebra F E]
[inst_3 : StrongRankCondition F] [inst_4 : NoZeroSMulDivisors F E] [inst_5 : Nontrivial E],
Module.rank F ↥⊥ = 1
This theorem states that for any types `F` and `E`, where `F` is a commutative ring, `E` is a ring, and `E` is an algebra over `F`. Also, `F` satisfies the strong rank condition, there are no zero `smul` divisors in `F` and `E`, and `E` is nontrivial. Then, the rank of the module that corresponds to the bottom element (zero subalgebra) of the lattice of subalgebras of `E` over `F` is always equal to `1`.
More concisely: For a commutative ring `F` satisfying the strong rank condition with no zero divisors, and `E` being an algebra over `F` with no zero divisors and being nontrivial, the rank of the bottom element of the lattice of subalgebras of `E` over `F` equals 1.
|
FiniteDimensional.finrank_tensorProduct
theorem FiniteDimensional.finrank_tensorProduct :
∀ {S : Type u} {M : Type v} {M' : Type v'} [inst : CommRing S] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M']
[inst_3 : StrongRankCondition S] [inst_4 : Module S M] [inst_5 : Module.Free S M] [inst_6 : Module S M']
[inst_7 : Module.Free S M'],
FiniteDimensional.finrank S (TensorProduct S M M') =
FiniteDimensional.finrank S M * FiniteDimensional.finrank S M'
The theorem `FiniteDimensional.finrank_tensorProduct` states that for any commutative ring `S` and any two modules `M` and `M'` over `S` that satisfy the `StrongRankCondition` and are free modules, the rank (as a natural number) of the tensor product module `M ⊗[S] M'` (denoted as `FiniteDimensional.finrank S (TensorProduct S M M')` in Lean) is the product of the ranks of `M` and `M'` (denoted as `FiniteDimensional.finrank S M * FiniteDimensional.finrank S M'`). In mathematical terms, this means that dimₛ(M ⊗ₛ M') = dimₛ(M) * dimₛ(M'). The `StrongRankCondition` ensures that the rank function behaves well under direct sums of modules.
More concisely: For free modules M and M' over a commutative ring S satisfying the StrongRankCondition, the rank of their tensor product M ⊗[S] M' equals the product of the ranks of M and M'.
|
FiniteDimensional.finrank_directSum
theorem FiniteDimensional.finrank_directSum :
∀ (R : Type u) [inst : Ring R] [inst_1 : StrongRankCondition R] {ι : Type v} [inst_2 : Fintype ι] (M : ι → Type w)
[inst_3 : (i : ι) → AddCommGroup (M i)] [inst_4 : (i : ι) → Module R (M i)]
[inst_5 : ∀ (i : ι), Module.Free R (M i)] [inst_6 : ∀ (i : ι), Module.Finite R (M i)],
FiniteDimensional.finrank R (DirectSum ι fun i => M i) =
Finset.univ.sum fun i => FiniteDimensional.finrank R (M i)
This theorem states that for a given ring `R` with a strong rank condition, and for a finite set `ι` of types, if each type `M i` is an additive commutative group and a `R`-module that is free and finite, then the rank of the direct sum of these modules (notated as `DirectSum ι fun i => M i`) is equal to the sum of the ranks of each individual module `M i`, where the sum is taken over all elements in the universal finite set of the types `ι`. In other words, the dimension of the direct sum of a family of vector spaces is the sum of the dimensions of the vector spaces.
More concisely: For a ring `R` with strong rank condition and a finite family `ι` of free and finite rank `R`-modules `M i` that are additive commutative groups, the rank of the direct sum of these modules equals the sum of their individual ranks.
|
rank_prod'
theorem rank_prod' :
∀ {R : Type u} {M M₁ : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₁]
[inst_3 : Module R M] [inst_4 : Module R M₁] [inst_5 : StrongRankCondition R] [inst_6 : Module.Free R M]
[inst_7 : Module.Free R M₁], Module.rank R (M × M₁) = Module.rank R M + Module.rank R M₁
The theorem `rank_prod'` states that for any ring `R` and any two free modules `M` and `M₁` over `R` (that lie in the same universe), the rank of the product module `M × M₁` is equal to the sum of the ranks of `M` and `M₁`. Here, "rank" refers to the size of a basis for a module, and "free" means the module has a basis. This is under the assumption of the Strong Rank Condition, which says that every surjective endomorphism of a finitely generated module is an isomorphism.
More concisely: Under the Strong Rank Condition, the rank of the product of two free modules over a ring is equal to the sum of their individual ranks.
|
rank_directSum
theorem rank_directSum :
∀ (R : Type u) [inst : Ring R] [inst_1 : StrongRankCondition R] {ι : Type v} (M : ι → Type w)
[inst_2 : (i : ι) → AddCommGroup (M i)] [inst_3 : (i : ι) → Module R (M i)]
[inst_4 : ∀ (i : ι), Module.Free R (M i)],
Module.rank R (DirectSum ι fun i => M i) = Cardinal.sum fun i => Module.rank R (M i)
The theorem `rank_directSum` states that for any type `R` with a ring structure and a strong rank condition, and an indexed type `M` where each `M i` is an additive commutative group and a module over `R` and is free as a `R`-module, the rank of the direct sum of the `M i`s (denoted as `DirectSum ι fun i => M i`) equals the sum of the ranks of each `M i`. In simpler terms, it means that the rank (the cardinality of a basis) of a direct sum of modules equals the sum of the ranks of the individual modules.
More concisely: For any indexed family of free modules over a ring with a strong rank condition, the rank of their direct sum equals the sum of the ranks of the individual modules.
|
rank_prod
theorem rank_prod :
∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M']
[inst_3 : Module R M] [inst_4 : Module R M'] [inst_5 : StrongRankCondition R] [inst_6 : Module.Free R M]
[inst_7 : Module.Free R M'],
Module.rank R (M × M') = Cardinal.lift.{v', v} (Module.rank R M) + Cardinal.lift.{v, v'} (Module.rank R M')
The theorem `rank_prod` states that for any ring `R` and for any two modules `M` and `M'` over `R`, if both `M` and `M'` are free modules, then the rank of the direct product module `M × M'` is the sum of the lifted ranks of `M` and `M'`. Here, the `Cardinal.lift` operation implies that we lift the rank of the modules to the max of the universes in which `M` and `M'` reside. The `StrongRankCondition` ensures that the ring `R` satisfies certain properties related to the rank of its modules.
More concisely: For free modules M and M' over a ring R satisfying the StrongRankCondition, the rank of their direct product is the sum of their lifted ranks.
|
rank_matrix''
theorem rank_matrix'' :
∀ (R : Type u) [inst : Ring R] [inst_1 : StrongRankCondition R] (m n : Type u) [inst_2 : Finite m]
[inst_3 : Finite n], Module.rank R (Matrix m n R) = Cardinal.mk m * Cardinal.mk n
This theorem states that for any ring `R`, if `m` and `n` are finite types that are in the same universe as `R`, then the rank of `m × n` matrices with entries in `R`, denoted as `Module.rank R (Matrix m n R)`, is equal to the product of the cardinalities of `m` and `n`, represented as `Cardinal.mk m * Cardinal.mk n`. This is under the assumption that `R` satisfies the `StrongRankCondition`. In essence, it is saying that the rank of a matrix is determined by the product of the sizes of its row and column index sets, given certain conditions on the ring of its entries.
More concisely: Given a ring `R` satisfying the StrongRankCondition, the rank of a matrix of size `m × n` over `R` equals the product of the cardinalities of `m` and `n`.
|