isSubDPIdeal_map_of_isSubDPIdeal — Mathlib

English

If f is a DP-morphism from I to J and K is a sub-dp-ideal of I, then the image map f K is a sub-dp-ideal of J.

Русский

Если f является dp-морфизмом из I в J и K — подdp-идеал над I, то образ map f K — под dp-идеал над J.

LaTeX

$$IsSubDPIdeal hJ (map f K)$$

Lean4

theorem isSubDPIdeal_map_of_isSubDPIdeal {f : A →+* B} (hf : IsDPMorphism hI hJ f) {K : Ideal A}
    (hK : IsSubDPIdeal hI K) : IsSubDPIdeal hJ (map f K) :=
  by
  rw [Ideal.map, span_isSubDPIdeal_iff]
  · rintro n hn y ⟨x, hx, rfl⟩
    exact hf.2 x (hK.1 hx) ▸ mem_map_of_mem _ (hK.2 _ hn hx)
  · rintro y ⟨x, hx, rfl⟩
    exact hf.1 (mem_map_of_mem f (hK.1 hx))

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