restrictNormal — Mathlib

English

There is a canonical F-algebra endomorphism of E obtained by restricting a given F-algebra homomorphism, provided E is Normal over F.

Русский

Существует каноничный F-алгебровый эндоморфизм E, получаемый ограничением данного F-алгебрового гомоморфизма, при условии Normal F E.

LaTeX

$$$\text{RestrictNormal }[\text{Normal } F E]\;: E \to_{F} E,$$$

Lean4

/-- Restrict algebra homomorphism to normal subfield. -/
@[stacks 0BME "Part 1"]
def restrictNormal [Normal F E] : E →ₐ[F] E :=
  ((AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K₂)).symm.toAlgHom.comp (ϕ.restrictNormalAux E)).comp
    (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K₁)).toAlgHom

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