FiniteDimensional.finrank_linearMap_self
theorem FiniteDimensional.finrank_linearMap_self :
∀ (R : Type u) (S : Type u') (M : Type v) [inst : Ring R] [inst_1 : Ring S] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : Module.Free R M] [inst_5 : Module.Finite R M] [inst_6 : StrongRankCondition R]
[inst_7 : StrongRankCondition S] [inst_8 : Module R S] [inst_9 : SMulCommClass R S S],
FiniteDimensional.finrank S (M →ₗ[R] S) = FiniteDimensional.finrank R M
This theorem states that for any types `R`, `S`, and `M`, where `R` and `S` are rings, `M` is an additively commutative group, `M` is a module over `R`, `M` is a free module over `R`, `M` is a finite module over `R`, `R` satisfies the strong rank condition, `S` satisfies the strong rank condition, `S` is a module over `R`, and the scalar multiplication on `S` commutes with `R`, the rank of the space of linear maps from `M` to `S` over the field `S` is equal to the rank of `M` over the field `R`. In other words, the dimension of the vector space of linear transformations from `M` to `S` (considered over the field `S`) is the same as the dimension of the vector space `M` (considered over the field `R`).
More concisely: Given rings `R` and `S`, a finite, free, additively commutative `R`-module `M`, and a commutative `S`-module `S` such that both `R` and `S` satisfy the strong rank condition, the dimension of the space of `S`-linear maps from `M` to `S` equals the dimension of `M` over `R`.
|
FiniteDimensional.finrank_linearMap
theorem FiniteDimensional.finrank_linearMap :
∀ (R : Type u) (S : Type u') (M : Type v) (N : Type w) [inst : Ring R] [inst_1 : Ring S] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : Module.Free R M] [inst_5 : Module.Finite R M] [inst_6 : AddCommGroup N]
[inst_7 : Module R N] [inst_8 : Module S N] [inst_9 : SMulCommClass R S N] [inst_10 : StrongRankCondition R]
[inst_11 : StrongRankCondition S] [inst_12 : Module.Free S N],
FiniteDimensional.finrank S (M →ₗ[R] N) = FiniteDimensional.finrank R M * FiniteDimensional.finrank S N
The theorem `FiniteDimensional.finrank_linearMap` states that for any Rings `R` and `S`, and Modules `M` over `R` and `N` over `S` and `R`, if `M` is a free and finite `R`-module, and `N` is a free `S`-module, and both `R` and `S` satisfy the strong rank condition, then the rank of the set of linear maps from `M` to `N`, when viewed as an `S`-module, is equal to the product of the rank of `M` as an `R`-module and the rank of `N` as an `S`-module. In other words, the dimension of the space of linear maps is the product of the dimensions of the domain and codomain spaces.
More concisely: Given free and finite rank modules M over Rings R and free modules N over S, if R and S satisfy the strong rank condition, then the rank of linear maps from M to N equals the product of the ranks of M and N.
|