normalClosure_map_eq — Mathlib

English

For any σ: L ≃ₐ[F] L, normalClosure F (K.map σ) L = normalClosure F K L.

Русский

Для любого σ: L ≃ₐ[F] L выполняется равенство normalClosure F (K.map σ) L = normalClosure F K L.

LaTeX

$$$\operatorname{normalClosure} F (K^{\sigma}) L = \operatorname{normalClosure} F K L$$$

Lean4

@[simp]
theorem normalClosure_map_eq (K : IntermediateField F L) (σ : L →ₐ[F] L) :
    normalClosure F (K.map σ) L = normalClosure F K L :=
  by
  have (σ : L ≃ₐ[F] L) : normalClosure F (K.map (σ : L →ₐ[F] L)) L = normalClosure F K L :=
    by
    simp_rw [normalClosure_def'', map_map]
    exact (Equiv.mulRight σ).iSup_congr fun _ ↦ rfl
  exact this ((Algebra.IsAlgebraic.algEquivEquivAlgHom _ _).symm σ)

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