Documentation

Mathlib.Order.Category.BoolAlg

The category of boolean algebras #

This defines BoolAlg, the category of boolean algebras.

def BoolAlg :
Type (u_1 + 1)

The category of boolean algebras.

Equations
Instances For
    Equations
    Equations
    • X.instBooleanAlgebra = X.str
    def BoolAlg.of (α : Type u_1) [BooleanAlgebra α] :

    Construct a bundled BoolAlg from a BooleanAlgebra.

    Equations
    Instances For
      @[simp]
      theorem BoolAlg.coe_of (α : Type u_1) [BooleanAlgebra α] :
      (BoolAlg.of α) = α

      Turn a BoolAlg into a BddDistLat by forgetting its complement operation.

      Equations
      Instances For
        @[simp]
        theorem BoolAlg.coe_toBddDistLat (X : BoolAlg) :
        X.toBddDistLat.toDistLat = X
        @[simp]
        theorem BoolAlg.hasForgetToHeytAlg_forget₂_obj_str (X : BoolAlg) :
        (CategoryTheory.HasForget₂.forget₂.obj X).str = inferInstance
        @[simp]
        theorem BoolAlg.hasForgetToHeytAlg_forget₂_map_toFun {X : BoolAlg} {Y : BoolAlg} (f : BoundedLatticeHom X Y) (a : X) :
        (CategoryTheory.HasForget₂.forget₂.map f) a = f a
        @[simp]
        theorem BoolAlg.hasForgetToHeytAlg_forget₂_obj_α (X : BoolAlg) :
        (CategoryTheory.HasForget₂.forget₂.obj X) = X
        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem BoolAlg.Iso.mk_hom_toLatticeHom_toSupHom_toFun {α : BoolAlg} {β : BoolAlg} (e : α ≃o β) (a : α) :
        (BoolAlg.Iso.mk e).hom.toSupHom a = e a
        @[simp]
        theorem BoolAlg.Iso.mk_inv_toLatticeHom_toSupHom_toFun {α : BoolAlg} {β : BoolAlg} (e : α ≃o β) (a : β) :
        (BoolAlg.Iso.mk e).inv.toSupHom a = e.symm a
        def BoolAlg.Iso.mk {α : BoolAlg} {β : BoolAlg} (e : α ≃o β) :
        α β

        Constructs an equivalence between Boolean algebras from an order isomorphism between them.

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

          OrderDual as a functor.

          Equations
          Instances For

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

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem typeToBoolAlgOp_map {X : Type u} {Y : Type u} (f : X Y) :
              typeToBoolAlgOp.map f = Quiver.Hom.op (let __src := { toFun := (CompleteLatticeHom.setPreimage f), map_sup' := , map_inf' := }; { toFun := (CompleteLatticeHom.setPreimage f), map_sup' := , map_inf' := , map_top' := , map_bot' := })

              The powerset functor. Set as a contravariant functor.

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