comap_le_iff_le_map — Mathlib

English

Let f be a bijective ring homomorphism. For any ideals I ⊆ R and K ⊆ S, comap f K ≤ I iff K ≤ map f I.

Русский

Пусть f — биекциируемый кольцевой гомоморфизм. Тогда для любых идеалов I ⊆ R и K ⊆ S выполняется comap f K ≤ I тогда и только тогда, когда K ≤ map f I.

LaTeX

$$$\\mathrm{comap}\, f\, K \\le I \\iff K \\le \\mathrm{map}\, f\, I$$$

Lean4

theorem comap_le_iff_le_map : comap f K ≤ I ↔ K ≤ map f I :=
  ⟨fun h => le_map_of_comap_le_of_surjective f hf.right h, fun h => (relIsoOfBijective f hf).right_inv I ▸ comap_mono h⟩

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