restrict_liftNormal — Mathlib

English

If F ⊆ K₁ ⊆ E is a tower with F-normal K₁, solvability of the automorphism groups propagates up the tower.

Русский

Если F ⊆ K₁ ⊆ E образует торовую структуру с F-нормальностью K₁, то разрешимость групп автоморфизмов переходит вверх по торовой структуре.

LaTeX

$$$\text{IsSolvable} (E \simeq_F E) \Rightarrow \text{IsSolvable}(E \simeq_F E)$$$

Lean4

@[simp]
theorem restrict_liftNormal (ϕ : K₁ →ₐ[F] K₁) [Normal F K₁] [Normal F E] : (ϕ.liftNormal E).restrictNormal K₁ = ϕ :=
  AlgHom.ext fun x =>
    (algebraMap K₁ E).injective (Eq.trans (AlgHom.restrictNormal_commutes _ K₁ x) (ϕ.liftNormal_commutes E x))

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