English
There is a natural equivalence between supremum-homomorphisms and infimum-homomorphisms on dual orders: sSupHom α β ≃ sInfHom αᵒᵈ βᵒᵈ.
Русский
Существует естественное эквивалентное соответствие между гомоморфизмами, сохраняющими наибольшие верхние пределы, и гомоморфизмами, сохраняющими наименьшие нижние пределы на двойственных порядка αᵒᵈ и βᵒᵈ.
LaTeX
$$$sSupHom\\;\\alpha\\;\\beta \\simeq sInfHom\\;\\alpha^{\\mathrm{op}}\\;\\beta^{\\mathrm{op}}$$$
Lean4
/-- Reinterpret a `⨆`-homomorphism as an `⨅`-homomorphism between the dual orders. -/
@[simps]
protected def dual : sSupHom α β ≃ sInfHom αᵒᵈ βᵒᵈ
where
toFun f := ⟨toDual ∘ f ∘ ofDual, f.map_sSup'⟩
invFun f := ⟨ofDual ∘ f ∘ toDual, f.map_sInf'⟩
