minimal_primes_comap_of_surjective

English

For a surjective f, the minimal primes of I.map f equal the comap f of I.minimalPrimes.

Русский

При сюръекции f минимальныеPrime карты I.map f равны comap f '' I.minimalPrimes.

LaTeX

$$$[IsLocalization]\; (J.map f).minimalPrimes = Ideal.comap f '' J.minimalPrimes$$$

Lean4

theorem minimal_primes_comap_of_surjective {f : R →+* S} (hf : Function.Surjective f) {I J : Ideal S}
    (h : J ∈ I.minimalPrimes) : J.comap f ∈ (I.comap f).minimalPrimes :=
  by
  have := h.1.1
  refine ⟨⟨inferInstance, Ideal.comap_mono h.1.2⟩, ?_⟩
  rintro K ⟨hK, e₁⟩ e₂
  have : RingHom.ker f ≤ K := (Ideal.comap_mono bot_le).trans e₁
  rw [← sup_eq_left.mpr this, RingHom.ker_eq_comap_bot, ← Ideal.comap_map_of_surjective f hf]
  apply Ideal.comap_mono _
  apply h.2 _ _
  · exact ⟨Ideal.map_isPrime_of_surjective hf this, Ideal.le_map_of_comap_le_of_surjective f hf e₁⟩
  · exact Ideal.map_le_of_le_comap e₂

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