Frobenius map for field extensions with exponent

Stream: mathlib4

[Michał Staromiejski]

Now that we have the exponent of a field extension L / K in mathlib (#21372), I'd like to add a version of the iterated Frobenius map that goes from L to K, both as a ring homomorphism and a semilinear map (over iterated Frobenius in K).
I suggest to define it with extra condition that the power is greater or equal the exponent for the extension:

import Mathlib.FieldTheory.PurelyInseparable.Exponent

section RingHom

variable [Field K] [Field L] [Algebra K L] [HasExponent K L]

/-- Iterated Frobenius map for purely inseparable field extension with exponent.
If `s ≥ exponent K L`, it acts like `x ↦ x ^ ringExpChar K ^ s` but the codomain
is the base field `K`. -/
noncomputable def iterateFrobenius_fun (s : ℕ) : L → K :=
  fun a ↦ elemReduct K a ^ ringExpChar K ^ (s - elemExponent K a)

/-- Iterated Frobenius ring homomorphism for purely inseparable field extension with exponent. -/
noncomputable def iterateFrobenius_ringHom {s : ℕ} (hs : exponent K L ≤ s) : L →+* K where
  toFun := iteratedFrobenius' K L s
  ...

end RingHom

section Semilinear

variable (F K L : Type*) [Field F] [Field K] [Field L]
variable [Algebra F K] [Algebra K L] [Algebra F L] [IsScalarTower F K L] [HasExponent K L]

/-- Iterated Frobenius as a semilinear map over `F` wrt iterated Frobenius map. -/
noncomputable def iteratedFrobeniusₛₗ {s : ℕ} (hs : exponent K L ≤ s) :
    L →ₛₗ[iterateFrobenius F (ringExpChar F) s] K where
  __ := iteratedFrobenius K L hs
  map_smul' r a := ...
...

end Semilinear

I tried also the approach with {s : ℕ} being "the extra" over exponent K L (so the action is a ^ p ^ (exponent K L + s)) but this leads to problems with defeqs (imagine two such semilinear maps for different exponents with "balancing" s₁ and s₂ so that the exponent of the underlying ring homomorphism is the same but not defeq, then it is hard to for example add such maps).
Any thoughts and suggestions (also regarding naming and namespaces) are highly welcome!

[Michał Staromiejski]

I'd hear some suggestions especially for naming/namespaces to differentiate from the "regular" iterateFrobenius.

[Michał Staromiejski]

Created #22673.