English
Assuming a tower of fields with Frobenius exponent conditions, there is a solvability transfer: if F–K1 is normal and AlgEquiv solvable, then E ≃ₐ[F] E is solvable.
Русский
При наличии башни полей с условиями степени Фробениуса выполняется перенос разрешимости: если F-K1 нормальное, а AlgEquiv разрешимы, то E ≃ₐ[F] E разрешимо.
LaTeX
$$$IsSolvable (AlgEquiv F E E)$$$
Lean4
/-- Version of `iterateFrobenius` as a semilinear map over a subfield `F` of `K`, w.r.t. the
iterated Frobenius homomorphism on `F`. -/
noncomputable def iterateFrobeniusₛₗ {n : ℕ} (hn : exponent K L ≤ n) : L →ₛₗ[_root_.iterateFrobenius F p n] K
where
__ := iterateFrobenius K L p hn
map_smul' r
a := by
dsimp [iterateFrobenius]
rw [Algebra.smul_def _ (iterateFrobeniusAux K L p n a)]
apply (algebraMap K L).injective
rw [(algebraMap K L).map_mul, ← IsScalarTower.algebraMap_apply, algebraMap_iterateFrobeniusAux K p hn a,
algebraMap_iterateFrobeniusAux K p hn (r • a), iterateFrobenius_def, map_pow, Algebra.smul_def, mul_pow]
