restrictNormalHom_surjective — Mathlib

English

One can lift an algebra isomorphism between base fields to an isomorphism of the ambient normal extension.

Русский

Можно поднять алгебраическое изоморфизм между базовыми полями до изоморфизма над нормальным расширением.

LaTeX

$$AlgEquiv.liftNormal (E) : E ≃ₐ[F] E$$

Lean4

/-- The group homomorphism given by restricting an algebra isomorphism to a normal subfield
is surjective. -/
theorem restrictNormalHom_surjective [Normal F K₁] [Normal F E] :
    Function.Surjective (AlgEquiv.restrictNormalHom K₁ : (E ≃ₐ[F] E) → K₁ ≃ₐ[F] K₁) := fun χ =>
  ⟨χ.liftNormal E, χ.restrict_liftNormal E⟩

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