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

Construct a bundled BoolAlg from a BooleanAlgebra.

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

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

Equations
Instances For
@[simp]
theorem BoolAlg.coe_toBddDistLat (X : BoolAlg) :
.toDistLat = X
@[simp]
theorem BoolAlg.hasForgetToHeytAlg_forget₂_obj_α (X : BoolAlg) :
(CategoryTheory.HasForget₂.forget₂.obj X) = 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 : ) (a : X) :
(CategoryTheory.HasForget₂.forget₂.map f) a = f a
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem BoolAlg.Iso.mk_inv_toLatticeHom_toSupHom_toFun {α : BoolAlg} {β : BoolAlg} (e : α ≃o β) (a : β) :
().inv.toSupHom a = () a
@[simp]
theorem BoolAlg.Iso.mk_hom_toLatticeHom_toSupHom_toFun {α : BoolAlg} {β : BoolAlg} (e : α ≃o β) (a : α) :
().hom.toSupHom a = e 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 .toLat .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