Documentation

Mathlib.Order.Category.PartOrd

Category of partial orders #

This defines PartOrd, the category of partial orders with monotone maps.

source
structure PartOrd :
Type (u_1 + 1)

The category of partial orders.

  • of :: (
    • carrier : Type u_1

      The underlying partially ordered type.

    • str : PartialOrder ↑self
  • )
Instances For
    source
    @[implicit_reducible]
    instance PartOrd.instCoeSortType :
    CoeSort PartOrd (Type u_1)
    source
    structure PartOrd.Hom (X Y : PartOrd) :
    Type u

    The type of morphisms in PartOrd R.

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

      Turn a morphism in PartOrd back into a OrderHom.

      Instances For
        source
        @[reducible, inline]
        abbrev PartOrd.ofHom {X Y : Type u} [PartialOrder X] [PartialOrder Y] (f : X →o Y) :
        { carrier := X, str := inst✝ } ⟶ { carrier := Y, str := inst✝¹ }

        Typecheck a OrderHom as a morphism in PartOrd.

        Instances For
          source
          def PartOrd.Hom.Simps.hom (X Y : PartOrd) (f : X.Hom Y) :
          ↑X →o ↑Y

          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 PartOrd.coe_id {X : PartOrd} :
            ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
            source
            @[simp]
            theorem PartOrd.coe_comp {X Y Z : PartOrd} {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 PartOrd.forget_map {X Y : PartOrd} (f : X ⟶ Y) :
            (CategoryTheory.forget PartOrd).map f = ⇑(CategoryTheory.ConcreteCategory.hom f)
            source
            theorem PartOrd.ext {X Y : PartOrd} {f g : X ⟶ Y} (w : ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) :
            f = g
            source
            theorem PartOrd.ext_iff {X Y : PartOrd} {f g : X ⟶ Y} :
            f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
            source
            theorem PartOrd.coe_of (X : Type u) [PartialOrder X] :
            ↑{ carrier := X, str := inst✝ } = X
            source
            @[simp]
            theorem PartOrd.hom_id {X : PartOrd} :
            Hom.hom (CategoryTheory.CategoryStruct.id X) = OrderHom.id
            source
            theorem PartOrd.id_apply (X : PartOrd) (x : ↑X) :
            (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
            source
            @[simp]
            theorem PartOrd.hom_comp {X Y Z : PartOrd} (f : X ⟶ Y) (g : Y ⟶ Z) :
            Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)
            source
            theorem PartOrd.comp_apply {X Y Z : PartOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X) :
            (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
            source
            theorem PartOrd.hom_ext {X Y : PartOrd} {f g : X ⟶ Y} (hf : Hom.hom f = Hom.hom g) :
            f = g
            source
            theorem PartOrd.hom_ext_iff {X Y : PartOrd} {f g : X ⟶ Y} :
            f = g ↔ Hom.hom f = Hom.hom g
            source
            @[simp]
            theorem PartOrd.hom_ofHom {X Y : Type u} [PartialOrder X] [PartialOrder Y] (f : X →o Y) :
            Hom.hom (ofHom f) = f
            source
            @[simp]
            theorem PartOrd.ofHom_hom {X Y : PartOrd} (f : X ⟶ Y) :
            ofHom (Hom.hom f) = f
            source
            @[simp]
            theorem PartOrd.ofHom_id {X : Type u} [PartialOrder X] :
            ofHom OrderHom.id = CategoryTheory.CategoryStruct.id { carrier := X, str := inst✝ }
            source
            @[simp]
            theorem PartOrd.ofHom_comp {X Y Z : Type u} [PartialOrder X] [PartialOrder Y] [PartialOrder Z] (f : X →o Y) (g : Y →o Z) :
            ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)
            source
            theorem PartOrd.ofHom_apply {X Y : Type u} [PartialOrder X] [PartialOrder Y] (f : X →o Y) (x : X) :
            (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x
            source
            theorem PartOrd.inv_hom_apply {X Y : PartOrd} (e : X ≅ Y) (x : ↑X) :
            (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
            source
            theorem PartOrd.hom_inv_apply {X Y : PartOrd} (e : X ≅ Y) (s : ↑Y) :
            (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
            source
            @[implicit_reducible]
            instance PartOrd.hasForgetToPreord :
            CategoryTheory.HasForget₂ PartOrd Preord
            source
            def PartOrd.Iso.mk {α β : PartOrd} (e : ↑α ≃o ↑β) :
            α ≅ β

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

            Instances For
              source
              @[simp]
              theorem PartOrd.Iso.mk_hom {α β : PartOrd} (e : ↑α ≃o ↑β) :
              (mk e).hom = ofHom ↑e
              source
              @[simp]
              theorem PartOrd.Iso.mk_inv {α β : PartOrd} (e : ↑α ≃o ↑β) :
              (mk e).inv = ofHom ↑e.symm
              source
              def PartOrd.dual :
              CategoryTheory.Functor PartOrd PartOrd

              OrderDual as a functor.

              Instances For
                source
                @[simp]
                theorem PartOrd.dual_map {X✝ Y✝ : PartOrd} (f : X✝ ⟶ Y✝) :
                dual.map f = ofHom (OrderHom.dual (Hom.hom f))
                source
                def PartOrd.dualEquiv :
                PartOrd ≌ PartOrd

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

                Instances For
                  source
                  @[simp]
                  theorem PartOrd.dualEquiv_inverse :
                  dualEquiv.inverse = dual
                  source
                  @[simp]
                  theorem PartOrd.dualEquiv_functor :
                  dualEquiv.functor = dual
                  source
                  theorem partOrd_dual_comp_forget_to_preord :
                  PartOrd.dual.comp (CategoryTheory.forget₂ PartOrd Preord) = (CategoryTheory.forget₂ PartOrd Preord).comp Preord.dual
                  source
                  def preordToPartOrd :
                  CategoryTheory.Functor Preord PartOrd

                  Antisymmetrization as a functor. It is the free functor.

                  Instances For
                    source
                    def preordToPartOrdForgetAdjunction :
                    preordToPartOrd ⊣ CategoryTheory.forget₂ PartOrd Preord

                    preordToPartOrd is left adjoint to the forgetful functor, meaning it is the free functor from Preord to PartOrd.

                    Instances For
                      source
                      def preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd :
                      preordToPartOrd.comp PartOrd.dual ≅ Preord.dual.comp preordToPartOrd

                      PreordToPartOrd and OrderDual commute.

                      Instances For
                        source
                        theorem preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_hom_coe (X : Preord) (a : ↑((preordToPartOrd.comp PartOrd.dual).obj X)) :
                        (PartOrd.Hom.hom (preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.hom.app X)) a = (OrderIso.dualAntisymmetrization ↑X) a
                        source
                        theorem preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe (X : Preord) (a : ↑((Preord.dual.comp preordToPartOrd).obj X)) :
                        (PartOrd.Hom.hom (preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.inv.app X)) a = (OrderIso.dualAntisymmetrization ↑X).symm a
                        source
                        @[simp]
                        theorem preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe' (X : Preord) (a : ↑(preordToPartOrd.obj (Preord.dual.obj X))) :
                        (PartOrd.Hom.hom (preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.inv.app X)) a = (OrderIso.dualAntisymmetrization ↑X).symm a