Documentation

Mathlib.Order.Category.PartOrd

Category of partial orders #

This defines PartOrd, the category of partial orders with monotone maps.

source
def PartOrd :
Type (u_1 + 1)

The category of partially ordered types.

Equations
Instances For
    source
    instance PartOrd.instParentProjectionTypePreorderPartialOrderToPreorder :
    CategoryTheory.BundledHom.ParentProjection @PartialOrder.toPreorder
    Equations
    source
    instance PartOrd.instConcreteCategoryPartOrdInstPartOrdLargeCategory :
    CategoryTheory.ConcreteCategory PartOrd
    Equations
    source
    instance PartOrd.instCoeSortPartOrdType :
    CoeSort PartOrd (Type u_1)
    Equations
    source
    def PartOrd.of (α : Type u_1) [PartialOrder α] :
    PartOrd

    Construct a bundled PartOrd from the underlying type and typeclass.

    Equations
    Instances For
      source
      @[simp]
      theorem PartOrd.coe_of (α : Type u_1) [PartialOrder α] :
      ↑(PartOrd.of α) = α
      source
      instance PartOrd.instInhabitedPartOrd :
      Inhabited PartOrd
      Equations
      source
      instance PartOrd.instPartialOrderα (α : PartOrd) :
      PartialOrder ↑α
      Equations
      source
      instance PartOrd.hasForgetToPreord :
      CategoryTheory.HasForget₂ PartOrd Preord
      Equations
      source
      @[simp]
      theorem PartOrd.Iso.mk_inv {α : PartOrd} {β : PartOrd} (e : ↑α ≃o ↑β) :
      (PartOrd.Iso.mk e).inv = ↑(OrderIso.symm e)
      source
      @[simp]
      theorem PartOrd.Iso.mk_hom {α : PartOrd} {β : PartOrd} (e : ↑α ≃o ↑β) :
      (PartOrd.Iso.mk e).hom = ↑e
      source
      def PartOrd.Iso.mk {α : PartOrd} {β : PartOrd} (e : ↑α ≃o ↑β) :
      α ≅ β

      Constructs an equivalence between partial orders from an order isomorphism between them.

      Equations
      Instances For
        source
        @[simp]
        theorem PartOrd.dual_map :
        ∀ {X Y : PartOrd} (a : ↑X →o ↑Y), PartOrd.dual.map a = OrderHom.dual a
        source
        @[simp]
        theorem PartOrd.dual_obj (X : PartOrd) :
        PartOrd.dual.obj X = PartOrd.of (↑X)ᵒᵈ
        source
        def PartOrd.dual :
        CategoryTheory.Functor PartOrd PartOrd

        OrderDual as a functor.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem PartOrd.dualEquiv_inverse :
          PartOrd.dualEquiv.inverse = PartOrd.dual
          source
          @[simp]
          theorem PartOrd.dualEquiv_functor :
          PartOrd.dualEquiv.functor = PartOrd.dual
          source
          def PartOrd.dualEquiv :
          PartOrd ≌ PartOrd

          The equivalence between PartOrd and itself induced by OrderDual both ways.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem partOrd_dual_comp_forget_to_preord :
            CategoryTheory.Functor.comp PartOrd.dual (CategoryTheory.forget₂ PartOrd Preord) = CategoryTheory.Functor.comp (CategoryTheory.forget₂ PartOrd Preord) Preord.dual
            source
            def preordToPartOrd :
            CategoryTheory.Functor Preord PartOrd

            Antisymmetrization as a functor. It is the free functor.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def preordToPartOrdForgetAdjunction :
              preordToPartOrd ⊣ CategoryTheory.forget₂ PartOrd Preord

              preordToPartOrd is left adjoint to the forgetful functor, meaning it is the free functor from Preord to PartOrd.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_coe (X : Preord) (a : ↑((CategoryTheory.Functor.comp Preord.dual preordToPartOrd).obj X)) :
                (preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.inv.app X) a = (OrderIso.symm (OrderIso.dualAntisymmetrization ↑X)) a
                source
                theorem preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_coe (X : Preord) (a : ↑((CategoryTheory.Functor.comp preordToPartOrd PartOrd.dual).obj X)) :
                (preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.hom.app X) a = (OrderIso.dualAntisymmetrization ↑X) a
                source
                def preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd :
                CategoryTheory.Functor.comp preordToPartOrd PartOrd.dual ≅ CategoryTheory.Functor.comp Preord.dual preordToPartOrd

                PreordToPartOrd and OrderDual commute.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For