Documentation

Mathlib.Order.Category.LinOrd

Category of linear orders #

This defines LinOrd, the category of linear orders with monotone maps.

source
def LinOrd :
Type (u_1 + 1)

The category of linear orders.

Equations
Instances For
    source
    instance LinOrd.instParentProjectionTypePartialOrderLinearOrderToPartialOrder :
    CategoryTheory.BundledHom.ParentProjection @LinearOrder.toPartialOrder
    Equations
    source
    instance LinOrd.instConcreteCategoryLinOrdInstLinOrdLargeCategory :
    CategoryTheory.ConcreteCategory LinOrd
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance LinOrd.instCoeSortLinOrdType :
    CoeSort LinOrd (Type u_1)
    Equations
    source
    def LinOrd.of (α : Type u_1) [LinearOrder α] :
    LinOrd

    Construct a bundled LinOrd from the underlying type and typeclass.

    Equations
    Instances For
      source
      @[simp]
      theorem LinOrd.coe_of (α : Type u_1) [LinearOrder α] :
      ↑(LinOrd.of α) = α
      source
      instance LinOrd.instInhabitedLinOrd :
      Inhabited LinOrd
      Equations
      source
      instance LinOrd.instLinearOrderα (α : LinOrd) :
      LinearOrder ↑α
      Equations
      source
      instance LinOrd.hasForgetToLat :
      CategoryTheory.HasForget₂ LinOrd Lat
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[simp]
      theorem LinOrd.Iso.mk_hom {α : LinOrd} {β : LinOrd} (e : ↑α ≃o ↑β) :
      (LinOrd.Iso.mk e).hom = ↑e
      source
      @[simp]
      theorem LinOrd.Iso.mk_inv {α : LinOrd} {β : LinOrd} (e : ↑α ≃o ↑β) :
      (LinOrd.Iso.mk e).inv = ↑(OrderIso.symm e)
      source
      def LinOrd.Iso.mk {α : LinOrd} {β : LinOrd} (e : ↑α ≃o ↑β) :
      α ≅ β

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

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

        OrderDual as a functor.

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

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem linOrd_dual_comp_forget_to_Lat :
            CategoryTheory.Functor.comp LinOrd.dual (CategoryTheory.forget₂ LinOrd Lat) = CategoryTheory.Functor.comp (CategoryTheory.forget₂ LinOrd Lat) Lat.dual