English
Let f be an R-algebra homomorphism from A to B. Then the subalgebra generated by the image of s equals the image of the subalgebra generated by s: adjoin_R(f''s) = (adjoin_R s).map f.
Русский
Пусть f — алгебра-гомоморфизм из A в B. Тогда порождающая единичная над изображением s равна образу порождающей над s: adjoin_R(f''s) = (adjoin_R s).map f.
LaTeX
$$$\\operatorname{adjoin}_R(f''s) = (\\operatorname{adjoin}_R s).map f$$$
Lean4
theorem adjoin_image (f : A →ₐ[R] B) (s : Set A) : adjoin R (f '' s) = (adjoin R s).map f :=
le_antisymm (adjoin_le <| Set.image_mono subset_adjoin) <|
Subalgebra.map_le.2 <|
adjoin_le <|
Set.image_subset_iff.1 <|
by
simp only [Set.image_id', coe_carrier_toSubmonoid, Subalgebra.coe_toSubsemiring, Subalgebra.coe_comap]
exact fun x hx => subset_adjoin ⟨x, hx, rfl⟩
