English
For an order isomorphism d between divisor lattices, the image of the unit 1 is the unit 1 in the codomain.
Русский
Для отображения порядка между цепями делителей верна карта единицы: образ единицы равен единице в кодомонадной цепи.
LaTeX
$$$d(1) = 1$$$
Lean4
theorem factor_orderIso_map_one_eq_bot {m : Associates M} {n : Associates N}
(d : { l : Associates M // l ≤ m } ≃o { l : Associates N // l ≤ n }) : (d ⟨1, one_dvd m⟩ : Associates N) = 1 :=
by
letI : OrderBot { l : Associates M // l ≤ m } := Subtype.orderBot bot_le
letI : OrderBot { l : Associates N // l ≤ n } := Subtype.orderBot bot_le
simp only [← Associates.bot_eq_one, Subtype.mk_bot, bot_le, Subtype.coe_eq_bot_iff]
letI : BotHomClass ({ l // l ≤ m } ≃o { l // l ≤ n }) _ _ := OrderIsoClass.toBotHomClass
exact map_bot d
