English
If the two subalgebras are finitely generated over the base and their top pieces are FG, then the composed top subalgebra is FG.
Русский
Если две подалгебры конечнопорождены над базой и их верхушки FG, то верхняя подалгебра цепочки также FG.
LaTeX
$$$\\text{top FG} \\rightarrow \\text{FG}$$$
Lean4
theorem adjoin_res_eq_adjoin_res (C D E F : Type*) [CommSemiring C] [CommSemiring D] [CommSemiring E] [CommSemiring F]
[Algebra C D] [Algebra C E] [Algebra C F] [Algebra D F] [Algebra E F] [IsScalarTower C D F] [IsScalarTower C E F]
{S : Set D} {T : Set E} (hS : Algebra.adjoin C S = ⊤) (hT : Algebra.adjoin C T = ⊤) :
(Algebra.adjoin E (algebraMap D F '' S)).restrictScalars C =
(Algebra.adjoin D (algebraMap E F '' T)).restrictScalars C :=
by
rw [adjoin_restrictScalars C E, adjoin_restrictScalars C D, ← hS, ← hT, ← Algebra.adjoin_image, ←
Algebra.adjoin_image, ← AlgHom.coe_toRingHom, ← AlgHom.coe_toRingHom, IsScalarTower.coe_toAlgHom,
IsScalarTower.coe_toAlgHom, ← adjoin_union_eq_adjoin_adjoin, ← adjoin_union_eq_adjoin_adjoin, Set.union_comm]
