Documentation

Mathlib.Order.Category.NonemptyFinLinOrd

Nonempty finite linear orders #

This defines NonemptyFinLinOrd, the category of nonempty finite linear orders with monotone maps. This is the index category for simplicial objects.

Note: NonemptyFinLinOrd is not a subcategory of FinBddDistLat because its morphisms do not preserve and .

class NonemptyFiniteLinearOrder (α : Type u_1) extends Fintype , LinearOrder , PartialOrder , Min , Max , Ord , Preorder , LE , LT :
Type u_1

A typeclass for nonempty finite linear orders.

    Instances
      def NonemptyFinLinOrd :
      Type (u_1 + 1)

      The category of nonempty finite linear orders.

      Equations
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        • One or more equations did not get rendered due to their size.

        Construct a bundled NonemptyFinLinOrd from the underlying type and typeclass.

        Equations
        Instances For
          Equations
          • α.instNonemptyFiniteLinearOrderα = α.str
          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          • One or more equations did not get rendered due to their size.
          def NonemptyFinLinOrd.Iso.mk {α : NonemptyFinLinOrd} {β : NonemptyFinLinOrd} (e : α ≃o β) :
          α β

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

          Equations
          Instances For
            @[simp]
            @[simp]
            theorem NonemptyFinLinOrd.Iso.mk_inv {α : NonemptyFinLinOrd} {β : NonemptyFinLinOrd} (e : α ≃o β) :
            (NonemptyFinLinOrd.Iso.mk e).inv = e.symm

            OrderDual as a functor.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem NonemptyFinLinOrd.dual_map :
              ∀ {X Y : NonemptyFinLinOrd} (a : X →o Y), NonemptyFinLinOrd.dual.map a = OrderHom.dual a

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

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • NonemptyFinLinOrd.instFunLikeHomαNonemptyFiniteLinearOrder = { coe := fun (f : A B) => (let_fun this := f; this), coe_injective' := }

                The forgetful functor NonemptyFinLinOrdFinPartOrd and OrderDual commute.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def Fin.hom_succ {n : } (i : Fin n) :
                  i.castSucc i.succ

                  The generating arrow i ⟶ i+1 in the category Fin n.

                  Equations
                  Instances For