Documentation

Mathlib.RingTheory.Adjoin.Field

Adjoining elements to a field #

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

Main statements #

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
    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) :
      (∀ xs, 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)) :
      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)) :
      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] :

      If K / E / F is a ring extension tower, L is a subalgebra of K / F, then [E[L] : E] ≤ [L : F].