normal_iff_forall_fieldRange_eq — Mathlib

English

Normal F K iff for all AlgEquiv σ: L ≃ₐ[F] L, map σ K = K.

Русский

Normal F K эквивалентно тому, что для любого AlgEquiv σ: L ≃ₐ[F] L выполняется map σ K = K.

LaTeX

$$$\mathrm{Normal} F K \iff \forall \sigma : L \simeq_{F} L,\ \operatorname{map} \sigma K = K$$$

Lean4

/-- If `L/K/F` is a field tower where `L/F` is normal, then
`K` is normal over `F` if and only if `σ(K) = K` for every `σ ∈ K →ₐ[F] L`. -/
@[stacks 09HQ "stronger version replacing an algebraic closure by a normal extension"]
theorem normal_iff_forall_fieldRange_eq : Normal F K ↔ ∀ σ : K →ₐ[F] L, σ.fieldRange = K :=
  ⟨@AlgHom.fieldRange_of_normal (E := K), normal_iff_forall_fieldRange_le.2 ∘ fun h σ ↦ (h σ).le⟩

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