fieldRange_of_normal — Mathlib

English

For a normal base, lifting an algebra homomorphism commutes with evaluation at elements of the domain.

Русский

Для нормального основания поднятие алгебра-гомоморфа коммутирует со сведением по элементам области.

LaTeX

$$χ.liftNormal E (algebraMap K₁ E x) = algebraMap K₂ E (χ x)$$

Lean4

theorem fieldRange_of_normal {E : IntermediateField F K} [Normal F E] (f : E →ₐ[F] K) : f.fieldRange = E :=
  by
  let g := f.restrictNormal' E
  rw [← show E.val.comp ↑g = f from DFunLike.ext_iff.mpr (f.restrictNormal_commutes E), ← AlgHom.map_fieldRange,
    AlgEquiv.fieldRange_eq_top g, ← AlgHom.fieldRange_eq_map, IntermediateField.fieldRange_val]

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