# 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.toBoolAlg.str
def FinBoolAlg.of (α : Type u_1) [] [] :

Construct a bundled FinBoolAlg from BooleanAlgebra + Fintype.

Equations
Instances For
@[simp]
theorem FinBoolAlg.coe_of (α : Type u_1) [] [] :
().toBoolAlg = α
instance FinBoolAlg.instBoundedLatticeHomClass {X : FinBoolAlg} {Y : FinBoolAlg} :
BoundedLatticeHomClass (X Y) X.toBoolAlg Y.toBoolAlg
Equations
• FinBoolAlg.instBoundedLatticeHomClass = BoundedLatticeHom.instBoundedLatticeHomClass
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_inv_toLatticeHom_toSupHom_toFun {α : FinBoolAlg} {β : FinBoolAlg} (e : α.toBoolAlg ≃o β.toBoolAlg) (a : β.toBoolAlg) :
.inv.toSupHom a = () a
@[simp]
theorem FinBoolAlg.Iso.mk_hom_toLatticeHom_toSupHom_toFun {α : FinBoolAlg} {β : FinBoolAlg} (e : α.toBoolAlg ≃o β.toBoolAlg) (a : α.toBoolAlg) :
.hom.toSupHom a = e 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 (BddDistLat.toBddLat (BoolAlg.toBddDistLat X.toBoolAlg)).toLat (BddDistLat.toBddLat (BoolAlg.toBddDistLat Y.toBoolAlg)).toLat) :
FinBoolAlg.dual.map a = BoundedLatticeHom.dual a

OrderDual as a functor.

Equations
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) :
= (let src := { toSupHom := { toFun := , map_sup' := (_ : ∀ (a b : Set Y), (a b) = ) }, map_inf' := (_ : ∀ (a b : Set Y), (a b) = ) }; { toLatticeHom := { toSupHom := { toFun := , map_sup' := (_ : ∀ (a b : Set Y), SupHom.toFun { toSupHom := { toFun := , map_sup' := (_ : ∀ (a b : Set Y), (a b) = ) }, map_inf' := (_ : ∀ (a b : Set Y), (a b) = ) }.toSupHom (a b) = SupHom.toFun { toSupHom := { toFun := , map_sup' := (_ : ∀ (a b : Set Y), (a b) = ) }, map_inf' := (_ : ∀ (a b : Set Y), (a b) = ) }.toSupHom a SupHom.toFun { toSupHom := { toFun := , map_sup' := (_ : ∀ (a b : Set Y), (a b) = ) }, map_inf' := (_ : ∀ (a b : Set Y), (a b) = ) }.toSupHom b) }, map_inf' := (_ : ∀ (a b : Set Y), SupHom.toFun { toSupHom := { toFun := , map_sup' := (_ : ∀ (a b : Set Y), (a b) = ) }, map_inf' := (_ : ∀ (a b : Set Y), (a b) = ) }.toSupHom (a b) = SupHom.toFun { toSupHom := { toFun := , map_sup' := (_ : ∀ (a b : Set Y), (a b) = ) }, map_inf' := (_ : ∀ (a b : Set Y), (a b) = ) }.toSupHom a SupHom.toFun { toSupHom := { toFun := , map_sup' := (_ : ∀ (a b : Set Y), (a b) = ) }, map_inf' := (_ : ∀ (a b : Set Y), (a b) = ) }.toSupHom b) }, map_top' := (_ : ), map_bot' := (_ : ) }).op

The powerset functor. Set as a functor.

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