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.
Equations
- FinBoolAlg.instCoeSortType = { coe := fun (X : FinBoolAlg) => ↑X.toBoolAlg }
@[simp]
Equations
- FinBoolAlg.instInhabited = { default := FinBoolAlg.of PUnit.{?u.3 + 1} }
instance
FinBoolAlg.instBoundedLatticeHomClass
{X Y : FinBoolAlg}
:
BoundedLatticeHomClass (X ⟶ Y) ↑X.toBoolAlg ↑Y.toBoolAlg
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
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
OrderDual
as a functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
FinBoolAlg.dual_map
{x✝ x✝¹ : FinBoolAlg}
(a : BoundedLatticeHom ↑x✝.toBoolAlg.toBddDistLat.toBddLat.toLat ↑x✝¹.toBoolAlg.toBddDistLat.toBddLat.toLat)
:
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
The powerset functor. Set
as a functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
fintypeToFinBoolAlgOp_map
{X 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' := ⋯ })