English
Let f: R → S be an injective ring homomorphism and let {s_i} be a nonempty family of subrings of R indexed by i. Then f maps the infimum of the family to the infimum of the images: f( ⋂_i s_i ) = ⋂_i f(s_i).
Русский
Пусть f: R → S — инъективное гомоморфизм колец, и пусть {s_i} — непустая семейство подкольц под R, индексированное i. Тогда образ инфимума семейства равен инфимума образов: f(⋂_i s_i) = ⋂_i f(s_i).
LaTeX
$$$ ( \inf_i s_i ).map f = \inf_i ( s_i ).map f $$$
Lean4
theorem map_iInf {ι : Sort*} [Nonempty ι] (f : R →+* S) (hf : Function.Injective f) (s : ι → Subring R) :
(iInf s).map f = ⨅ i, (s i).map f := by
apply SetLike.coe_injective
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)
