English
There is a natural equivalence between lattice homomorphisms α→β and lattice homomorphisms αᵒᵈ→βᵒᵈ, obtained by passing to the dual lattices and using InfHom and SupHom structure.
Русский
Существует естественное эквивалентное соответствие между гомоморфизмами решётки α→β и гомоморфизмами αᵒᵈ→βᵒᵈ, получаемое переходом к двойственным решёткам.
LaTeX
$$$\text{LatticeHom}(α,β) \simeq \text{LatticeHom}(α^{op}, β^{op}).$$$
Lean4
/-- Reinterpret a lattice homomorphism as a lattice homomorphism between the dual lattices. -/
@[simps]
protected def dual : LatticeHom α β ≃ LatticeHom αᵒᵈ βᵒᵈ
where
toFun f := ⟨InfHom.dual f.toInfHom, f.map_sup'⟩
invFun f := ⟨SupHom.dual.symm f.toInfHom, f.map_sup'⟩
