Adjoining elements to a field

Some lemmas on the ring generated by adjoining an element to a field.

Main statements

• Polynomial.lift_of_splits: 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.

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

• AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly F x = (AlgEquiv.ofBijective (AdjoinRoot.Minpoly.toAdjoin F x) ⋯).symm

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)

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] {x : L} [Algebra R 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] {x : L} [Algebra R L] [Algebra K L] [IsScalarTower R K L] (int : IsIntegral R x) (h : Polynomial.Splits (algebraMap R K) (minpoly R x)) : 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 M] [Algebra K M] [IsScalarTower R K M] {x : M} [Algebra K L] [Algebra R L] [IsScalarTower R K L] (int : IsIntegral R x) (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].