English
If m,p ∈ Associates(M) and n ∈ Associates(N) with appropriate hypotheses, then there exists a factor iso mapping p to a divisor in n preserving emultiplicity.
Русский
Если m,p ∈ Associates(M) и n ∈ Associates(N) с нужными допущениями, существует отображение-фактор-изоморфизм, сохраняющий эмпемлиптичность.
LaTeX
$$emultiplicity_prime_le_emultiplicity_image_by_factor_orderIso hp d$$
Lean4
theorem emultiplicity_factor_dvd_iso_eq_emultiplicity_of_mem_normalizedFactors {m p : M} {n : N} (hm : m ≠ 0)
(hn : n ≠ 0) (hp : p ∈ normalizedFactors m) {d : { l : M // l ∣ m } ≃ { l : N // l ∣ n }}
(hd : ∀ l l', (d l : N) ∣ d l' ↔ (l : M) ∣ l') :
emultiplicity (d ⟨p, dvd_of_mem_normalizedFactors hp⟩ : N) n = emultiplicity p m :=
by
apply Eq.symm
suffices
emultiplicity (Associates.mk p) (Associates.mk m) =
emultiplicity
(Associates.mk
↑(d
⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), by
simp [dvd_of_mem_normalizedFactors hp]⟩))
(Associates.mk n)
by
simpa only [emultiplicity_mk_eq_emultiplicity, associatesEquivOfUniqueUnits_symm_apply,
associatesEquivOfUniqueUnits_apply, out_mk, normalize_eq] using this
have :
Associates.mk
(d
⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), by
simp only [dvd_of_mem_normalizedFactors hp, associatesEquivOfUniqueUnits_symm_apply,
associatesEquivOfUniqueUnits_apply, out_mk, normalize_eq]⟩ :
N) =
↑(mkFactorOrderIsoOfFactorDvdEquiv hd
⟨associatesEquivOfUniqueUnits.symm p,
by
rw [associatesEquivOfUniqueUnits_symm_apply]
exact mk_le_mk_of_dvd (dvd_of_mem_normalizedFactors hp)⟩) :=
by rw [mkFactorOrderIsoOfFactorDvdEquiv_apply_coe]
rw [this]
refine
emultiplicity_prime_eq_emultiplicity_image_by_factor_orderIso (mk_ne_zero.mpr hn) ?_
(mkFactorOrderIsoOfFactorDvdEquiv hd)
obtain ⟨q, hq, hq'⟩ :=
exists_mem_normalizedFactors_of_dvd (mk_ne_zero.mpr hm) (prime_mk.mpr (prime_of_normalized_factor p hp)).irreducible
(mk_le_mk_of_dvd (dvd_of_mem_normalizedFactors hp))
rwa [associated_iff_eq.mp hq']
