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.
The category of finite boolean algebras with bounded lattice morphisms.
Instances For
Equations
- FinBoolAlg.instCoeSortType = { coe := fun (X : FinBoolAlg) => ↑X.toBoolAlg }
Equations
- X.instBooleanAlgebraαToBoolAlg = X.toBoolAlg.str
Construct a bundled FinBoolAlg
from BooleanAlgebra
+ Fintype
.
Equations
- FinBoolAlg.of α = FinBoolAlg.mk { α := α, str := inferInstance }
Instances For
@[simp]
theorem
FinBoolAlg.coe_of
(α : Type u_1)
[BooleanAlgebra α]
[Fintype α]
:
↑(FinBoolAlg.of α).toBoolAlg = α
Equations
- FinBoolAlg.instInhabited = { default := FinBoolAlg.of PUnit.{?u.3 + 1} }
Equations
- FinBoolAlg.instFunLike = BoundedLatticeHom.instFunLike
instance
FinBoolAlg.instBoundedLatticeHomClass
{X : FinBoolAlg}
{Y : FinBoolAlg}
:
BoundedLatticeHomClass (X ⟶ Y) ↑X.toBoolAlg ↑Y.toBoolAlg
Equations
- ⋯ = ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
Equations
@[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.
instance
FinBoolAlg.forgetToFinPartOrdFaithful :
(CategoryTheory.forget₂ FinBoolAlg FinPartOrd).Faithful
Equations
@[simp]
theorem
FinBoolAlg.Iso.mk_hom_toLatticeHom_toSupHom_toFun
{α : FinBoolAlg}
{β : FinBoolAlg}
(e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg)
(a : ↑α.toBoolAlg)
:
(FinBoolAlg.Iso.mk e).hom.toSupHom a = e a
@[simp]
theorem
FinBoolAlg.Iso.mk_inv_toLatticeHom_toSupHom_toFun
{α : FinBoolAlg}
{β : FinBoolAlg}
(e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg)
(a : ↑β.toBoolAlg)
:
(FinBoolAlg.Iso.mk e).inv.toSupHom a = e.symm a
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]
theorem
FinBoolAlg.dual_map :
∀ {x x_1 : FinBoolAlg}
(a : BoundedLatticeHom ↑x.toBoolAlg.toBddDistLat.toBddLat.toLat ↑x_1.toBoolAlg.toBddDistLat.toBddLat.toLat),
FinBoolAlg.dual.map a = BoundedLatticeHom.dual a
@[simp]
theorem
FinBoolAlg.dual_obj
(X : FinBoolAlg)
:
FinBoolAlg.dual.obj X = FinBoolAlg.of (↑X.toBoolAlg)ᵒᵈ
OrderDual
as a functor.
Equations
- One or more equations did not get rendered due to their size.
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_obj
(X : FintypeCat)
:
fintypeToFinBoolAlgOp.obj X = Opposite.op (FinBoolAlg.of (Set ↑X))
@[simp]
theorem
fintypeToFinBoolAlgOp_map
{X : FintypeCat}
{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' := ⋯ })
The powerset functor. Set
as a functor.
Equations
- One or more equations did not get rendered due to their size.