Documentation

Mathlib.Order.Category.Preord

Category of preorders #

This defines Preord, the category of preorders with monotone maps.

source
def Preord :
Type (u_1 + 1)

The category of preorders.

Equations
Instances For
    source
    instance Preord.instBundledHomTypePreorderOrderHom :
    CategoryTheory.BundledHom OrderHom
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance Preord.instConcreteCategoryPreordInstPreordLargeCategory :
    CategoryTheory.ConcreteCategory Preord
    Equations
    source
    instance Preord.instCoeSortPreordType :
    CoeSort Preord (Type u_1)
    Equations
    source
    def Preord.of (α : Type u_1) [Preorder α] :
    Preord

    Construct a bundled Preord from the underlying type and typeclass.

    Equations
    Instances For
      source
      @[simp]
      theorem Preord.coe_of (α : Type u_1) [Preorder α] :
      ↑(Preord.of α) = α
      source
      instance Preord.instInhabitedPreord :
      Inhabited Preord
      Equations
      source
      instance Preord.instPreorderα (α : Preord) :
      Preorder ↑α
      Equations
      source
      @[simp]
      theorem Preord.Iso.mk_hom {α : Preord} {β : Preord} (e : ↑α ≃o ↑β) :
      (Preord.Iso.mk e).hom = ↑e
      source
      @[simp]
      theorem Preord.Iso.mk_inv {α : Preord} {β : Preord} (e : ↑α ≃o ↑β) :
      (Preord.Iso.mk e).inv = ↑(OrderIso.symm e)
      source
      def Preord.Iso.mk {α : Preord} {β : Preord} (e : ↑α ≃o ↑β) :
      α ≅ β

      Constructs an equivalence between preorders from an order isomorphism between them.

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

        OrderDual as a functor.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem Preord.dualEquiv_inverse :
          Preord.dualEquiv.inverse = Preord.dual
          source
          @[simp]
          theorem Preord.dualEquiv_functor :
          Preord.dualEquiv.functor = Preord.dual
          source
          def Preord.dualEquiv :
          Preord ≌ Preord

          The equivalence between Preord 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 preordToCat_obj (X : Preord) :
            preordToCat.obj X = CategoryTheory.Cat.of ↑X
            source
            @[simp]
            theorem preordToCat_map :
            ∀ {X Y : Preord} (f : X ⟶ Y), preordToCat.map f = Monotone.functor ⋯
            source
            def preordToCat :
            CategoryTheory.Functor Preord CategoryTheory.Cat

            The embedding of Preord into Cat.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              instance instFaithfulPreordInstPreordLargeCategoryCatCategoryPreordToCat :
              CategoryTheory.Functor.Faithful preordToCat
              Equations
              source
              instance instFullPreordInstPreordLargeCategoryCatCategoryPreordToCat :
              CategoryTheory.Functor.Full preordToCat
              Equations