of_restrictScalars — Mathlib

English

If L is an intermediate field K over F, and E is algebraic over F, then (adjoin E (L:Set K)).toSubalgebra = Algebra.adjoin E (L:Set K).

Русский

Если L — промежуточное поле K над F, и E алгебраическое над F, то адъюнкт над E и L равен адъюнкту над E и L как подалгебре.

LaTeX

$$$(\text{adjoin } E (L : Set K)).toSubalgebra = \operatorname{Algebra.adjoin}_E (L : Set K)$$

Lean4

theorem of_restrictScalars {K L E : Type*} [Field K] [Field L] [Field E] [Algebra K L] [Algebra K E] [Algebra L E]
    [IsScalarTower K L E] {E' : IntermediateField L E} (H : (E'.restrictScalars K).FG) : E'.FG :=
  by
  obtain ⟨s, hs⟩ := H
  refine ⟨s, le_antisymm ?_ ?_⟩
  · rw [adjoin_le_iff]
    exact (subset_adjoin K _).trans_eq congr(($hs : Set E))
  · rw [← restrictScalars_le_iff K, ← hs, adjoin_le_iff]
    exact subset_adjoin L _

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