map_iSup — Mathlib

English

For a ring hom f and a family of subrings s_i of R, map f (iSup s) = iSup (map f s_i).

Русский

Для кольцевого гомоморфизма f и семейства подкольц s_i, образ через f верхней предела равен верхнему пределу образов: map f (iSup s) = iSup (map f s_i).

LaTeX

$$$\\mathrm{map}\,f\\bigl(\\mathrm{iSup}\\,s\\bigr) = \\big\\(\\mathrm{iSup}\\,i\\bigl(\\mathrm{map}\,f\\,(s\,i)\\bigr)\\right)$$$

Lean4

theorem map_iSup {ι : Sort*} (f : R →+* S) (s : ι → Subring R) : (iSup s).map f = ⨆ i, (s i).map f :=
  (gc_map_comap f).l_iSup

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