English
If E2 is algebraic over K, the compositum of E1 and E2 as intermediate fields has the same subalgebra as the join of their subalgebras: (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra.
Русский
Если E2 алгебраическое над K, композиция E1 и E2 как промежуточных полей имеет ту же подалгебру, что и их объединение подалгебр: (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra.
LaTeX
$$$(E_1 \sqcup E_2)^{\text{toSubalgebra}} = E_1^{\text{toSubalgebra}} \sqcup E_2^{\text{toSubalgebra}} \quad\text{under } \ Algebra.IsAlgebraic K E_2$$$
Lean4
theorem sup_toSubalgebra_of_isAlgebraic_right [Algebra.IsAlgebraic K E2] :
(E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra :=
by
have : (adjoin E1 (E2 : Set L)).toSubalgebra = _ :=
adjoin_algebraic_toSubalgebra fun x h ↦
IsAlgebraic.tower_top E1 (isAlgebraic_iff.1 (Algebra.IsAlgebraic.isAlgebraic (⟨x, h⟩ : E2)))
apply_fun Subalgebra.restrictScalars K at this
rw [← restrictScalars_toSubalgebra, restrictScalars_adjoin] at this
simp only [← coe_type_toSubalgebra] at this
rw [Algebra.restrictScalars_adjoin] at this
exact this
