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 FinPartOrdextends PartOrd :
Type (u_1 + 1)

The category of finite partial orders with monotone functions.

Instances For
    source
    instance FinPartOrd.instCoeSortType :
    CoeSort FinPartOrd (Type u_1)
    Equations
      source
      instance FinPartOrd.instPartialOrderCarrier (X : FinPartOrd) :
      PartialOrder ↑X.toPartOrd
      Equations
        source
        @[reducible, inline]
        abbrev FinPartOrd.of (α : Type u_1) [PartialOrder α] [Fintype α] :
        FinPartOrd

        Construct a bundled FinPartOrd from PartialOrder + Fintype.

        Equations
          Instances For
            source
            instance FinPartOrd.instInhabited :
            Inhabited FinPartOrd
            Equations
              source
              instance FinPartOrd.largeCategory :
              CategoryTheory.LargeCategory FinPartOrd
              Equations
                source
                instance FinPartOrd.concreteCategory :
                CategoryTheory.ConcreteCategory FinPartOrd fun (x1 x2 : FinPartOrd) => ↑x1.toPartOrd →o ↑x2.toPartOrd
                Equations
                  source
                  instance FinPartOrd.hasForgetToPartOrd :
                  CategoryTheory.HasForget₂ FinPartOrd PartOrd
                  Equations
                    source
                    instance FinPartOrd.hasForgetToFintype :
                    CategoryTheory.HasForget₂ FinPartOrd FintypeCat
                    Equations
                      source
                      @[reducible, inline]
                      abbrev FinPartOrd.ofHom {X Y : Type u} [PartialOrder X] [Fintype X] [PartialOrder Y] [Fintype Y] (f : X →o Y) :
                      of X ⟶ of Y

                      Typecheck a OrderHom as a morphism in FinPartOrd.

                      Equations
                        Instances For
                          source
                          @[simp]
                          theorem FinPartOrd.hom_id {X : FinPartOrd} :
                          PartOrd.Hom.hom (CategoryTheory.CategoryStruct.id X) = OrderHom.id
                          source
                          theorem FinPartOrd.id_apply (X : FinPartOrd) (x : ↑X.toPartOrd) :
                          (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
                          source
                          @[simp]
                          theorem FinPartOrd.hom_comp {X Y Z : FinPartOrd} (f : X ⟶ Y) (g : Y ⟶ Z) :
                          PartOrd.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (PartOrd.Hom.hom g).comp (PartOrd.Hom.hom f)
                          source
                          theorem FinPartOrd.comp_apply {X Y Z : FinPartOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X.toPartOrd) :
                          (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
                          source
                          theorem FinPartOrd.hom_ext {X Y : FinPartOrd} {f g : X ⟶ Y} (hf : PartOrd.Hom.hom f = PartOrd.Hom.hom g) :
                          f = g
                          source
                          theorem FinPartOrd.hom_ext_iff {X Y : FinPartOrd} {f g : X ⟶ Y} :
                          f = g ↔ PartOrd.Hom.hom f = PartOrd.Hom.hom g
                          source
                          @[simp]
                          theorem FinPartOrd.hom_ofHom {X Y : Type u} [PartialOrder X] [Fintype X] [PartialOrder Y] [Fintype Y] (f : X →o Y) :
                          PartOrd.Hom.hom (ofHom f) = f
                          source
                          @[simp]
                          theorem FinPartOrd.ofHom_hom {X Y : FinPartOrd} (f : X ⟶ Y) :
                          ofHom (PartOrd.Hom.hom f) = f
                          source
                          def FinPartOrd.Iso.mk {α β : FinPartOrd} (e : ↑α.toPartOrd ≃o ↑β.toPartOrd) :
                          α ≅ β

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

                          Equations
                            Instances For
                              source
                              @[simp]
                              theorem FinPartOrd.Iso.mk_inv {α β : FinPartOrd} (e : ↑α.toPartOrd ≃o ↑β.toPartOrd) :
                              (mk e).inv = ofHom ↑e.symm
                              source
                              @[simp]
                              theorem FinPartOrd.Iso.mk_hom {α β : FinPartOrd} (e : ↑α.toPartOrd ≃o ↑β.toPartOrd) :
                              (mk e).hom = ofHom ↑e
                              source
                              def FinPartOrd.dual :
                              CategoryTheory.Functor FinPartOrd FinPartOrd

                              OrderDual as a functor.

                              Equations
                                Instances For
                                  source
                                  @[simp]
                                  theorem FinPartOrd.dual_map {X✝ Y✝ : FinPartOrd} (f : X✝ ⟶ Y✝) :
                                  dual.map f = ofHom (OrderHom.dual (PartOrd.Hom.hom f))
                                  source
                                  def FinPartOrd.dualEquiv :
                                  FinPartOrd ≌ FinPartOrd

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

                                  Equations
                                    Instances For
                                      source
                                      @[simp]
                                      theorem FinPartOrd.dualEquiv_unitIso :
                                      dualEquiv.unitIso = CategoryTheory.NatIso.ofComponents (fun (X : FinPartOrd) => Iso.mk (OrderIso.dualDual ↑X.toPartOrd)) @dualEquiv._proof_1
                                      source
                                      @[simp]
                                      theorem FinPartOrd.dualEquiv_inverse :
                                      dualEquiv.inverse = dual
                                      source
                                      @[simp]
                                      theorem FinPartOrd.dualEquiv_counitIso :
                                      dualEquiv.counitIso = CategoryTheory.NatIso.ofComponents (fun (X : FinPartOrd) => Iso.mk (OrderIso.dualDual ↑X.toPartOrd)) @dualEquiv._proof_2
                                      source
                                      @[simp]
                                      theorem FinPartOrd.dualEquiv_functor :
                                      dualEquiv.functor = dual
                                      source
                                      theorem FinPartOrd_dual_comp_forget_to_partOrd :
                                      FinPartOrd.dual.comp (CategoryTheory.forget₂ FinPartOrd PartOrd) = (CategoryTheory.forget₂ FinPartOrd PartOrd).comp PartOrd.dual