English
There is a natural equivalence between TopHom α β and BotHom αᵒᵈ βᵒᵈ, given by sending a top-homomorphism to a bot-homomorphism on the dual order and vice versa.
Русский
Существует естественное эквивалентное соответствие между TopHom α β и BotHom αᵒᵈ βᵒᵈ, переводя топ-гомоморфизм в бот-гомоморфизм на двойственном порядке и обратно.
LaTeX
$$$\mathrm{TopHom}(\alpha,\beta) \simeq \mathrm{BotHom}(\alpha^{\mathrm{op}},\beta^{\mathrm{op}})$$$
Lean4
/-- Reinterpret a top homomorphism as a bot homomorphism between the dual lattices. -/
@[simps]
protected def dual : TopHom α β ≃ BotHom αᵒᵈ βᵒᵈ
where
toFun f := ⟨f, f.map_top'⟩
invFun f := ⟨f, f.map_bot'⟩
