exists_minimalPrimes_comap_eq — Mathlib

English

For any p ∈ (I.comap f).minimalPrimes, there exists p' ∈ I.minimalPrimes with comap f p' = p.

Русский

Для любого p ∈ (I.comap f).minimalPrimes найдётся p' ∈ I.minimalPrimes с comap f p' = p.

LaTeX

$$$\exists p' \in I.minimalPrimes,\ Ideal.comap f p' = p$$$

Lean4

theorem exists_minimalPrimes_comap_eq {I : Ideal S} (f : R →+* S) (p) (H : p ∈ (I.comap f).minimalPrimes) :
    ∃ p' ∈ I.minimalPrimes, Ideal.comap f p' = p :=
  by
  obtain ⟨p', h₁, h₂, h₃⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f p H
  obtain ⟨q, hq, hq'⟩ := Ideal.exists_minimalPrimes_le h₂
  refine ⟨q, hq, Eq.symm ?_⟩
  have := hq.1.1
  have := (Ideal.comap_mono hq').trans_eq h₃
  exact (H.2 ⟨inferInstance, Ideal.comap_mono hq.1.2⟩ this).antisymm this

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