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.



Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Author: acmepjz

Mathlib.lean

@@ -2133,6 +2133,7 @@ import Mathlib.FieldTheory.Perfect
 import Mathlib.FieldTheory.PerfectClosure
 import Mathlib.FieldTheory.PolynomialGaloisGroup
 import Mathlib.FieldTheory.PrimitiveElement
+import Mathlib.FieldTheory.PurelyInseparable
 import Mathlib.FieldTheory.RatFunc
 import Mathlib.FieldTheory.Separable
 import Mathlib.FieldTheory.SeparableClosure

Mathlib/Algebra/CharP/Reduced.lean

@@ -17,13 +17,21 @@ open Finset
 
 open BigOperators
 
-theorem frobenius_inj (R : Type*) [CommRing R] [IsReduced R] (p : ℕ) [ExpChar R p] :
-    Function.Injective (frobenius R p) := fun x h H => by
+section
+
+variable (R : Type*) [CommRing R] [IsReduced R] (p n : ℕ) [ExpChar R p]
+
+theorem iterateFrobenius_inj : Function.Injective (iterateFrobenius R p n) := fun x y H ↦ by
   rw [← sub_eq_zero] at H ⊢
-  rw [← frobenius_sub] at H
+  simp_rw [iterateFrobenius_def, ← sub_pow_expChar_pow] at H
   exact IsReduced.eq_zero _ ⟨_, H⟩
+
+theorem frobenius_inj : Function.Injective (frobenius R p) :=
+  iterateFrobenius_one (R := R) p ▸ iterateFrobenius_inj R p 1
 #align frobenius_inj frobenius_inj
 
+end
+
 /-- If `ringChar R = 2`, where `R` is a finite reduced commutative ring,
 then every `a : R` is a square. -/
 theorem isSquare_of_charTwo' {R : Type*} [Finite R] [CommRing R] [IsReduced R] [CharP R 2]
@@ -39,12 +47,9 @@ variable {R : Type*} [CommRing R] [IsReduced R]
 @[simp]
 theorem ExpChar.pow_prime_pow_mul_eq_one_iff (p k m : ℕ) [ExpChar R p] (x : R) :
     x ^ (p ^ k * m) = 1 ↔ x ^ m = 1 := by
-  induction' k with k hk
-  · rw [pow_zero, one_mul]
-  · refine' ⟨fun h => _, fun h => _⟩
-    · rw [pow_succ, mul_assoc, pow_mul', ← frobenius_def, ← frobenius_one p] at h
-      exact hk.1 (frobenius_inj R p h)
-    · rw [pow_mul', h, one_pow]
+  rw [pow_mul']
+  convert ← (iterateFrobenius_inj R p k).eq_iff
+  apply map_one
 #align char_p.pow_prime_pow_mul_eq_one_iff ExpChar.pow_prime_pow_mul_eq_one_iff
 
 @[deprecated] alias CharP.pow_prime_pow_mul_eq_one_iff := ExpChar.pow_prime_pow_mul_eq_one_iff