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
        @[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_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
          • 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_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