primesOverFinset_eq — Mathlib

English

A bijection between height-one primes over p and primes over p in a Dedekind domain via liesOver relations.

Русский

Биекция между высотными единичными простыми над p и простыми над p в кольце Дедекина через отношения liesOver.

LaTeX

$$equivPrimesOver B hp : { v ∈ HeightOneSpectrum B // v.asIdeal ∣ map p } ≃ p.primesOver B$$

Lean4

theorem primesOverFinset_eq [IsLocalRing A] [IsDedekindDomain A] [Algebra R A] [FaithfulSMul R A] [Module.Finite R A]
    {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) : primesOverFinset p A = {IsLocalRing.maximalIdeal A} := by
  rw [← Finset.coe_eq_singleton, coe_primesOverFinset hp0, IsLocalRing.primesOver_eq A hp0]

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