map_iSup_comap_of_surjective — Mathlib

English

Let f be surjective. For any index set ι and a family K: ι → Ideal S, the map of the supremum of comaps equals the supremum of the K(i): map f (⊔_i (K(i).comap f)) = ⊔_i K(i).

Русский

Пусть f сюръективно. Для любой семейки K(i) идеалов S выполнение отображения ядра предобраза отправляет сумму предобразов в сумму K(i).

LaTeX

$$$hf : \mathrm{Function.Surjective}(f) \rightarrow \forall K : ι \to \mathrm{Ideal}(S),\; \mathrm{map}(f)(\bigvee_{i} (K(i).comap f)) = \bigvee_{i} K(i)$$$

Lean4

theorem map_iSup_comap_of_surjective (K : ι → Ideal S) : (⨆ i, (K i).comap f).map f = iSup K :=
  (giMapComap f hf).l_iSup_u _

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