nonemptyFinLinOrdDualCompForgetToFinPartOrd

English

The forgetful functor from NonemptyFinLinOrd to FinPartOrd commutes with taking dual; there is a natural isomorphism between the two composite functors.

Русский

Забывающий функтор из NonemptyFinLinOrd в FinPartOrd коммутирует с двойственностью; существует естественное изоморождение между двумя композициями функторов.

LaTeX

$$$ NonemptyFinLinOrd.dual \circ forget_{NonemptyFinLinOrd,FinPartOrd} \cong forget_{NonemptyFinLinOrd,FinPartOrd} \circ FinPartOrd.dual $$$

Lean4

/-- The forgetful functor `NonemptyFinLinOrd ⥤ FinPartOrd` and `OrderDual` commute. -/
def nonemptyFinLinOrdDualCompForgetToFinPartOrd :
    NonemptyFinLinOrd.dual ⋙ forget₂ NonemptyFinLinOrd FinPartOrd ≅
      forget₂ NonemptyFinLinOrd FinPartOrd ⋙ FinPartOrd.dual
    where
  hom.app X := FinPartOrd.ofHom OrderHom.id
  inv.app X := FinPartOrd.ofHom OrderHom.id

Похожие утверждения