Documentation

Mathlib.Order.Category.BddDistLat

The category of bounded distributive lattices #

This defines BddDistLat, the category of bounded distributive lattices.

Note that this category is sometimes called DistLat when being a lattice is understood to entail having a bottom and a top element.

structure BddDistLat :
Type (u_1 + 1)

The category of bounded distributive lattices with bounded lattice morphisms.

  • toDistLat : DistLat

    The underlying distrib lattice of a bounded distributive lattice.

  • isBoundedOrder : BoundedOrder self.toDistLat
Instances For
    Equations
    Equations
    • X.instDistribLatticeαToDistLat = X.toDistLat.str

    Construct a bundled BddDistLat from a BoundedOrder DistribLattice.

    Equations
    Instances For
      @[simp]
      theorem BddDistLat.coe_of (α : Type u_1) [DistribLattice α] [BoundedOrder α] :
      (BddDistLat.of α).toDistLat = α

      Turn a BddDistLat into a BddLat by forgetting it is distributive.

      Equations
      Instances For
        @[simp]
        theorem BddDistLat.coe_toBddLat (X : BddDistLat) :
        X.toBddLat.toLat = X.toDistLat
        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem BddDistLat.Iso.mk_hom_toLatticeHom_toSupHom_toFun {α : BddDistLat} {β : BddDistLat} (e : α.toDistLat ≃o β.toDistLat) (a : α.toDistLat) :
        (BddDistLat.Iso.mk e).hom.toSupHom a = e a
        @[simp]
        theorem BddDistLat.Iso.mk_inv_toLatticeHom_toSupHom_toFun {α : BddDistLat} {β : BddDistLat} (e : α.toDistLat ≃o β.toDistLat) (a : β.toDistLat) :
        (BddDistLat.Iso.mk e).inv.toSupHom a = e.symm a
        def BddDistLat.Iso.mk {α : BddDistLat} {β : BddDistLat} (e : α.toDistLat ≃o β.toDistLat) :
        α β

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

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

          OrderDual as a functor.

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

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

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