Commit 2023-11-18 00:38 b6646ed1

feat: IsNormalClosure predicate (#8418) Main changes are to the file NormalClosure:

• Introduce predicate IsNormalClosure to characterize normal closures L/F of a field extension K/F by the conditions that every minimal polynomial of an element of K over F splits in L, and that L is generated by roots of such polynomials. (When K/F is not necessarily algebraic, the conditions actually says L/F is a normal closure of the algebraic closure of F in K over F.
• IsNormalClosure.normal: a normal closure is always normal.
• isNormalClosure_iff : if K/F is algebraic, the "generated by roots" condition in IsNormalClosure can be replaced by "generated by images of embeddings". To prove it, we split out the two inclusions in restrictScalars_eq_iSup_adjoin and golf its proof. restrictScalars_eq_iSup_adjoin is renamed to normalClosure_eq_iSup_adjoin as it has nothing to do with restrictScalars.
• IsNormalClosure.lift: a normal closure of K/F embeds into any L/F such that the minpolys of K/F splits in L/F.
• IsNormalClosure.equiv: normal closures are unique up to F-algebra isomorphisms.
• isNormalClosure_normalClosure: normalClosure F K L is a valid normal closure if K/F is algebraic and all minpolys of K/F splits in L/F; in particular, if there is at least one F-embedding of K into L, and L/F is normal.
• Algebra.IsAlgebraic.cardinal_mk_algHom_le_of_splits: if every minpoly of K/F splits in L/F, then L is maximal w.r.t. F-embeddings of K, in the sense that K →ₐ[F] L achieves maximal cardinality. In the file Normal:
• splits_of_mem_adjoin: If a set of algebraic elements in a field extension K/F have minimal polynomials that split in another extension L/F, then all minimal polynomials in the intermediate field generated by the set also split in L/F. This is in preparation for connecting IsNormalClosure and IsSplittingField. In the file IntermediateField:
• Add comap and show it forms a Galois connection with map. In the file FieldTheory/Adjoin:
• Add map_sup/iSup lemmas that follow from the Galois connection, plus an additional convenience lemma. In the file RingTheory/Algebraic: add a lemma AlgHom.isAlgebraic_of_injective.