Commit 2024-02-06 18:38 d172b397

feat(FieldTheory/PurelyInseparable): definition and basic results of purely inseparable extensions (#9488) Main defintions:

• IsPurelyInseparable: typeclass for purely inseparable field extension: an algebraic extension E / F is purely inseparable if and only if the minimal polynomial of every element of E ∖ F is not separable. Main results (not exhaustive):
• isPurelyInseparable_iff_mem_pow: a field extension E / F of exponential characteristic q is purely inseparable if and only if for every element x of E, there exists a natural number n such that x ^ (q ^ n) is contained in F.
• IsPurelyInseparable.trans: if E / F and K / E are both purely inseparable extensions, then K / F is also purely inseparable.
• isPurelyInseparable_iff_natSepDegree_eq_one: E / F is purely inseparable if and only if for every element x of E, its minimal polynomial has separable degree one.
• isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C: a field extension E / F of exponential characteristic q is purely inseparable if and only if for every element x of E, the minimal polynomial of x over F is of form X ^ (q ^ n) - y for some natural number n and some element y of F.
• isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow: a field extension E / F of exponential characteristic q is purely inseparable if and only if for every element x of E, the minimal polynomial of x over F is of form (X - x) ^ (q ^ n) for some natural number n.
• isPurelyInseparable_iff_finSepDegree_eq_one: an algebraic extension is purely inseparable if and only if it has (finite) separable degree one. TODO: remove the algebraic assumption. (will be in later PR)
• IsPurelyInseparable.normal: a purely inseparable extension is normal.
• separableClosure.isPurelyInseparable: if E / F is algebraic, then E is purely inseparable over the (relative) separable closure of E / F.
• IsPurelyInseparable.injective_comp_algebraMap: if E / F is purely inseparable, then for any reduced ring L, the map (E →+* L) → (F →+* L) induced by algebraMap F E is injective. In other words, a purely inseparable field extension is an epimorphism in the category of fields.
• isPurelyInseparable_adjoin_iff_mem_pow: if F is of exponential characteristic q, then F(S) / F is a purely inseparable extension if and only if for any x ∈ S, x ^ (q ^ n) is contained in F for some n : ℕ.
• Field.finSepDegree_eq: if E / F is algebraic, then the Field.finSepDegree F E is equal to Field.sepDegree F E as a natural number. This means that the cardinality of Field.Emb F E and the degree of (separableClosure F E) / F are both finite or infinite, and when they are finite, they coincide. TODO: (will be in later PR)
• IsPurelyInseparable.of_injective_comp_algebraMap: if L is an algebraically closed field containing E, such that the map (E →+* L) → (F →+* L) induced by algebraMap F E is injective, then E / F is purely inseparable. In other words, epimorphisms in the category of fields must be purely inseparable extensions. Need to use the fact that Emb F E is infintie when E / F is (purely) transcendental.
• Prove that the (infinite) inseparable degree are multiplicative; linearly disjoint argument is needed.