Commit 2023-11-18 00:38 b6646ed1View on Github →
feat: IsNormalClosure predicate (#8418) Main changes are to the file NormalClosure:
- Introduce predicate
IsNormalClosureto 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_adjoinand golf its proof.
restrictScalars_eq_iSup_adjoinis renamed to
normalClosure_eq_iSup_adjoinas it has nothing to do with
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.
normalClosure F K Lis 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
Lis maximal w.r.t.
K, in the sense that
K →ₐ[F] Lachieves maximal cardinality. In the file Normal:
splits_of_mem_adjoin: If a set of algebraic elements in a field extension
K/Fhave 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
IsSplittingField. In the file IntermediateField:
comapand show it forms a Galois connection with
map. In the file FieldTheory/Adjoin:
map_sup/iSuplemmas that follow from the Galois connection, plus an additional convenience lemma. In the file RingTheory/Algebraic: add a lemma
modified theorem AlgEquiv.fieldRange_eq_top
modified theorem AlgHom.fieldRange_eq_map
modified theorem AlgHom.fieldRange_eq_top
modified theorem AlgHom.map_fieldRange
modified theorem IntermediateField.biSup_adjoin_simple
modified theorem IntermediateField.map_bot
added theorem IntermediateField.map_iSup
added theorem IntermediateField.map_sup
added theorem isSplittingField_iff_intermediateField
modified theorem AlgHom.fieldRange_le_normalClosure
added theorem Algebra.IsAlgebraic.isNormalClosure_iff
added theorem Algebra.IsAlgebraic.isNormalClosure_normalClosure
added theorem Algebra.IsAlgebraic.normalClosure_le_iSup_adjoin
added theorem IsNormalClosure.normal
deleted theorem normalClosure.restrictScalars_eq_iSup_adjoin
added theorem normalClosure_eq_iSup_adjoin'
added theorem normalClosure_eq_iSup_adjoin