map — Mathlib

English

Under a scalar tower, splitting fields commute with base change: if f ∈ F[X] and you map scalars K → F → L, f becomes a splitting field over L.

Русский

В рамках торового расслоения разложение сохраняется при изменении оснований.

LaTeX

$$$[IsScalarTower F K L] \Rightarrow \mathrm{IsSplittingField}(K,L,\mathrm{mapAlg}_{F\to K}(f))$$$

Lean4

instance map (f : F[X]) [IsSplittingField F L f] : IsSplittingField K L (f.map <| algebraMap F K) :=
  ⟨by rw [splits_map_iff, ← IsScalarTower.algebraMap_eq]; exact splits L f,
    Subalgebra.restrictScalars_injective F <|
      by
      rw [rootSet, aroots, map_map, ← IsScalarTower.algebraMap_eq, Subalgebra.restrictScalars_top, eq_top_iff, ←
        adjoin_rootSet L f, Algebra.adjoin_le_iff]
      exact fun x hx => @Algebra.subset_adjoin K _ _ _ _ _ _ hx⟩

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