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.

source
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
    source
    instance BddDistLat.instCoeSortBddDistLatType :
    CoeSort BddDistLat (Type u_1)
    Equations
    source
    instance BddDistLat.instDistribLatticeαToDistLat (X : BddDistLat) :
    DistribLattice ↑X.toDistLat
    Equations
    source
    def BddDistLat.of (α : Type u_1) [DistribLattice α] [BoundedOrder α] :
    BddDistLat

    Construct a bundled BddDistLat from a BoundedOrder DistribLattice.

    Equations
    Instances For
      source
      @[simp]
      theorem BddDistLat.coe_of (α : Type u_1) [DistribLattice α] [BoundedOrder α] :
      ↑(BddDistLat.of α).toDistLat = α
      source
      instance BddDistLat.instInhabitedBddDistLat :
      Inhabited BddDistLat
      Equations
      source
      def BddDistLat.toBddLat (X : BddDistLat) :
      BddLat

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

      Equations
      Instances For
        source
        @[simp]
        theorem BddDistLat.coe_toBddLat (X : BddDistLat) :
        ↑(BddDistLat.toBddLat X).toLat = ↑X.toDistLat
        source
        instance BddDistLat.instLargeCategoryBddDistLat :
        CategoryTheory.LargeCategory BddDistLat
        Equations
        source
        instance BddDistLat.instConcreteCategoryBddDistLatInstLargeCategoryBddDistLat :
        CategoryTheory.ConcreteCategory BddDistLat
        Equations
        source
        instance BddDistLat.hasForgetToDistLat :
        CategoryTheory.HasForget₂ BddDistLat DistLat
        Equations
        • One or more equations did not get rendered due to their size.
        source
        instance BddDistLat.hasForgetToBddLat :
        CategoryTheory.HasForget₂ BddDistLat BddLat
        Equations
        source
        theorem BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat :
        CategoryTheory.Functor.comp (CategoryTheory.forget₂ BddDistLat BddLat) (CategoryTheory.forget₂ BddLat Lat) = CategoryTheory.Functor.comp (CategoryTheory.forget₂ BddDistLat DistLat) (CategoryTheory.forget₂ DistLat Lat)
        source
        @[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
        source
        @[simp]
        theorem BddDistLat.Iso.mk_inv_toLatticeHom_toSupHom_toFun {α : BddDistLat} {β : BddDistLat} (e : ↑α.toDistLat ≃o ↑β.toDistLat) (a : ↑β.toDistLat) :
        (BddDistLat.Iso.mk e).inv.toSupHom a = (OrderIso.symm e) a
        source
        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
          source
          @[simp]
          theorem BddDistLat.dual_obj (X : BddDistLat) :
          BddDistLat.dual.obj X = BddDistLat.of (↑X.toDistLat)ᵒᵈ
          source
          @[simp]
          theorem BddDistLat.dual_map {X : BddDistLat} {Y : BddDistLat} (a : BoundedLatticeHom ↑(BddDistLat.toBddLat X).toLat ↑(BddDistLat.toBddLat Y).toLat) :
          BddDistLat.dual.map a = BoundedLatticeHom.dual a
          source
          def BddDistLat.dual :
          CategoryTheory.Functor BddDistLat BddDistLat

          OrderDual as a functor.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem BddDistLat.dualEquiv_inverse :
            BddDistLat.dualEquiv.inverse = BddDistLat.dual
            source
            @[simp]
            theorem BddDistLat.dualEquiv_functor :
            BddDistLat.dualEquiv.functor = BddDistLat.dual
            source
            def BddDistLat.dualEquiv :
            BddDistLat ≌ BddDistLat

            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
              source
              theorem bddDistLat_dual_comp_forget_to_distLat :
              CategoryTheory.Functor.comp BddDistLat.dual (CategoryTheory.forget₂ BddDistLat DistLat) = CategoryTheory.Functor.comp (CategoryTheory.forget₂ BddDistLat DistLat) DistLat.dual