English
If K1 is a normal extension of F and both K1 and E are solvable in the sense of algebra isomorphisms, then E ≃ₐ[F] E is solvable; i.e., the algebra automorphism group of E over F is solvable.
Русский
Если K1 — нормальное расширение F, и соответствующие алгебраические группы из AlgEquiv являются разрешимыми, тогда AlgEquiv(F,E) — разрешимы.
LaTeX
$$$IsSolvable (AlgEquiv F E E)$$$
Lean4
theorem isSolvable_of_isScalarTower [Normal F K₁] [h1 : IsSolvable (K₁ ≃ₐ[F] K₁)] [h2 : IsSolvable (E ≃ₐ[K₁] E)] :
IsSolvable (E ≃ₐ[F] E) :=
by
let f : (E ≃ₐ[K₁] E) →* E ≃ₐ[F] E :=
{ toFun := fun ϕ =>
AlgEquiv.ofAlgHom (ϕ.toAlgHom.restrictScalars F) (ϕ.symm.toAlgHom.restrictScalars F)
(AlgHom.ext fun x => ϕ.apply_symm_apply x) (AlgHom.ext fun x => ϕ.symm_apply_apply x)
map_one' := AlgEquiv.ext fun _ => rfl
map_mul' := fun _ _ => AlgEquiv.ext fun _ => rfl }
refine
solvable_of_ker_le_range f (AlgEquiv.restrictNormalHom K₁) fun ϕ hϕ =>
⟨{ ϕ with commutes' := fun x => ?_ }, AlgEquiv.ext fun _ => rfl⟩
exact Eq.trans (ϕ.restrictNormal_commutes K₁ x).symm (congr_arg _ (AlgEquiv.ext_iff.mp hϕ x))
