exists_comap_eq_of_mem_minimalPrimes

English

If f is injective, and p ∈ minimalPrimes R, then there exists p' ∈ Ideal S with p'.IsPrime and p'.comap f = p.

Русский

Пусть f инъективно; если p ∈ minimalPrimes R, найдётся p' ∈ Ideal S с p'prime и p'.comap f = p.

LaTeX

$$$\text{If } hf: \text{Function.Injective } f,\ p \in I.minimalPrimes \Rightarrow \exists p' : Ideal S, p'.IsPrime \land p'.comap f = p$$$

Lean4

theorem exists_comap_eq_of_mem_minimalPrimes {I : Ideal S} (f : R →+* S) (p) (H : p ∈ (I.comap f).minimalPrimes) :
    ∃ p' : Ideal S, p'.IsPrime ∧ I ≤ p' ∧ p'.comap f = p :=
  have := H.1.1
  have ⟨p', hIp', hp', le⟩ := exists_ideal_comap_le_prime p I H.1.2
  ⟨p', hp', hIp', le.antisymm (H.2 ⟨inferInstance, comap_mono hIp'⟩ le)⟩

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