Adjoining elements to a field #
Some lemmas on the ring generated by adjoining an element to a field.
Main statements #
lift_of_splits
: IfK
andL
are field extensions ofF
and we haves : Finset K
such that the minimal polynomial of eachx ∈ s
splits inL
thenAlgebra.adjoin F s
embeds inL
.
def
AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly
(F : Type u_1)
[Field F]
{R : Type u_2}
[CommRing R]
[Algebra F R]
(x : R)
:
↥(Algebra.adjoin F {x}) ≃ₐ[F] AdjoinRoot (minpoly F x)
If p
is the minimal polynomial of a
over F
then F[a] ≃ₐ[F] F[x]/(p)
Equations
Instances For
noncomputable def
Algebra.adjoin.liftSingleton
(F : Type u_1)
[Field F]
{S : Type u_2}
{T : Type u_3}
[CommRing S]
[CommRing T]
[Algebra F S]
[Algebra F T]
(x : S)
(y : T)
(h : (Polynomial.aeval y) (minpoly F x) = 0)
:
↥(Algebra.adjoin F {x}) →ₐ[F] T
Produce an algebra homomorphism Adjoin R {x} →ₐ[R] T
sending x
to
a root of x
's minimal polynomial in T
.
Equations
- Algebra.adjoin.liftSingleton F x y h = (AdjoinRoot.liftHom (minpoly F x) y h).comp ↑(AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly F x)
Instances For
theorem
Polynomial.lift_of_splits
{F : Type u_2}
{K : Type u_3}
{L : Type u_4}
[Field F]
[Field K]
[Field L]
[Algebra F K]
[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)
If K
and L
are field extensions of F
and we have s : Finset K
such that
the minimal polynomial of each x ∈ s
splits in L
then Algebra.adjoin F s
embeds in L
.
theorem
IsIntegral.mem_range_algHom_of_minpoly_splits
{R : Type u_1}
{K : Type u_2}
{L : Type u_3}
[CommRing R]
[Field K]
[Field L]
[Algebra R K]
[Algebra R L]
{x : L}
(int : IsIntegral R x)
(h : Polynomial.Splits (algebraMap R K) (minpoly R x))
(f : K →ₐ[R] L)
:
x ∈ f.range
theorem
IsIntegral.mem_range_algebraMap_of_minpoly_splits
{R : Type u_1}
{K : Type u_2}
{L : Type u_3}
[CommRing R]
[Field K]
[Field L]
[Algebra R K]
[Algebra R L]
{x : L}
(int : IsIntegral R x)
(h : Polynomial.Splits (algebraMap R K) (minpoly R x))
[Algebra K L]
[IsScalarTower R K L]
:
x ∈ (algebraMap K L).range
theorem
IsIntegral.minpoly_splits_tower_top'
{R : Type u_1}
{K : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[Field K]
[Field L]
[CommRing M]
[Algebra R K]
[Algebra R M]
[Algebra K M]
[IsScalarTower R K M]
{x : M}
(int : IsIntegral R x)
{f : K →+* L}
(h : Polynomial.Splits (f.comp (algebraMap R K)) (minpoly R x))
:
Polynomial.Splits f (minpoly K x)
theorem
IsIntegral.minpoly_splits_tower_top
{R : Type u_1}
{K : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[Field K]
[Field L]
[CommRing M]
[Algebra R K]
[Algebra R L]
[Algebra R M]
[Algebra K M]
[IsScalarTower R K M]
{x : M}
(int : IsIntegral R x)
[Algebra K L]
[IsScalarTower R K L]
(h : Polynomial.Splits (algebraMap R L) (minpoly R x))
:
Polynomial.Splits (algebraMap K L) (minpoly K x)
theorem
Subalgebra.adjoin_rank_le
{F : Type u_5}
(E : Type u_6)
{K : Type u_7}
[CommRing F]
[StrongRankCondition F]
[CommRing E]
[StrongRankCondition E]
[Ring K]
[SMul F E]
[Algebra E K]
[Algebra F K]
[IsScalarTower F E K]
(L : Subalgebra F K)
[Module.Free F ↥L]
:
Module.rank E ↥(Algebra.adjoin E ↑L) ≤ Module.rank F ↥L
If K / E / F
is a ring extension tower, L
is a subalgebra of K / F
,
then [E[L] : E] ≤ [L : F]
.