Documentation

Mathlib.Order.Category.FinPartOrd

The category of finite partial orders #

This defines FinPartOrd, the category of finite partial orders.

Note: FinPartOrd is not a subcategory of BddOrd because finite orders are not necessarily bounded.

TODO #

FinPartOrd is equivalent to a small category.

source
structure FinPartOrd :
Type (u_1 + 1)

The category of finite partial orders with monotone functions.

Instances For
    source
    instance FinPartOrd.instCoeSortFinPartOrdType :
    CoeSort FinPartOrd (Type u_1)
    source
    instance FinPartOrd.instPartialOrderαToPartOrd (X : FinPartOrd) :
    PartialOrder ↑X.toPartOrd
    source
    def FinPartOrd.of (α : Type u_1) [PartialOrder α] [Fintype α] :
    FinPartOrd

    Construct a bundled FinPartOrd from PartialOrder + Fintype.

    Instances For
      source
      @[simp]
      theorem FinPartOrd.coe_of (α : Type u_1) [PartialOrder α] [Fintype α] :
      ↑(FinPartOrd.of α).toPartOrd = α
      source
      instance FinPartOrd.instInhabitedFinPartOrd :
      Inhabited FinPartOrd
      source
      instance FinPartOrd.largeCategory :
      CategoryTheory.LargeCategory FinPartOrd
      source
      instance FinPartOrd.concreteCategory :
      CategoryTheory.ConcreteCategory FinPartOrd
      source
      instance FinPartOrd.hasForgetToPartOrd :
      CategoryTheory.HasForget₂ FinPartOrd PartOrd
      source
      instance FinPartOrd.hasForgetToFintype :
      CategoryTheory.HasForget₂ FinPartOrd FintypeCat
      source
      @[simp]
      theorem FinPartOrd.Iso.mk_inv {α : FinPartOrd} {β : FinPartOrd} (e : ↑α.toPartOrd ≃o ↑β.toPartOrd) :
      (FinPartOrd.Iso.mk e).inv = ↑(OrderIso.symm e)
      source
      @[simp]
      theorem FinPartOrd.Iso.mk_hom {α : FinPartOrd} {β : FinPartOrd} (e : ↑α.toPartOrd ≃o ↑β.toPartOrd) :
      (FinPartOrd.Iso.mk e).hom = ↑e
      source
      def FinPartOrd.Iso.mk {α : FinPartOrd} {β : FinPartOrd} (e : ↑α.toPartOrd ≃o ↑β.toPartOrd) :
      α ≅ β

      Constructs an isomorphism of finite partial orders from an order isomorphism between them.

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

        OrderDual as a functor.

        Instances For
          source
          @[simp]
          theorem FinPartOrd.dualEquiv_functor :
          FinPartOrd.dualEquiv.functor = FinPartOrd.dual
          source
          @[simp]
          theorem FinPartOrd.dualEquiv_inverse :
          FinPartOrd.dualEquiv.inverse = FinPartOrd.dual
          source
          def FinPartOrd.dualEquiv :
          FinPartOrd ≌ FinPartOrd

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

          Instances For
            source
            theorem FinPartOrd_dual_comp_forget_to_partOrd :
            CategoryTheory.Functor.comp FinPartOrd.dual (CategoryTheory.forget₂ FinPartOrd PartOrd) = CategoryTheory.Functor.comp (CategoryTheory.forget₂ FinPartOrd PartOrd) PartOrd.dual