English
The equality of emultiplicities holds for corresponding factors under a prime-power correspondence.
Русский
Сохранение эмп множителей под соответствием простого фактора влечёт равенство эмп.
LaTeX
$$emultiplicity (P_i^{e_i}) (P_j^{e_j}) = emultiplicity (P_i) (P_j)$$
Lean4
/-- The bijection between the (normalized) prime factors of `r` and the (normalized) prime factors
of `span {r}` -/
noncomputable def normalizedFactorsEquivSpanNormalizedFactors {r : R} (hr : r ≠ 0) :
{d : R | d ∈ normalizedFactors r} ≃ {I : Ideal R | I ∈ normalizedFactors (Ideal.span ({ r } : Set R))} :=
by
refine Equiv.ofBijective ?_ ?_
· exact fun d => ⟨Ideal.span {↑d}, singleton_span_mem_normalizedFactors_of_mem_normalizedFactors d.prop⟩
· refine ⟨?_, ?_⟩
· rintro ⟨a, ha⟩ ⟨b, hb⟩ h
rw [Subtype.mk_eq_mk, Ideal.span_singleton_eq_span_singleton, Subtype.coe_mk, Subtype.coe_mk] at h
exact Subtype.mk_eq_mk.mpr (mem_normalizedFactors_eq_of_associated ha hb h)
· rintro ⟨i, hi⟩
have : i.IsPrime := isPrime_of_prime (prime_of_normalized_factor i hi)
have :=
exists_mem_normalizedFactors_of_dvd hr
(Submodule.IsPrincipal.prime_generator_of_isPrime i (prime_of_normalized_factor i hi).ne_zero).irreducible ?_
· obtain ⟨a, ha, ha'⟩ := this
use ⟨a, ha⟩
simp only [← span_singleton_eq_span_singleton.mpr ha', Ideal.span_singleton_generator]
·
exact
(Submodule.IsPrincipal.mem_iff_generator_dvd i).mp
((show Ideal.span { r } ≤ i from dvd_iff_le.mp (dvd_of_mem_normalizedFactors hi))
(mem_span_singleton.mpr (dvd_refl r)))
