English
Adjoin of the union of algebraMap images equals the adjoin of adjoin with a restriction of scalars, i.e., adjoin R (image of s under algebraMap S A union t) = adjoin (adjoin R s) t, restricted to R.
Русский
Совокупность ADJ в образах algebraMap суммы s и t равна adjoin (adjoin R s) t с ограничением скаляров.
LaTeX
$$$ adjoin\ R (algebraMap S A '' s \cup t) = (adjoin (adjoin R s) t).restrictScalars R $$$
Lean4
theorem adjoin_algebraMap_image_union_eq_adjoin_adjoin (s : Set S) (t : Set A) :
adjoin R (algebraMap S A '' s ∪ t) = (adjoin (adjoin R s) t).restrictScalars R :=
le_antisymm
(closure_mono <|
Set.union_subset
(Set.range_subset_iff.2 fun r =>
Or.inl ⟨algebraMap R (adjoin R s) r, (IsScalarTower.algebraMap_apply _ _ _ _).symm⟩)
(Set.union_subset_union_left _ fun _ ⟨_x, hx, hxs⟩ => hxs ▸ ⟨⟨_, subset_adjoin hx⟩, rfl⟩))
(closure_le.2 <|
Set.union_subset
(Set.range_subset_iff.2 fun x =>
adjoin_mono Set.subset_union_left <| Algebra.adjoin_algebraMap R A s ▸ ⟨x, x.prop, rfl⟩)
(Set.Subset.trans Set.subset_union_right subset_adjoin))
