extendScalars_adjoin — Mathlib

English

If K ≤ adjoin F S, then extending scalars along F to the intermediate field yields the adjoin of K and S over F: extendScalars(h) = adjoin K S.

Русский

Если K ⊆ adjoin_F S, то расширение скаляров даёт adjoin_K S: extendScalars(h) = adjoin_K S.

LaTeX

$$$\\\\operatorname{extendScalars} h = \\\\operatorname{adjoin} K S.$$$

Lean4

theorem extendScalars_adjoin {K : IntermediateField F E} {S : Set E} (h : K ≤ adjoin F S) :
    extendScalars h = adjoin K S :=
  restrictScalars_injective F <|
    by
    rw [extendScalars_restrictScalars, restrictScalars_adjoin]
    exact
      le_antisymm (adjoin.mono F S _ Set.subset_union_right) <|
        adjoin_le_iff.2 <| Set.union_subset h (subset_adjoin F S)

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