toIntermediateField — Mathlib

English

If S is an algebraic subalgebra of L over K, then S can be endowed with an intermediate field structure inside L/K; i.e., there is a natural IntermediateField K L coming from the algebraic subalgebra S.

Русский

Если S — алгебраическая подалгебра L над K, то S можно снабдить структурой промежуточного поля в L/K; то есть существует соответствующее IntermediateField K L, порождаемое подалгеброй S.

LaTeX

$$$ \operatorname{toSubalgebra}(\operatorname{toIntermediateField}(S,h_S)) = S. $$$$

Lean4

/-- Turn an algebraic subalgebra into an intermediate field, `Subalgebra.IsAlgebraic` version. -/
def toIntermediateField {S : Subalgebra K L} (hS : S.IsAlgebraic) : IntermediateField K L
    where
  toSubalgebra := S
  inv_mem' x hx := Algebra.adjoin_le_iff.mpr (Set.singleton_subset_iff.mpr hx) (hS x hx).isIntegral.inv_mem_adjoin

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