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.instParentProjectionPreorderPartialOrderToPreorder :
    CategoryTheory.BundledHom.ParentProjection @PartialOrder.toPreorder
    Equations
    source
    instance instPartOrdLargeCategory :
    CategoryTheory.LargeCategory PartOrd
    Equations
    source
    instance PartOrd.instConcreteCategory :
    CategoryTheory.ConcreteCategory PartOrd
    Equations
    source
    instance PartOrd.instCoeSortType :
    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.instInhabited :
      Inhabited PartOrd
      Equations
      source
      instance PartOrd.instPartialOrderα (α : PartOrd) :
      PartialOrder ↑α
      Equations
      • α.instPartialOrderα = α.str
      source
      instance PartOrd.hasForgetToPreord :
      CategoryTheory.HasForget₂ PartOrd Preord
      Equations
      source
      def PartOrd.Iso.mk {α : PartOrd} {β : PartOrd} (e : ↑α ≃o ↑β) :
      α ≅ β

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

      Equations
      • PartOrd.Iso.mk e = { hom := ↑e, inv := ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }
      Instances For
        source
        @[simp]
        theorem PartOrd.Iso.mk_inv {α : PartOrd} {β : PartOrd} (e : ↑α ≃o ↑β) :
        (PartOrd.Iso.mk e).inv = ↑e.symm
        source
        @[simp]
        theorem PartOrd.Iso.mk_hom {α : PartOrd} {β : PartOrd} (e : ↑α ≃o ↑β) :
        (PartOrd.Iso.mk e).hom = ↑e
        source
        def PartOrd.dual :
        CategoryTheory.Functor PartOrd PartOrd

        OrderDual as a functor.

        Equations
        Instances For
          source
          @[simp]
          theorem PartOrd.dual_obj (X : PartOrd) :
          PartOrd.dual.obj X = PartOrd.of (↑X)ᵒᵈ
          source
          @[simp]
          theorem PartOrd.dual_map :
          ∀ {X Y : PartOrd} (a : ↑X →o ↑Y), PartOrd.dual.map a = OrderHom.dual a
          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
            @[simp]
            theorem PartOrd.dualEquiv_inverse :
            PartOrd.dualEquiv.inverse = PartOrd.dual
            source
            @[simp]
            theorem PartOrd.dualEquiv_functor :
            PartOrd.dualEquiv.functor = PartOrd.dual
            source
            theorem partOrd_dual_comp_forget_to_preord :
            PartOrd.dual.comp (CategoryTheory.forget₂ PartOrd Preord) = (CategoryTheory.forget₂ PartOrd Preord).comp 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
                def preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd :
                preordToPartOrd.comp PartOrd.dual ≅ Preord.dual.comp preordToPartOrd

                PreordToPartOrd and OrderDual commute.

                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 : ↑((Preord.dual.comp preordToPartOrd).obj X)) :
                  (preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.inv.app X) a = (OrderIso.dualAntisymmetrization ↑X).symm a
                  source
                  theorem preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_coe (X : Preord) (a : ↑((preordToPartOrd.comp PartOrd.dual).obj X)) :
                  (preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.hom.app X) a = (OrderIso.dualAntisymmetrization ↑X) a