exists_comap_eq_of_mem_minimalPrimes_of_injective

English

Given 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,\ \text{Ideal.comap } f p' = p$$$

Lean4

@[stacks 00FK]
theorem exists_comap_eq_of_mem_minimalPrimes_of_injective {f : R →+* S} (hf : Function.Injective f) (p)
    (H : p ∈ minimalPrimes R) : ∃ p' : Ideal S, p'.IsPrime ∧ p'.comap f = p :=
  have ⟨p', hp', _, eq⟩ := exists_comap_eq_of_mem_minimalPrimes f (I := ⊥) p <| by rwa [comap_bot_of_injective f hf]
  ⟨p', hp', eq⟩

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