English
If w ≠ v are two height-one primes, then count(K, v, w.asIdeal) = 0.
Русский
Пусть w ≠ v — два простых идеала высоты 1; тогда count(K, v, w.asIdeal) = 0.
LaTeX
$$$$ \\operatorname{count}(K,v, w.asIdeal) = 0 \\quad\\text{ if } w \\neq v. $$$$
Lean4
/-- If `v ≠ w` are two maximal ideals of `R`, then `val_v(w) = 0`. -/
theorem count_maximal_coprime {w : HeightOneSpectrum R} (hw : w ≠ v) :
count K v (w.asIdeal : FractionalIdeal R⁰ K) = 0 :=
by
have hw_fact : (w.asIdeal : FractionalIdeal R⁰ K) = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal := by
rw [(algebraMap R K).map_one, inv_one, spanSingleton_one, one_mul]
have hw_ne_zero : (w.asIdeal : FractionalIdeal R⁰ K) ≠ 0 := coeIdeal_ne_zero.mpr w.ne_bot
have hv : Irreducible (Associates.mk v.asIdeal) := by apply v.associates_irreducible
have hw' : Irreducible (Associates.mk w.asIdeal) := by apply w.associates_irreducible
classical
rw [count_well_defined K v hw_ne_zero hw_fact, Ideal.span_singleton_one, ← Ideal.one_eq_top, Associates.mk_one,
Associates.factors_one, Associates.count_zero hv, ofNat_zero, sub_zero, natCast_eq_zero, ←
pow_one (Associates.mk w.asIdeal), Associates.factors_prime_pow hw', Associates.count_some hv,
Multiset.replicate_one, Multiset.count_eq_zero, Multiset.mem_singleton]
simp only [Subtype.mk.injEq]
rw [Associates.mk_eq_mk_iff_associated, associated_iff_eq, ← HeightOneSpectrum.ext_iff]
exact Ne.symm hw
