map_sInf — Mathlib

English

Let A be a set of ideals in R and f: R → S be surjective. If ker f ≤ J for every J in A, then the image under f distributes over Inf: map f (sInf A) = sInf (map f '' A).

Русский

Пусть A — множество идеалов R, f сюръективно. Если ker f ≤ J для каждого J ∈ A, то образ f распадается над inf: map f (sInf A) = sInf (map f '' A).

LaTeX

$$$$ \\operatorname{map}\,f(\\mathrm{sInf}\,A) = \\mathrm{sInf}\\big(\\operatorname{map}\,f''A\\big), \\quad \\text{provided } \\ker f \\le J \\text{ for all } J\\in A.$$$$

Lean4

theorem map_sInf {A : Set (Ideal R)} {f : F} (hf : Function.Surjective f) :
    (∀ J ∈ A, RingHom.ker f ≤ J) → map f (sInf A) = sInf (map f '' A) :=
  by
  refine fun h => le_antisymm (le_sInf ?_) ?_
  · intro j hj y hy
    obtain ⟨x, hx⟩ := (mem_map_iff_of_surjective f hf).1 hy
    obtain ⟨J, hJ⟩ := (Set.mem_image _ _ _).mp hj
    rw [← hJ.right, ← hx.right]
    exact mem_map_of_mem f (sInf_le_of_le hJ.left (le_of_eq rfl) hx.left)
  · intro y hy
    obtain ⟨x, hx⟩ := hf y
    refine hx ▸ mem_map_of_mem f ?_
    have : ∀ I ∈ A, y ∈ map f I := by simpa using hy
    rw [Submodule.mem_sInf]
    intro J hJ
    rcases (mem_map_iff_of_surjective f hf).1 (this J hJ) with ⟨x', hx', rfl⟩
    have : x - x' ∈ J := by
      apply h J hJ
      rw [RingHom.mem_ker, map_sub, hx, sub_self]
    simpa only [sub_add_cancel] using J.add_mem this hx'

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