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.

noncomputable def AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly (F : Type u_1) [Field F] {R : Type u_2} [CommRing R] [Algebra F R] (x : R) : ↥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

@[simp]

theorem AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly_symm_toAlgHom (F : Type u_1) [Field F] {R : Type u_2} [CommRing R] [Algebra F R] (x : R) : ↑(adjoinSingletonEquivAdjoinRootMinpoly F x).symm = AdjoinRoot.Minpoly.toAdjoin F x

@[simp]

theorem AlgEquiv.coe_adjoinSingletonEquivAdjoinRootMinpoly_symm (F : Type u_1) [Field F] {R : Type u_2} [CommRing R] [Algebra F R] (x : R) : ⇑(adjoinSingletonEquivAdjoinRootMinpoly F x).symm = ⇑(AdjoinRoot.Minpoly.toAdjoin F x)

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) : ↥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.liftAlgHom (minpoly F x) (Algebra.ofId F T) 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 ∧ (map (algebraMap F L) (minpoly F x)).Splits) → 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.map (algebraMap R K) (minpoly R x)).Splits) (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.map (algebraMap R K) (minpoly R x)).Splits) : x ∈ (algebraMap K L).range

theorem minpoly_neg_splits {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] {x : L} (g : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits) : (Polynomial.map (algebraMap K L) (minpoly K (-x))).Splits

theorem minpoly_add_algebraMap_splits {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] {x : L} (r : K) (g : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits) : (Polynomial.map (algebraMap K L) (minpoly K (x + (algebraMap K L) r))).Splits

theorem minpoly_sub_algebraMap_splits {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] {x : L} (r : K) (g : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits) : (Polynomial.map (algebraMap K L) (minpoly K (x - (algebraMap K L) r))).Splits

theorem minpoly_algebraMap_add_splits {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] {x : L} (r : K) (g : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits) : (Polynomial.map (algebraMap K L) (minpoly K ((algebraMap K L) r + x))).Splits

theorem minpoly_algebraMap_sub_splits {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] {x : L} (r : K) (g : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits) : (Polynomial.map (algebraMap K L) (minpoly K ((algebraMap K L) r - x))).Splits

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.map (f.comp (algebraMap R K)) (minpoly R x)).Splits) : (Polynomial.map f (minpoly K x)).Splits

The RingHom version of IsIntegral.minpoly_splits_tower_top.

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.map (algebraMap R L) (minpoly R x)).Splits) : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits

theorem Subalgebra.adjoin_rank_le {F : Type u_5} (E : Type u_6) {K : Type u_7} [CommSemiring F] [StrongRankCondition F] [CommSemiring E] [StrongRankCondition E] [Semiring 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].