English
Let m, p in Associates M; n in Associates N; with a divisor order isomorphism d between their divisor sets. If p is in the normalized factors of m, then the image d(p) is prime in N.
Русский
Пусть m, p ∈ Associates(M); n ∈ Associates(N); имеется отображение-изоморфизм между цепями делителей; если p входит в нормализованные фактори m, то образ d(p) является простым в N.
LaTeX
$$Prime (d ⟨p, dvd_of_mem_normalizedFactors hp⟩ : Associates N)$$
Lean4
theorem pow_image_of_prime_by_factor_orderIso_dvd {m p : Associates M} {n : Associates N} (hn : n ≠ 0)
(hp : p ∈ normalizedFactors m) (d : Set.Iic m ≃o Set.Iic n) {s : ℕ} (hs' : p ^ s ≤ m) :
(d ⟨p, dvd_of_mem_normalizedFactors hp⟩ : Associates N) ^ s ≤ n :=
by
by_cases hs : s = 0
· simp [← Associates.bot_eq_one, hs]
suffices (d ⟨p, dvd_of_mem_normalizedFactors hp⟩ : Associates N) ^ s = (d ⟨p ^ s, hs'⟩)
by
rw [this]
apply Subtype.prop (d ⟨p ^ s, hs'⟩)
obtain ⟨c₁, rfl, hc₁', hc₁''⟩ := exists_chain_of_prime_pow hs (prime_of_normalized_factor p hp)
let c₂ : Fin (s + 1) → Associates N := fun t => d ⟨c₁ t, le_trans (hc₁''.2 ⟨t, by simp⟩) hs'⟩
have c₂_def : ∀ t, c₂ t = d ⟨c₁ t, _⟩ := fun t => rfl
rw [← c₂_def]
refine (eq_pow_second_of_chain_of_has_chain hs (fun t u h => ?_) (@fun r => ⟨@fun hr => ?_, ?_⟩) ?_).symm
· rw [c₂_def, c₂_def, Subtype.coe_lt_coe, d.lt_iff_lt, Subtype.mk_lt_mk, hc₁'.lt_iff_lt]
exact h
· have : r ≤ n := hr.trans (d ⟨c₁ 1 ^ s, _⟩).2
suffices d.symm ⟨r, this⟩ ≤ ⟨c₁ 1 ^ s, hs'⟩
by
obtain ⟨i, hi⟩ := hc₁''.1 this
use i
simp only [c₂_def, ← hi, d.apply_symm_apply, Subtype.coe_eta, Subtype.coe_mk]
conv_rhs => rw [← d.symm_apply_apply ⟨c₁ 1 ^ s, hs'⟩]
rw [d.symm.le_iff_le]
simpa only [← Subtype.coe_le_coe, Subtype.coe_mk] using hr
· rintro ⟨i, hr⟩
rw [hr, c₂_def, Subtype.coe_le_coe, d.le_iff_le]
simpa [Subtype.mk_le_mk] using hc₁''.2 ⟨i, rfl⟩
exact ne_zero_of_dvd_ne_zero hn (Subtype.prop (d ⟨c₁ 1 ^ s, _⟩))
