map_sup_comap_of_surjective — Mathlib

English

If f is surjective, the image under f of the supremum (sum) of two pullbacks equals the supremum of the two original ideals: map f (I.comap f ⊔ J.comap f) = I ⊔ J.

Русский

Пусть f сюръективно. Тогда образ отображения f сумм предобразов I и J равен сумме самих I и J: map f (I.comap f ⊔ J.comap f) = I ⊔ J.

LaTeX

$$$hf : \mathrm{Function.Surjective}(f) \rightarrow \forall I,J \in \mathrm{Ideal}(S),\; \mathrm{map}(f)(I.\comap f ⊔ J.\comap f) = I ⊔ J$$$

Lean4

theorem map_sup_comap_of_surjective (I J : Ideal S) : (I.comap f ⊔ J.comap f).map f = I ⊔ J :=
  (giMapComap f hf).l_sup_u _ _

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