Documentation

Mathlib.Order.Category.BddOrd

The category of bounded orders #

This defines BddOrd, the category of bounded orders.

source
structure BddOrdextends PartOrd :
Type (u_1 + 1)

The category of bounded orders with monotone functions.

Instances For
    source
    @[implicit_reducible]
    instance BddOrd.instCoeSortType :
    CoeSort BddOrd (Type u_1)
    source
    @[reducible, inline]
    abbrev BddOrd.of (X : Type u_1) [PartialOrder X] [BoundedOrder X] :
    BddOrd

    Construct a bundled BddOrd from the underlying type and typeclass.

    Instances For
      source
      structure BddOrd.Hom (X Y : BddOrd) :
      Type u

      The type of morphisms in BddOrd R.

      Instances For
        source
        theorem BddOrd.Hom.ext_iff {X Y : BddOrd} {x y : X.Hom Y} :
        x = y ↔ x.hom' = y.hom'
        source
        theorem BddOrd.Hom.ext {X Y : BddOrd} {x y : X.Hom Y} (hom' : x.hom' = y.hom') :
        x = y
        source
        @[implicit_reducible]
        instance BddOrd.instCategory :
        CategoryTheory.Category.{u, u + 1} BddOrd
        source
        @[implicit_reducible]
        instance BddOrd.instConcreteCategoryBoundedOrderHomCarrier :
        CategoryTheory.ConcreteCategory BddOrd fun (x1 x2 : BddOrd) => BoundedOrderHom ↑x1.toPartOrd ↑x2.toPartOrd
        source
        @[reducible, inline]
        abbrev BddOrd.Hom.hom {X Y : BddOrd} (f : X.Hom Y) :
        BoundedOrderHom ↑X.toPartOrd ↑Y.toPartOrd

        Turn a morphism in BddOrd back into a BoundedOrderHom.

        Instances For
          source
          @[reducible, inline]
          abbrev BddOrd.ofHom {X Y : Type u} [PartialOrder X] [BoundedOrder X] [PartialOrder Y] [BoundedOrder Y] (f : BoundedOrderHom X Y) :
          of X ⟶ of Y

          Typecheck a BoundedOrderHom as a morphism in BddOrd.

          Instances For
            source
            def BddOrd.Hom.Simps.hom (X Y : BddOrd) (f : X.Hom Y) :
            BoundedOrderHom ↑X.toPartOrd ↑Y.toPartOrd

            Use the ConcreteCategory.hom projection for @[simps] lemmas.

            Instances For

              The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

              source
              @[simp]
              theorem BddOrd.coe_id {X : BddOrd} :
              ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
              source
              @[simp]
              theorem BddOrd.coe_comp {X Y Z : BddOrd} {f : X ⟶ Y} {g : Y ⟶ Z} :
              ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
              source
              @[simp]
              theorem BddOrd.forget_map {X Y : BddOrd} (f : X ⟶ Y) :
              (CategoryTheory.forget BddOrd).map f = ⇑(CategoryTheory.ConcreteCategory.hom f)
              source
              theorem BddOrd.ext {X Y : BddOrd} {f g : X ⟶ Y} (w : ∀ (x : ↑X.toPartOrd), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) :
              f = g
              source
              theorem BddOrd.ext_iff {X Y : BddOrd} {f g : X ⟶ Y} :
              f = g ↔ ∀ (x : ↑X.toPartOrd), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
              source
              theorem BddOrd.coe_of (X : Type u) [PartialOrder X] [BoundedOrder X] :
              ↑(of X).toPartOrd = X
              source
              @[simp]
              theorem BddOrd.hom_id {X : BddOrd} :
              Hom.hom (CategoryTheory.CategoryStruct.id X) = BoundedOrderHom.id ↑X.toPartOrd
              source
              theorem BddOrd.id_apply (X : BddOrd) (x : ↑X.toPartOrd) :
              (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
              source
              @[simp]
              theorem BddOrd.hom_comp {X Y Z : BddOrd} (f : X ⟶ Y) (g : Y ⟶ Z) :
              Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)
              source
              theorem BddOrd.comp_apply {X Y Z : BddOrd} (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 BddOrd.hom_ext {X Y : BddOrd} {f g : X ⟶ Y} (hf : Hom.hom f = Hom.hom g) :
              f = g
              source
              theorem BddOrd.hom_ext_iff {X Y : BddOrd} {f g : X ⟶ Y} :
              f = g ↔ Hom.hom f = Hom.hom g
              source
              @[simp]
              theorem BddOrd.hom_ofHom {X Y : Type u} [PartialOrder X] [BoundedOrder X] [PartialOrder Y] [BoundedOrder Y] (f : BoundedOrderHom X Y) :
              Hom.hom (ofHom f) = f
              source
              @[simp]
              theorem BddOrd.ofHom_hom {X Y : BddOrd} (f : X ⟶ Y) :
              ofHom (Hom.hom f) = f
              source
              @[simp]
              theorem BddOrd.ofHom_id {X : Type u} [PartialOrder X] [BoundedOrder X] :
              ofHom (BoundedOrderHom.id X) = CategoryTheory.CategoryStruct.id (of X)
              source
              @[simp]
              theorem BddOrd.ofHom_comp {X Y Z : Type u} [PartialOrder X] [BoundedOrder X] [PartialOrder Y] [BoundedOrder Y] [PartialOrder Z] [BoundedOrder Z] (f : BoundedOrderHom X Y) (g : BoundedOrderHom Y Z) :
              ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)
              source
              theorem BddOrd.ofHom_apply {X Y : Type u} [PartialOrder X] [BoundedOrder X] [PartialOrder Y] [BoundedOrder Y] (f : BoundedOrderHom X Y) (x : X) :
              (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x
              source
              theorem BddOrd.inv_hom_apply {X Y : BddOrd} (e : X ≅ Y) (x : ↑X.toPartOrd) :
              (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
              source
              theorem BddOrd.hom_inv_apply {X Y : BddOrd} (e : X ≅ Y) (s : ↑Y.toPartOrd) :
              (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
              source
              @[implicit_reducible]
              instance BddOrd.instInhabited :
              Inhabited BddOrd
              source
              @[implicit_reducible]
              instance BddOrd.hasForgetToPartOrd :
              CategoryTheory.HasForget₂ BddOrd PartOrd
              source
              @[implicit_reducible]
              instance BddOrd.hasForgetToBipointed :
              CategoryTheory.HasForget₂ BddOrd Bipointed
              source
              def BddOrd.dual :
              CategoryTheory.Functor BddOrd BddOrd

              OrderDual as a functor.

              Instances For
                source
                @[simp]
                theorem BddOrd.dual_map {X✝ Y✝ : BddOrd} (f : X✝ ⟶ Y✝) :
                dual.map f = ofHom (BoundedOrderHom.dual (Hom.hom f))
                source
                def BddOrd.Iso.mk {α β : BddOrd} (e : ↑α.toPartOrd ≃o ↑β.toPartOrd) :
                α ≅ β

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

                Instances For
                  source
                  @[simp]
                  theorem BddOrd.Iso.mk_inv {α β : BddOrd} (e : ↑α.toPartOrd ≃o ↑β.toPartOrd) :
                  (mk e).inv = ofHom ↑e.symm
                  source
                  @[simp]
                  theorem BddOrd.Iso.mk_hom {α β : BddOrd} (e : ↑α.toPartOrd ≃o ↑β.toPartOrd) :
                  (mk e).hom = ofHom ↑e
                  source
                  def BddOrd.dualEquiv :
                  BddOrd ≌ BddOrd

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

                  Instances For
                    source
                    @[simp]
                    theorem BddOrd.dualEquiv_functor :
                    dualEquiv.functor = dual
                    source
                    @[simp]
                    theorem BddOrd.dualEquiv_inverse :
                    dualEquiv.inverse = dual
                    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