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
      • One or more equations did not get rendered due to their size.
      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
        def FinPartOrd.Hom.Simps.hom (X Y : FinPartOrd) (f : X.Hom Y.toPartOrd) :
        ↑X.toPartOrd →o ↑Y.toPartOrd

        Use the ConcreteCategory.hom projection for @[simps] lemmas.

        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
          @[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_hom {α β : FinPartOrd} (e : ↑α.toPartOrd ≃o ↑β.toPartOrd) :
            (mk e).hom = ofHom ↑e
            source
            @[simp]
            theorem FinPartOrd.Iso.mk_inv {α β : FinPartOrd} (e : ↑α.toPartOrd ≃o ↑β.toPartOrd) :
            (mk e).inv = ofHom ↑e.symm
            source
            def FinPartOrd.dual :
            CategoryTheory.Functor FinPartOrd FinPartOrd

            OrderDual as a functor.

            Equations
            • One or more equations did not get rendered due to their size.
            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
              • One or more equations did not get rendered due to their size.
              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_counitIso :
                dualEquiv.counitIso = CategoryTheory.NatIso.ofComponents (fun (X : FinPartOrd) => Iso.mk (OrderIso.dualDual ↑X.toPartOrd)) @dualEquiv.proof_2
                source
                @[simp]
                theorem FinPartOrd.dualEquiv_inverse :
                dualEquiv.inverse = dual
                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