# mathlib3documentation

order.category.BoolAlg

# The category of boolean algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This defines BoolAlg, the category of boolean algebras.

def BoolAlg  :
Type (u_1+1)

The category of boolean algebras.

Equations
Instances for BoolAlg
@[protected, instance]
Equations
@[protected, instance]
Equations
def BoolAlg.of (α : Type u_1)  :

Construct a bundled BoolAlg from a boolean_algebra.

Equations
@[simp]
theorem BoolAlg.coe_of (α : Type u_1)  :
@[protected, instance]
Equations

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

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
@[protected, instance]
Equations
@[simp]
@[simp]
theorem BoolAlg.has_forget_to_HeytAlg_forget₂_map (X Y : BoolAlg) (f : X Y) :
= ((λ (this : bounded_lattice_hom X Y), this) f)
def BoolAlg.iso.mk {α β : BoolAlg} (e : α ≃o β) :
α β

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

Equations
@[simp]
theorem BoolAlg.iso.mk_inv {α β : BoolAlg} (e : α ≃o β) :
@[simp]
theorem BoolAlg.iso.mk_hom {α β : BoolAlg} (e : α ≃o β) :
@[simp]
theorem BoolAlg.dual_obj (X : BoolAlg) :
@[simp]
theorem BoolAlg.dual_map (X Y : BoolAlg)  :

order_dual as a functor.

Equations
@[simp]

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

Equations
@[simp]