eq_restrictScalars_of_isSeparable

English

If E/F is separable, then SeparableClosure F K equals the restriction of scalars of SeparableClosure E K.

Русский

Если E/F сепарабельно, то сепарабельное замыкание F в K равно ограничению скаляров сепарабельного замыкания E в K.

LaTeX

$$$\\mathrm{separableClosure}(F,K) = (\\mathrm{separableClosure}(E,K)).\\mathrm{restrictScalars}(F)$$$

Lean4

/-- If `K / E / F` is a field extension tower, such that `E / F` is separable, then
`separableClosure F K` is equal to `separableClosure E K`. -/
theorem eq_restrictScalars_of_isSeparable [Algebra E K] [IsScalarTower F E K] [Algebra.IsSeparable F E] :
    separableClosure F K = (separableClosure E K).restrictScalars F :=
  (separableClosure.le_restrictScalars F E K).antisymm fun _ h ↦ IsSeparable.of_algebra_isSeparable_of_isSeparable F h

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