English
There is a bijection between height-one spectrum primes over p and primes over p in B under suitable hypotheses.
Русский
Существует биекция между простыми высоты единицы над p и простыми над p в B при заданных условиях.
LaTeX
$$equivPrimesOver B hp : { v ∈ HeightOneSpectrum B // v.asIdeal ∣ map p } ≃ p.primesOver B$$
Lean4
/-- The bijection between the elements of the height one prime spectrum of `B` that divide the lift
of the maximal ideal `p` in `B` and the primes over `p` in `B`.
-/
noncomputable def equivPrimesOver (hp : p ≠ 0) :
{ v : HeightOneSpectrum B // v.asIdeal ∣ map (algebraMap A B) p } ≃ p.primesOver B :=
Set.BijOn.equiv HeightOneSpectrum.asIdeal
⟨fun v hv ↦ ⟨v.isPrime, by rwa [liesOver_iff_dvd_map v.isPrime.ne_top]⟩, fun _ _ _ _ h ↦
HeightOneSpectrum.ext_iff.mpr h, fun Q hQ ↦
⟨⟨Q, hQ.1, ne_bot_of_mem_primesOver hp hQ⟩, (liesOver_iff_dvd_map hQ.1.ne_top).mp hQ.2, rfl⟩⟩
