Documentation

Mathlib.Order.Category.BddLat

The category of bounded lattices #

This file defines BddLat, the category of bounded lattices.

In literature, this is sometimes called Lat, the category of lattices, because being a lattice is understood to entail having a bottom and a top element.

structure BddLat :
Type (u_1 + 1)

The category of bounded lattices with bounded lattice morphisms.

  • toLat : Lat

    The underlying lattice of a bounded lattice.

  • isBoundedOrder : BoundedOrder self.toLat
Instances For
    Equations
    instance BddLat.instLatticeαToLat (X : BddLat) :
    Lattice X.toLat
    Equations
    • X.instLatticeαToLat = X.toLat.str
    def BddLat.of (α : Type u_1) [Lattice α] [BoundedOrder α] :

    Construct a bundled BddLat from Lattice + BoundedOrder.

    Equations
    Instances For
      @[simp]
      theorem BddLat.coe_of (α : Type u_1) [Lattice α] [BoundedOrder α] :
      (BddLat.of α).toLat = α
      instance BddLat.instFunLike (X : BddLat) (Y : BddLat) :
      FunLike (X Y) X.toLat Y.toLat
      Equations
      • X.instFunLike Y = inferInstance
      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.
      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.
      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem BddLat.coe_forget_to_bddOrd (X : BddLat) :
      ((CategoryTheory.forget₂ BddLat BddOrd).obj X).toPartOrd = X.toLat
      @[simp]
      theorem BddLat.coe_forget_to_lat (X : BddLat) :
      ((CategoryTheory.forget₂ BddLat Lat).obj X) = X.toLat
      @[simp]
      theorem BddLat.Iso.mk_hom_toLatticeHom_toSupHom_toFun {α : BddLat} {β : BddLat} (e : α.toLat ≃o β.toLat) (a : α.toLat) :
      (BddLat.Iso.mk e).hom.toSupHom a = e a
      @[simp]
      theorem BddLat.Iso.mk_inv_toLatticeHom_toSupHom_toFun {α : BddLat} {β : BddLat} (e : α.toLat ≃o β.toLat) (a : β.toLat) :
      (BddLat.Iso.mk e).inv.toSupHom a = e.symm a
      def BddLat.Iso.mk {α : BddLat} {β : BddLat} (e : α.toLat ≃o β.toLat) :
      α β

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem BddLat.dual_map {X : BddLat} {Y : BddLat} (a : BoundedLatticeHom X.toLat Y.toLat) :
        BddLat.dual.map a = BoundedLatticeHom.dual a
        @[simp]
        theorem BddLat.dual_obj (X : BddLat) :
        BddLat.dual.obj X = BddLat.of (↑X.toLat)ᵒᵈ

        OrderDual as a functor.

        Equations
        Instances For

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

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

            The functor that adds a bottom and a top element to a lattice. This is the free functor.

            Equations
            Instances For

              latToBddLat is left adjoint to the forgetful functor, meaning it is the free functor from Lat to BddLat.

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