English
In a divisor chain, if p is prime and p divides r with r divides q, and the chain enumerates divisors up to q, then p equals the second element c(1).
Русский
В цепи делителей, если p — простое и p делит r, а r делит q, и цепь перечисляет делители до q, то p равно второму элементу c(1).
LaTeX
$$$p = c(1)$$$
Lean4
theorem map_prime_of_factor_orderIso {m p : Associates M} {n : Associates N} (hn : n ≠ 0) (hp : p ∈ normalizedFactors m)
(d : Set.Iic m ≃o Set.Iic n) : Prime (d ⟨p, dvd_of_mem_normalizedFactors hp⟩ : Associates N) :=
by
rw [← irreducible_iff_prime]
refine (Associates.isAtom_iff <| ne_zero_of_dvd_ne_zero hn (d ⟨p, _⟩).prop).mp ⟨?_, fun b hb => ?_⟩
· rw [Ne, ← Associates.isUnit_iff_eq_bot, Associates.isUnit_iff_eq_one, coe_factor_orderIso_map_eq_one_iff _ d]
rintro rfl
exact (prime_of_normalized_factor 1 hp).not_unit isUnit_one
· have : b ≤ n := le_trans (le_of_lt hb) (d ⟨p, dvd_of_mem_normalizedFactors hp⟩).prop
obtain ⟨x, hx⟩ := d.surjective ⟨b, this⟩
rw [← Subtype.coe_mk (p := (· ≤ n)) b this, ← hx] at hb
letI : OrderBot { l : Associates M // l ≤ m } := Subtype.orderBot bot_le
letI : OrderBot { l : Associates N // l ≤ n } := Subtype.orderBot bot_le
suffices x = ⊥ by
rw [this, OrderIso.map_bot d] at hx
refine (Subtype.mk_eq_bot_iff ?_ _).mp hx.symm
simp
obtain ⟨a, ha⟩ := x
rw [Subtype.mk_eq_bot_iff]
·
exact
((Associates.isAtom_iff <| Prime.ne_zero <| prime_of_normalized_factor p hp).mpr <|
irreducible_of_normalized_factor p hp).right
a (Subtype.mk_lt_mk.mp <| d.lt_iff_lt.mp hb)
simp
