algebraMap_iterateFrobeniusₛₗ

English

Let K ⊆ L be fields with L an algebra over K, and suppose exponent(L|K) ≤ n. For a ∈ L, the base-field image of the iterate Frobenius applied to a equals a raised to p^n in L.

Русский

Пусть K ⊆ L — поля, где L является K-расширением, с экспонентой экспоненты над K не более n. Для любого a ∈ L отображение, полученное из применения повторного Фробениуса к a затем переход через алгебраическую карту базового поля, равно a^{p^n} в L.

LaTeX

$$$\operatorname{algebraMap}_{K,L}\bigl(\operatorname{iterateFrobenius}_{F,K,L,p,hn}(a)\bigr) = a^{p^n}$$$

Lean4

/-- Action of `iterateFrobeniusₛₗ` on the top field. -/
theorem algebraMap_iterateFrobeniusₛₗ {n : ℕ} (hn : exponent K L ≤ n) (a : L) :
    algebraMap K L (iterateFrobeniusₛₗ F K L p hn a) = a ^ p ^ n :=
  algebraMap_iterateFrobenius K p hn a

Похожие утверждения