Commit 2024-01-01 07:00 bded32ac

feat(FieldTheory/SeparableClosure): (relative) separable closure (#9338) Main definitions:

• separableClosure: the (relative) separable closure of E / F, or called maximal separable subextension of E / F, is defined to be the intermediate field of E / F consisting of all separable elements.
• Field.sepDegree F E: the (infinite) separable degree [E:F]_s of an algebraic extension E / F of fields, defined to be the degree of separableClosure F E / F.
• Field.insepDegree F E: the (infinite) inseparable degree [E:F]_i of an algebraic extension E / F of fields, defined to be the degree of E / separableClosure F E.
• Field.finInsepDegree F E: the (finite) inseparable degree [E:F]_i of an algebraic extension E / F of fields, defined to be the degree of E / separableClosure F E as a natural number. It is zero if such field extension is not finite. Main results:
• le_separableClosure_iff: an intermediate field of E / F is contained in the (relative) separable closure of E / F if and only if it is separable over F.
• separableClosure.normalClosure_eq_self: the normal closure of the (relative) separable closure of E / F is equal to itself.
• separableClosure.normal: the (relative) separable closure of a normal extension is normal.
• separableClosure.isSepClosure: the (relative) separable closure of a separably closed extension is a separable closure of the base field.
• IntermediateField.isSeparable_adjoin_iff_separable: F(S) / F is a separable extension if and only if all elements of S are separable elements.
• separableClosure.eq_top_iff: the (relative) separable closure of E / F is equal to E if and only if E / F is separable.