Documentation

Mathlib.Order.Category.FinBddDistLat

The category of finite bounded distributive lattices #

This file defines FinBddDistLat, the category of finite distributive lattices with bounded lattice homomorphisms.

structure FinBddDistLat :
Type (u_1 + 1)

The category of finite distributive lattices with bounded lattice morphisms.

Instances For
    Equations
    Equations
    • X.instDistribLatticeαToDistLatToBddDistLat = X.toBddDistLat.toDistLat.str
    Equations
    • X.instBoundedOrderαDistribLatticeToDistLatToBddDistLat = X.toBddDistLat.isBoundedOrder

    Construct a bundled FinBddDistLat from a Nonempty BoundedOrder DistribLattice.

    Equations
    Instances For

      Construct a bundled FinBddDistLat from a Nonempty BoundedOrder DistribLattice.

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

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem FinBddDistLat.dual_obj (X : FinBddDistLat) :
          FinBddDistLat.dual.obj X = FinBddDistLat.of (↑X.toBddDistLat.toDistLat)ᵒᵈ
          @[simp]
          theorem FinBddDistLat.dual_map :
          ∀ {x x_1 : FinBddDistLat} (a : BoundedLatticeHom x.toBddDistLat.toBddLat.toLat x_1.toBddDistLat.toBddLat.toLat), FinBddDistLat.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 FinBddDistLat and itself induced by OrderDual both ways.

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