map_inf_comap_of_surjective — Mathlib

English

Under surjectivity of f, the image under f of the infimum (intersection) of two pullbacks equals the infimum of the two originals: map f (I.comap f ⊓ J.comap f) = I ⊓ J.

Русский

Пусть f сюръективно. Тогда изображение под f пересечения предобразов равно пересечению самих 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 \inf J.\comap f) = I \inf J$$$

Lean4

theorem map_inf_comap_of_surjective (I J : Ideal S) : (I.comap f ⊓ J.comap f).map f = I ⊓ J :=
  (giMapComap f hf).l_inf_u _ _

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