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.

  • X : Type u

    The underlying type of a sup-semilattice with a bottom element.

  • isSemilatticeSup : SemilatticeSup self.X
  • isOrderBot : OrderBot self.X
Instances For
    structure SemilatInfCat :
    Type (u + 1)

    The category of inf-semilattices with a top element.

    • X : Type u

      The underlying type of an inf-semilattice with a top element.

    • isSemilatticeInf : SemilatticeInf self.X
    • isOrderTop : OrderTop self.X
    Instances For

      Construct a bundled SemilatSupCat from a SemilatticeSup.

      Equations
      Instances For
        @[simp]
        theorem SemilatSupCat.coe_of (α : Type u_1) [SemilatticeSup α] [OrderBot α] :
        Equations
        • X.instFunLike Y = let_fun this := inferInstance; this
        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 SemilatInfCat from a SemilatticeInf.

        Equations
        Instances For
          @[simp]
          theorem SemilatInfCat.coe_of (α : Type u_1) [SemilatticeInf α] [OrderTop α] :
          Equations
          • X.instFunLike Y = let_fun this := inferInstance; this
          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.

          Order dual #

          @[simp]
          theorem SemilatSupCat.Iso.mk_inv_toSupHom_toFun {α : SemilatSupCat} {β : SemilatSupCat} (e : α.X ≃o β.X) (a : β.X) :
          (SemilatSupCat.Iso.mk e).inv.toSupHom a = e.symm a
          @[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
          def SemilatSupCat.Iso.mk {α : SemilatSupCat} {β : SemilatSupCat} (e : α.X ≃o β.X) :
          α β

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

          Equations
          • SemilatSupCat.Iso.mk e = { hom := { toFun := e, map_sup' := , map_bot' := }, inv := { toFun := e.symm, map_sup' := , map_bot' := }, hom_inv_id := , inv_hom_id := }
          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
            • One or more equations did not get rendered due to their size.
            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 = e.symm a
              def SemilatInfCat.Iso.mk {α : SemilatInfCat} {β : SemilatInfCat} (e : α.X ≃o β.X) :
              α β

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

              Equations
              • SemilatInfCat.Iso.mk e = { hom := { toFun := e, map_inf' := , map_top' := }, inv := { toFun := e.symm, map_inf' := , map_top' := }, hom_inv_id := , inv_hom_id := }
              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
                • One or more equations did not get rendered due to their size.
                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