Subalgebra.adjoin_rank_le
theorem Subalgebra.adjoin_rank_le :
∀ {F : Type u_5} (E : Type u_6) {K : Type u_7} [inst : CommRing F] [inst_1 : StrongRankCondition F]
[inst_2 : CommRing E] [inst_3 : StrongRankCondition E] [inst_4 : Ring K] [inst_5 : SMul F E]
[inst_6 : Algebra E K] [inst_7 : Algebra F K] [inst_8 : IsScalarTower F E K] (L : Subalgebra F K)
[inst_9 : Module.Free F ↥L], Module.rank E ↥(Algebra.adjoin E ↑L) ≤ Module.rank F ↥L
This theorem states that if you have a ring extension tower `K / E / F`, and `L` is a subalgebra of `K / F`, then the rank of the subalgebra generated by `E` and `L` over `E` is less than or equal to the rank of `L` over `F`. The rank of a module is a measure of its "size", or more specifically, it is the maximum number of linearly independent elements in the module. This theorem essentially tells us that adding additional structure to a subalgebra (in this case, adjoining `E`) cannot increase the rank beyond that of the original subalgebra over the base field. The term 'StrongRankCondition' refers to the property that every left module has a well-defined rank. The conditions `Module.Free F ↥L` and `IsScalarTower F E K` ensure that `L` is a free module over `F` and that multiplication in the tower respects the algebra structure, respectively.
More concisely: The rank of a subalgebra generated by a free submodule over a base field and elements from a ring extension is less than or equal to the rank of the submodule over the base field.
|
Polynomial.lift_of_splits
theorem Polynomial.lift_of_splits :
∀ {F : Type u_2} {K : Type u_3} {L : Type u_4} [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
[inst_3 : Algebra F K] [inst_4 : Algebra F L] (s : Finset K),
(∀ x ∈ s, IsIntegral F x ∧ Polynomial.Splits (algebraMap F L) (minpoly F x)) →
Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)
The theorem `Polynomial.lift_of_splits` states that for any two field extensions `K` and `L` of a field `F`, and a finite set `s` of elements from `K`, if each element in `s` is integral over `F` and the minimal polynomial of each element splits in field `L`, then there exists an algebra homomorphism from the minimal subalgebra of `K` that includes `s`, to `L`. Here, an element is said to be integral if it is the root of some monic polynomial with coefficients in `F`. A polynomial is said to split in a field if it is zero or all of its irreducible factors have degree 1.
More concisely: Given field extensions K and L of a field F, if every element in the finite set s from K is integral over F and the minimal polynomial of each element in s splits in L, then there exists an algebra homomorphism from the subalgebra of K generated by s into L.
|