algebra — Mathlib

English

Restricting scalars from the ambient field to F on the range of the canonical algebra map back to normalClosure yields the same normalClosure.

Русский

Ограничение скаляров до F на образе канонического алгебромапа обратно в нормальное замыкание даёт то же самое нормальное замыкание.

LaTeX

$$$(\text{normalClosure}(F,K,L)).fieldRange.restrictScalars F = \text{normalClosure}(F,K,L)$$$

Lean4

noncomputable instance algebra : Algebra K (normalClosure F K L) :=
  IntermediateField.algebra'
    { ⨆ f : K →ₐ[F] L, f.fieldRange with
      algebraMap_mem' := fun r ↦ (toAlgHom F K L).fieldRange_le_normalClosure ⟨r, rfl⟩ }

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