map_closure — Mathlib

English

The image under a ring homomorphism of the subring generated by a set s equals the subring generated by the image of s.

Русский

Образ подкольца, порождаемого множества s, под действием гомоморфизма равен подкольцу, порождаемому образами элементов s.

LaTeX

$$$ (\\mathrm{closure}\\; s).\\mathrm{map} f = \\mathrm{closure}(f''s) $$$

Lean4

/-- The image under a ring homomorphism of the subring generated by a set equals
the subring generated by the image of the set. -/
theorem map_closure (f : R →+* S) (s : Set R) : (closure s).map f = closure (f '' s) :=
  Set.image_preimage.l_comm_of_u_comm (gc_map_comap f) (Subring.gi S).gc (Subring.gi R).gc fun _ ↦ rfl

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