English
Let R,S be nonunital rings and f an injective homomorphism from R to S. For any indexed family (S_i) of NonUnitalSubring of R, the image under f of the infimum of the family equals the infimum of the images: f( iInf_i S_i ) = iInf_i ( S_i.map f ).
Русский
Пусть R, S — некоторые кольца без единицы, и f — инъективный однозначный гомоморфизм R → S. Для любой индексированной семейства (S_i) подполь кольца R имеем: образ f от наименьшего (по включению) пересечения всех S_i равен наименьшему пересечению образов S_i под f: f( iInf_i S_i ) = iInf_i ( S_i.map f ).
LaTeX
$$$(\iInf s).map f = \bigwedge_{i} (s(i)).map f$$$
Lean4
theorem map_iInf {ι : Sort*} [Nonempty ι] (f : F) (hf : Function.Injective f) (s : ι → NonUnitalSubring 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)
