Commit 2023-11-28 15:55 60b5e237

feat(FieldTheory/SeparableDegree): basic definition of separable degree of field extension (#8117) Main changes:

• rename current Mathlib/FieldTheory/SeparableDegree to Mathlib/RingTheory/Polynomial/SeparableDegree and create new Mathlib/FieldTheory/SeparableDegree Main definitions
• Emb F E: the type of F-algebra homomorphisms from E to the algebraic closure of E.
• sepDegree F E: the separable degree of an algebraic extension E / F of fields, defined to be the cardinal of F-algebra homomorphisms from E to the algebraic closure of E. (Mathematically, it should be the algebraic closure of F, but in order to make the type compatible with Module.rank F E, we use the algebraic closure of E.) Note that if E / F is not algebraic, then this definition makes no mathematical sense.
• finSepDegree F E: the separable degree of E / F as a natural number, which is zero if sepDegree F E is not finite. Main results
• embEquivOfEquiv, sepDegree_eq_of_equiv, finSepDegree_eq_of_equiv: a random isomorphism between Emb F E and Emb F E' when E and E' are isomorphic as F-algebras. In particular, they have the same cardinality (so sepDegree and finSepDegree are equal).
• embEquivOfAdjoinSplits', sepDegree_eq_of_adjoin_splits', finSepDegree_eq_of_adjoin_splits': a random isomorphism between 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. In particular, they have the same cardinality.
• embEquivOfIsAlgClosed, sepDegree_eq_of_isAlgClosed, finSepDegree_eq_of_isAlgClosed: a random isomorphism between Emb F E and E →ₐ[F] K when E / F is algebraic and K / F is algebraically closed. In particular, they have the same cardinality.
• embProdEmbOfIsAlgebraic, lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic, sepDegree_mul_sepDegree_of_isAlgebraic, finSepDegree_mul_finSepDegree_of_isAlgebraic: if K / E / F is a field extension tower, such that K / E is algebraic, then there is a non-canonical isomorphism (Emb F E) × (Emb E K) ≃ (Emb F K). In particular, the separable degree satisfies the tower law: [E:F]_s [K:E]_s = [K:F]_s.