English
Same principle as above, in the appropriate setting relating primes over p with normalized factors of mapped p.
Русский
То же самое в соответствующей постановке между primesOver и нормализованными факторами образованного p.
LaTeX
$$$P \in p.primesOver A \iff P \in \mathrm{normalizedFactors}(\mathrm{Ideal.map}(\mathrm{algebraMap}\,R\,A) p)$$$
Lean4
theorem mem_primesOver_iff_mem_normalizedFactors {p : Ideal R} [h : p.IsMaximal] [Algebra R A] [NoZeroSMulDivisors R A]
(hp : p ≠ ⊥) {P : Ideal A} : P ∈ p.primesOver A ↔ P ∈ normalizedFactors (Ideal.map (algebraMap R A) p) :=
by
rw [primesOver, Set.mem_setOf_eq, mem_normalizedFactors_iff (map_ne_bot_of_ne_bot hp), liesOver_iff, under_def,
and_congr_right_iff, map_le_iff_le_comap]
intro hP
refine ⟨fun h ↦ le_of_eq h, fun h' ↦ ((IsCoatom.le_iff_eq (isMaximal_def.mp h) ?_).mp h').symm⟩
exact comap_ne_top (algebraMap R A) (IsPrime.ne_top hP)
