iterateFrobeniusₛₗ_algebraMap_base

English

For a ∈ F, iterating Frobenius on the bottom extension and then mapping along F ⊆ L yields the p^n-th power of the image of a in L, matching the two algebra embeddings.

Русский

Пусть a ∈ F. Тогда применение Фробениуса к нижнему полю и последующее отображение по F ⊆ L дают a^{p^n} в L через соответствующие вложения.

LaTeX

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

Lean4

/-- Action of `iterateFrobeniusₛₗ` on the base field. -/
theorem iterateFrobeniusₛₗ_algebraMap_base {n : ℕ} (hn : exponent K L ≤ n) (a : F) :
    iterateFrobeniusₛₗ F K L p hn (algebraMap F L a) = (algebraMap F K a) ^ p ^ n :=
  by
  apply (algebraMap K L).injective
  rw [← map_pow, ← IsScalarTower.algebraMap_apply, map_pow, algebraMap_iterateFrobeniusₛₗ F K L p hn]

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