comap_injective_of_surjective — Mathlib

English

Let f be a surjective homomorphism between semiring-like structures. Then the preimage map on ideals, comap f, is injective: if comap f(I) = comap f(J) for two ideals I and J, then I = J.

Русский

Пусть f — сюръективное гомоморфизм между полупринцами. Тогда отображение предобраза comap f на идеалы инъективно: если comap f(I) = comap f(J), то I = J.

LaTeX

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

Lean4

theorem comap_injective_of_surjective : Injective (comap f) :=
  (giMapComap f hf).u_injective

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