FiniteDimensional.left
theorem FiniteDimensional.left :
∀ (F : Type u) (K : Type v) (A : Type w) [inst : DivisionRing F] [inst_1 : DivisionRing 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 : Nontrivial A] [inst_8 : FiniteDimensional F A], FiniteDimensional F K
This theorem states that in a tower of field extensions, denoted as `A / K / F`, if the extension `A / F` is finite then the extension `K / F` is also finite. Here, `A`, `K`, and `F` are types representing the three fields, `DivisionRing F` and `DivisionRing K` are typeclass instances stating that `F` and `K` are division rings, `AddCommGroup A` is a typeclass instance stating that `A` is an additive commutative group, and `Module F K`, `Module K A`, `Module F A` are typeclass instances stating that `K` is a vector space over `F`, `A` is a vector space over `K`, and `A` is a vector space over `F` respectively. The condition `IsScalarTower F K A` requires that the scalar multiplication operations in these vector spaces are compatible. The theorem holds as long as `A` is nontrivial, which is expressed with `Nontrivial A`. The finiteness of `A / F` is expressed with `FiniteDimensional F A`, and the theorem concludes that `K / F` is also finite, expressed with `FiniteDimensional F K`.
More concisely: If `A` is a nontrivial vector space over `F`, `K` is a vector space over `F`, `A` is a finite-dimensional vector space over `F`, and `A` is a finite-dimensional vector space over `K` with compatible scalar multiplications, then `K` is a finite-dimensional vector space over `F`.
|
FiniteDimensional.finrank_linear_map'
theorem FiniteDimensional.finrank_linear_map' :
∀ (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 rings `R` and `S` and an `R`-module `M`, under the conditions that `M` is a free `R`-module, `M` has finite `R`-rank, `R` and `S` satisfy the strong rank condition, `R` acts linearly on `S`, and `R` and `S` commute under scalar multiplication, the `S`-rank of the space of `R`-linear maps from `M` to `S` is equal to the `R`-rank of `M`.
In simpler terms, given certain conditions about the structure and properties of the rings and the module, the dimension of the space of linear transformations from the module to the second ring (when thought of as a vector space over the second ring) is the same as the dimension of the module itself (when thought of as a vector space over the first ring).
More concisely: Given free `R`-modules `M` of finite `R`-rank, rings `R` and `S` satisfying the strong rank condition and commuting under scalar multiplication, the space of `R`-linear maps from `M` to `S` has the same rank as `M`.
|