mathlib3 documentation

order.category.FinBoolAlg

The category of finite boolean algebras #

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

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

TODO #

Birkhoff's representation for finite Boolean algebras.

Fintype_to_FinBoolAlg_op.left_op ⋙ FinBoolAlg.dual ≅ Fintype_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 FinBoolAlg
@[protected, instance]
Equations
def FinBoolAlg.of (α : Type u_1) [boolean_algebra α] [fintype α] :

Construct a bundled FinBoolAlg from boolean_algebra + fintype.

Equations
@[simp]
theorem FinBoolAlg.coe_of (α : Type u_1) [boolean_algebra α] [fintype α] :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem FinBoolAlg.iso.mk_hom {α β : FinBoolAlg} (e : α ≃o β) :
@[simp]
theorem FinBoolAlg.iso.mk_inv {α β : FinBoolAlg} (e : α ≃o β) :
def FinBoolAlg.iso.mk {α β : FinBoolAlg} (e : α ≃o β) :
α β

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

Equations

order_dual as a functor.

Equations

The powerset functor. set as a functor.

Equations