isAlgebraic_field — Mathlib

English

In a field context, the adjoin of the range of a transcendence basis is algebraic over the ambient field.

Русский

В контексте поля адъюнкт диапазона базиса трансцендентности есть алгебраически над базовым полем.

LaTeX

$$$ Algebra.IsAlgebraic (adjoin F (range x)) E$$$

Lean4

theorem isAlgebraic_field {F E : Type*} {x : ι → E} [Field F] [Field E] [Algebra F E] (hx : IsTranscendenceBasis F x) :
    Algebra.IsAlgebraic (IntermediateField.adjoin F (range x)) E :=
  by
  haveI := hx.isAlgebraic
  set S := range x
  letI : Algebra (adjoin F S) (IntermediateField.adjoin F S) :=
    (Subalgebra.inclusion (IntermediateField.algebra_adjoin_le_adjoin F S)).toRingHom.toAlgebra
  haveI : IsScalarTower (adjoin F S) (IntermediateField.adjoin F S) E := IsScalarTower.of_algebraMap_eq (congrFun rfl)
  exact Algebra.IsAlgebraic.extendScalars (R := adjoin F S) (Subalgebra.inclusion_injective _)

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