Documentation

Mathlib.Order.Category.BddOrd

The category of bounded orders #

This defines BddOrd, the category of bounded orders.

source
structure BddOrd :
Type (u_1 + 1)

The category of bounded orders with monotone functions.

  • toPartOrd : PartOrd

    The underlying object in the category of partial orders.

  • isBoundedOrder : BoundedOrder ↑self.toPartOrd
Instances For
    source
    instance BddOrd.instCoeSortType :
    CoeSort BddOrd (Type u_1)
    Equations
    source
    instance BddOrd.instPartialOrderαToPartOrd (X : BddOrd) :
    PartialOrder ↑X.toPartOrd
    Equations
    • X.instPartialOrderαToPartOrd = X.toPartOrd.str
    source
    def BddOrd.of (α : Type u_1) [PartialOrder α] [BoundedOrder α] :
    BddOrd

    Construct a bundled BddOrd from a Fintype PartialOrder.

    Equations
    Instances For
      source
      @[simp]
      theorem BddOrd.coe_of (α : Type u_1) [PartialOrder α] [BoundedOrder α] :
      ↑(BddOrd.of α).toPartOrd = α
      source
      instance BddOrd.instInhabited :
      Inhabited BddOrd
      Equations
      source
      instance BddOrd.largeCategory :
      CategoryTheory.LargeCategory BddOrd
      Equations
      source
      instance BddOrd.instFunLike (X : BddOrd) (Y : BddOrd) :
      FunLike (X ⟶ Y) ↑X.toPartOrd ↑Y.toPartOrd
      Equations
      • X.instFunLike Y = let_fun this := inferInstance; this
      source
      instance BddOrd.concreteCategory :
      CategoryTheory.ConcreteCategory BddOrd
      Equations
      • One or more equations did not get rendered due to their size.
      source
      instance BddOrd.hasForgetToPartOrd :
      CategoryTheory.HasForget₂ BddOrd PartOrd
      Equations
      • One or more equations did not get rendered due to their size.
      source
      instance BddOrd.hasForgetToBipointed :
      CategoryTheory.HasForget₂ BddOrd Bipointed
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[simp]
      theorem BddOrd.dual_map {X : BddOrd} {Y : BddOrd} (a : BoundedOrderHom ↑X.toPartOrd ↑Y.toPartOrd) :
      BddOrd.dual.map a = BoundedOrderHom.dual a
      source
      @[simp]
      theorem BddOrd.dual_obj (X : BddOrd) :
      BddOrd.dual.obj X = BddOrd.of (↑X.toPartOrd)ᵒᵈ
      source
      def BddOrd.dual :
      CategoryTheory.Functor BddOrd BddOrd

      OrderDual as a functor.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem BddOrd.Iso.mk_hom {α : BddOrd} {β : BddOrd} (e : ↑α.toPartOrd ≃o ↑β.toPartOrd) :
        (BddOrd.Iso.mk e).hom = ↑e
        source
        @[simp]
        theorem BddOrd.Iso.mk_inv {α : BddOrd} {β : BddOrd} (e : ↑α.toPartOrd ≃o ↑β.toPartOrd) :
        (BddOrd.Iso.mk e).inv = ↑e.symm
        source
        def BddOrd.Iso.mk {α : BddOrd} {β : BddOrd} (e : ↑α.toPartOrd ≃o ↑β.toPartOrd) :
        α ≅ β

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

        Equations
        • BddOrd.Iso.mk e = { hom := ↑e, inv := ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }
        Instances For
          source
          @[simp]
          theorem BddOrd.dualEquiv_functor :
          BddOrd.dualEquiv.functor = BddOrd.dual
          source
          @[simp]
          theorem BddOrd.dualEquiv_inverse :
          BddOrd.dualEquiv.inverse = BddOrd.dual
          source
          def BddOrd.dualEquiv :
          BddOrd ≌ BddOrd

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem bddOrd_dual_comp_forget_to_partOrd :
            BddOrd.dual.comp (CategoryTheory.forget₂ BddOrd PartOrd) = (CategoryTheory.forget₂ BddOrd PartOrd).comp PartOrd.dual
            source
            theorem bddOrd_dual_comp_forget_to_bipointed :
            BddOrd.dual.comp (CategoryTheory.forget₂ BddOrd Bipointed) = (CategoryTheory.forget₂ BddOrd Bipointed).comp Bipointed.swap