English
The value count(K, v, I) does not depend on the choice of a and J in a representation I = a^{-1} J.
Русский
Значение count(K, v, I) не зависит от выбора a и J в представлении I = a^{-1}J.
LaTeX
$$$$\\text{count}(K,v,I) = \\bigl(\\mathrm{count}\\,v(J) - \\mathrm{count}\\,v(a)\\bigr) \\quad\\text{independent of } I=a^{-1}J.$$$$
Lean4
/-- `val_v(I)` does not depend on the choice of `a` and `J` used to represent `I`. -/
theorem count_well_defined {I : FractionalIdeal R⁰ K} (hI : I ≠ 0) {a : R} {J : Ideal R}
(h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J) :
count K v I =
((Associates.mk v.asIdeal).count (Associates.mk J).factors -
(Associates.mk v.asIdeal).count (Associates.mk (Ideal.span { a })).factors :
ℤ) :=
by
set a₁ := choose (exists_eq_spanSingleton_mul I)
set J₁ := choose (choose_spec (exists_eq_spanSingleton_mul I))
have h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁ :=
(choose_spec (choose_spec (exists_eq_spanSingleton_mul I))).2
have h_a₁_ne_zero : a₁ ≠ 0 := (choose_spec (choose_spec (exists_eq_spanSingleton_mul I))).1
have h_J₁_ne_zero : J₁ ≠ 0 := ideal_factor_ne_zero hI h_a₁J₁
have h_a_ne_zero : Ideal.span { a } ≠ 0 := constant_factor_ne_zero hI h_aJ
have h_J_ne_zero : J ≠ 0 := ideal_factor_ne_zero hI h_aJ
have h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0 :=
by
rw [ne_eq, spanSingleton_eq_zero_iff, ← (algebraMap R K).map_zero,
Injective.eq_iff (IsLocalization.injective K (le_refl R⁰))]
exact h_a₁_ne_zero
have h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0 :=
by
rw [ne_eq, spanSingleton_eq_zero_iff, ← (algebraMap R K).map_zero,
Injective.eq_iff (IsLocalization.injective K (le_refl R⁰))]
rw [ne_eq, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot] at h_a_ne_zero
exact h_a_ne_zero
have hv : Irreducible (Associates.mk v.asIdeal) := by exact Associates.irreducible_mk.mpr v.irreducible
rw [h_a₁J₁, ← div_spanSingleton, ← div_spanSingleton, div_eq_div_iff h_a₁' h_a', ← coeIdeal_span_singleton, ←
coeIdeal_span_singleton, ← coeIdeal_mul, ← coeIdeal_mul] at h_aJ
rw [count, dif_neg hI, sub_eq_sub_iff_add_eq_add, ← natCast_add, ← natCast_add, natCast_inj, ←
Associates.count_mul _ _ hv, ← Associates.count_mul _ _ hv, Associates.mk_mul_mk, Associates.mk_mul_mk,
coeIdeal_injective h_aJ]
· rw [ne_eq, Associates.mk_eq_zero]; exact h_J_ne_zero
· rw [ne_eq, Associates.mk_eq_zero, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]
exact h_a₁_ne_zero
· rw [ne_eq, Associates.mk_eq_zero]; exact h_J₁_ne_zero
· rw [ne_eq, Associates.mk_eq_zero]; exact h_a_ne_zero
