le_perfectClosure_iff
theorem le_perfectClosure_iff :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (L : IntermediateField F E),
L ≤ perfectClosure F E ↔ IsPurelyInseparable F ↥L
This theorem states that for any intermediate field `L` of a field extension `E / F`, `L` is contained in the relative perfect closure of `F` in `E` if and only if it is purely inseparable over `F`. In the field theory, the perfect closure of a field `F` in an extension `E` is the largest subfield of `E` which is perfect and contains `F`. A field extension is called purely inseparable if every element in the extension field is purely inseparable over the base field.
More concisely: A field extension `L` of `F` in `E` is contained in the relative perfect closure of `F` in `E` if and only if it is purely inseparable over `F`.
|
isPurelyInseparable_iff
theorem isPurelyInseparable_iff :
∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
IsPurelyInseparable F E ↔ ∀ (x : E), IsIntegral F x ∧ ((minpoly F x).Separable → x ∈ (algebraMap F E).range)
This theorem states that for any two fields `F` and `E` where `E` is an algebra over `F`, `E` is purely inseparable over `F` if and only if for every element `x` of `E`, `x` is integral over `F`, and if the minimal polynomial of `x` over `F` is separable, then `x` is in the image of the algebra homomorphism from `F` to `E`. Here, an element being integral means it's a root of some monic polynomial from `F`, and a polynomial is separable if it is coprime with its derivative.
More concisely: A field extension `E` over `F` is purely inseparable if and only if every element of `E` is integral over `F` and lies in the image of the algebra homomorphism from `F` to `E`, with integrality implying separability of the minimal polynomial.
|
IsPurelyInseparable.inseparable
theorem IsPurelyInseparable.inseparable :
∀ (F : Type u) {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
[inst_3 : IsPurelyInseparable F E] (x : E), (minpoly F x).Separable → x ∈ (algebraMap F E).range
The theorem `IsPurelyInseparable.inseparable` states that for any field `F`, and a field `E` that is a purely inseparable extension of `F` with an algebra structure over `F`, and any element `x` from `E`, if the minimal polynomial of `x` over `F` is separable (which means it is coprime with its derivative), then `x` lies in the range of the ring homomorphism given by the algebra structure from `F` to `E`. In other words, if an element in a purely inseparable extension field has a separable minimal polynomial, it can be mapped from the base field via the algebra structure's ring homomorphism.
More concisely: If `F` is a field, `E` is a purely inseparable extension of `F` as an `F`-algebra, and `x` is an element of `E` with separable minimal polynomial over `F`, then `x` lies in the image of the `F`-algebra homomorphism from `F` to `E`.
|
isPurelyInseparable_iff_pow_mem
theorem isPurelyInseparable_iff_pow_mem :
∀ (F : Type u) {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ)
[inst_3 : ExpChar F q], IsPurelyInseparable F E ↔ ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
The theorem `isPurelyInseparable_iff_pow_mem` states that for any field `F` and field extension `E` endowed with an `Algebra` structure from `F` to `E`, and a given exponential characteristic `q`, the extension `E / F` is purely inseparable if and only if for every element `x` in `E`, there exists a natural number `n` such that the `q^n`-th power of `x` belongs to the range of the ring homomorphism induced by the `Algebra` structure from `F` to `E`. In other words, an element `x` of `E` raised to the power of `q` to the `n`th is in the image of the map from `F` to `E`. Here, `q` is a natural number representing the exponential characteristic of the field `F`.
More concisely: For a field extension endowed with an algebra structure, an extension is purely inseparable if and only if every element in the extension raises to a power in its image under the induced homomorphism for some natural number, equivalent to the exponential characteristic of the base field.
|