Theorems · Definition · field theory

Field.embEquivOfAdjoinSplits

(F : Type u) →
  (E : Type v) →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          (K : Type w) →
            [inst_3 : Field K] →
              [inst_4 : Algebra F K] →
                {S : Set E} →
                  IntermediateField.adjoin F S = ⊤ →
                    (∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) →
                      Field.Emb F E ≃ (E →ₐ[F] K)

A random bijection between Field.Emb F E and E →ₐ[F] K if E = F(S) such that every element s of S is integral (= algebraic) over F and whose minimal polynomial splits in K. Combined with Field.instInhabitedEmb, it can be viewed as a stronger version of IntermediateField.nonempty_algHom_of_adjoin_splits.

Defined in

Mathlib.FieldTheory.SeparableDegree

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFieldAlgebra