Documentation

Mathlib.Order.Category.FinBoolAlg

The category of finite boolean algebras #

This file defines FinBoolAlg, the category of finite boolean algebras.

TODO #

Birkhoff's representation for finite Boolean algebras.

FintypeCat_to_FinBoolAlg_op.left_op ⋙ FinBoolAlg.dual ≅
FintypeCat_to_FinBoolAlg_op.left_op

FinBoolAlg is essentially small.

structure FinBoolAlg :
Type (u_1 + 1)

The category of finite boolean algebras with bounded lattice morphisms.

Instances For
    Equations
    Equations
    • X.instBooleanAlgebraαToBoolAlg = X.toBoolAlg.str

    Construct a bundled FinBoolAlg from BooleanAlgebra + Fintype.

    Equations
    Instances For
      @[simp]
      theorem FinBoolAlg.coe_of (α : Type u_1) [BooleanAlgebra α] [Fintype α] :
      (FinBoolAlg.of α).toBoolAlg = α
      instance FinBoolAlg.instFunLike {X : FinBoolAlg} {Y : FinBoolAlg} :
      FunLike (X Y) X.toBoolAlg Y.toBoolAlg
      Equations
      • FinBoolAlg.instFunLike = BoundedLatticeHom.instFunLike
      instance FinBoolAlg.instBoundedLatticeHomClass {X : FinBoolAlg} {Y : FinBoolAlg} :
      BoundedLatticeHomClass (X Y) X.toBoolAlg Y.toBoolAlg
      Equations
      • =
      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem FinBoolAlg.hasForgetToFinPartOrd_forget₂_map {X : FinBoolAlg} {Y : FinBoolAlg} (f : X Y) :
      CategoryTheory.HasForget₂.forget₂.map f = let_fun this := (let_fun this := f; this); this
      @[simp]
      theorem FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj (X : FinBoolAlg) :
      CategoryTheory.HasForget₂.forget₂.obj X = FinPartOrd.of X.toBoolAlg
      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem FinBoolAlg.Iso.mk_hom_toLatticeHom_toSupHom_toFun {α : FinBoolAlg} {β : FinBoolAlg} (e : α.toBoolAlg ≃o β.toBoolAlg) (a : α.toBoolAlg) :
      (FinBoolAlg.Iso.mk e).hom.toSupHom a = e a
      @[simp]
      theorem FinBoolAlg.Iso.mk_inv_toLatticeHom_toSupHom_toFun {α : FinBoolAlg} {β : FinBoolAlg} (e : α.toBoolAlg ≃o β.toBoolAlg) (a : β.toBoolAlg) :
      (FinBoolAlg.Iso.mk e).inv.toSupHom a = e.symm a
      def FinBoolAlg.Iso.mk {α : FinBoolAlg} {β : FinBoolAlg} (e : α.toBoolAlg ≃o β.toBoolAlg) :
      α β

      Constructs an equivalence between finite 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 FinBoolAlg.dual_map {X : FinBoolAlg} {Y : FinBoolAlg} (a : BoundedLatticeHom X.toBoolAlg.toBddDistLat.toBddLat.toLat Y.toBoolAlg.toBddDistLat.toBddLat.toLat) :
        FinBoolAlg.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 FinBoolAlg and itself induced by OrderDual both ways.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem fintypeToFinBoolAlgOp_map {X : FintypeCat} {Y : FintypeCat} (f : X Y) :
            fintypeToFinBoolAlgOp.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 functor.

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