Documentation

Mathlib.Order.Category.Semilat

The categories of semilattices #

This defines SemilatSupCat and SemilatInfCat, the categories of sup-semilattices with a bottom element and inf-semilattices with a top element.

References #

structure SemilatSupCat :
Type (u + 1)

The category of sup-semilattices with a bottom element.

Instances For
    structure SemilatInfCat :
    Type (u + 1)

    The category of inf-semilattices with a top element.

    Instances For

      Construct a bundled SemilatSupCat from a SemilatticeSup.

      Equations
      Instances For
        @[simp]
        theorem SemilatSupCat.coe_of (α : Type u_1) [SemilatticeSup α] [OrderBot α] :
        instance SemilatSupCat.instFunLike (X : SemilatSupCat) (Y : SemilatSupCat) :
        FunLike (X Y) X.X fun (x : X.X) => Y.X
        Equations
        Equations
        • One or more equations did not get rendered due to their size.

        Construct a bundled SemilatInfCat from a SemilatticeInf.

        Equations
        Instances For
          @[simp]
          theorem SemilatInfCat.coe_of (α : Type u_1) [SemilatticeInf α] [OrderTop α] :
          instance SemilatInfCat.instFunLike (X : SemilatInfCat) (Y : SemilatInfCat) :
          FunLike (X Y) X.X fun (x : X.X) => Y.X
          Equations
          Equations
          • One or more equations did not get rendered due to their size.

          Order dual #

          @[simp]
          theorem SemilatSupCat.Iso.mk_hom_toSupHom_toFun {α : SemilatSupCat} {β : SemilatSupCat} (e : α.X ≃o β.X) (a : α.X) :
          (SemilatSupCat.Iso.mk e).hom.toSupHom a = e a
          @[simp]
          theorem SemilatSupCat.Iso.mk_inv_toSupHom_toFun {α : SemilatSupCat} {β : SemilatSupCat} (e : α.X ≃o β.X) (a : β.X) :
          (SemilatSupCat.Iso.mk e).inv.toSupHom a = (OrderIso.symm e) a
          def SemilatSupCat.Iso.mk {α : SemilatSupCat} {β : SemilatSupCat} (e : α.X ≃o β.X) :
          α β

          Constructs an isomorphism of lattices from an order isomorphism between them.

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

            OrderDual as a functor.

            Equations
            Instances For
              @[simp]
              theorem SemilatInfCat.Iso.mk_hom_toInfHom_toFun {α : SemilatInfCat} {β : SemilatInfCat} (e : α.X ≃o β.X) (a : α.X) :
              (SemilatInfCat.Iso.mk e).hom.toInfHom a = e a
              @[simp]
              theorem SemilatInfCat.Iso.mk_inv_toInfHom_toFun {α : SemilatInfCat} {β : SemilatInfCat} (e : α.X ≃o β.X) (a : β.X) :
              (SemilatInfCat.Iso.mk e).inv.toInfHom a = (OrderIso.symm e) a
              def SemilatInfCat.Iso.mk {α : SemilatInfCat} {β : SemilatInfCat} (e : α.X ≃o β.X) :
              α β

              Constructs an isomorphism of lattices from an order isomorphism between them.

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

                OrderDual as a functor.

                Equations
                Instances For

                  The equivalence between SemilatSupCat and SemilatInfCat induced by OrderDual both ways.

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