Theorems · Definition · field theory

IntermediateField.algHomEquivAlgHomOfSplits

{F : Type u_1} →
  {K : Type u_2} →
    (A : Type u_3) →
      [inst : Field F] →
        [inst_1 : Field K] →
          [inst_2 : Field A] →
            [inst_3 : Algebra F K] →
              [inst_4 : Algebra F A] →
                [Algebra.IsAlgebraic F K] →
                  (L : IntermediateField F A) →
                    (∀ (x : K), (Polynomial.map (algebraMap F ↥L) (minpoly F x)).Splits) → (K →ₐ[F] ↥L) ≃ (K →ₐ[F] A)

All F-embeddings of a field K into another field A factor through any intermediate field of A/F in which the minimal polynomial of elements of K splits.

Defined in

Mathlib.FieldTheory.IsAlgClosed.Basic

Cited by

3 results in Mathlib

Foundations

Depth 146 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldFieldAlgebraAlgebraAlgebra.IsAlgebraic