map_iSup — Mathlib

English

Let f be a ring homomorphism and s(i) a directed family of subfields of K. The image of the iSup equals the iSup of the images: (iSup s).map f = ⨆ i, (s i).map f.

Русский

Пусть f — кольцеобразный гомоморфизм, а {S_i} — направленная семейство подполей K. Образ iSup равен iSup образов: (iSup s).map f = ⨆ i, (s i).map f.

LaTeX

$$$$(\operatorname{iSup}_{i} S(i)).map f = \bigvee_{i} (S(i)).map f$$$$

Lean4

theorem map_iSup {ι : Sort*} (f : K →+* L) (s : ι → Subfield K) : (iSup s).map f = ⨆ i, (s i).map f :=
  (gc_map_comap f).l_iSup

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