English
There is a natural equivalence between supremum-homomorphisms from α to β and infimum-homomorphisms from the duals αᵒᵈ to βᵒᵈ, given by taking dual maps.
Русский
Существует естественное эквивалентное соответствие между гомоморфизмами верхней гранки (sup) из α в β и гомоморфизмами нижней гранки (inf) между двойственными решётками αᵒᵈ и βᵒᵈ, получаемое посредством двойственности.
LaTeX
$$$\mathrm{SupHom}_{\alpha,\beta} \cong \mathrm{InfHom}_{\alpha^{op},\beta^{op}}$$$
Lean4
/-- Reinterpret a supremum homomorphism as an infimum homomorphism between the dual lattices. -/
@[simps]
protected def dual : SupHom α β ≃ InfHom αᵒᵈ βᵒᵈ
where
toFun f := ⟨f, f.map_sup'⟩
invFun f := ⟨f, f.map_inf'⟩
