Documentation

Mathlib.Order.Category.DistLat

The category of distributive lattices #

This file defines DistLat, the category of distributive lattices.

Note that DistLat in the literature doesn't always correspond to DistLat as we don't require bottom or top elements. Instead, this DistLat corresponds to BddDistLat.

def DistLat :
Type (u_1 + 1)

The category of distributive lattices.

Equations
Instances For
    Equations
    Equations
    • X.instDistribLatticeα = X.str
    def DistLat.of (α : Type u_1) [DistribLattice α] :

    Construct a bundled DistLat from a DistribLattice underlying type and typeclass.

    Equations
    Instances For
      @[simp]
      theorem DistLat.coe_of (α : Type u_1) [DistribLattice α] :
      (DistLat.of α) = α
      @[simp]
      theorem DistLat.Iso.mk_hom_toSupHom_toFun {α : DistLat} {β : DistLat} (e : α ≃o β) (a : α) :
      (DistLat.Iso.mk e).hom.toSupHom a = e a
      @[simp]
      theorem DistLat.Iso.mk_inv_toSupHom_toFun {α : DistLat} {β : DistLat} (e : α ≃o β) (a : β) :
      (DistLat.Iso.mk e).inv.toSupHom a = e.symm a
      def DistLat.Iso.mk {α : DistLat} {β : DistLat} (e : α ≃o β) :
      α β

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

      Equations
      • DistLat.Iso.mk e = { hom := { toFun := e, map_sup' := , map_inf' := }, inv := { toFun := e.symm, map_sup' := , map_inf' := }, hom_inv_id := , inv_hom_id := }
      Instances For
        @[simp]
        theorem DistLat.dual_map :
        ∀ {X Y : DistLat} (a : LatticeHom X Y), DistLat.dual.map a = LatticeHom.dual a
        @[simp]

        OrderDual as a functor.

        Equations
        Instances For

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

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