comap_iInf — Mathlib

English

For a family s_i of subrings of S and a ring hom f: R →+* S, the comap distributes over infimum: (iInf s).comap f = ⨅ i, (s i).comap f.

Русский

Пусть s_i — семейство подкольц S; f: R →+* S — гомоморфизм колец. Тогда предобраз по f распределяется по инфимума: (iInf s).comap f = ⨅ i, (s i).comap f.

LaTeX

$$$ (\inf_i s_i).comap f = \inf_i ( s_i.comap f ) $$$

Lean4

theorem comap_iInf {ι : Sort*} (f : R →+* S) (s : ι → Subring S) : (iInf s).comap f = ⨅ i, (s i).comap f :=
  (gc_map_comap f).u_iInf

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