# Commit 2023-11-18 00:38 b6646ed1

View on Github →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`

.