The category of boolean algebras.
Equations
Instances For
Equations
- BoolAlg.instCoeSortType = CategoryTheory.Bundled.coeSort
Equations
- X.instBooleanAlgebra = X.str
Equations
- BoolAlg.instInhabited = { default := BoolAlg.of PUnit.{u_1 + 1} }
Turn a BoolAlg
into a BddDistLat
by forgetting its complement operation.
Equations
- X.toBddDistLat = BddDistLat.of ↑X
Instances For
@[simp]
theorem
BoolAlg.hasForgetToHeytAlg_forget₂_map_toFun
{X : BoolAlg}
{Y : BoolAlg}
(f : BoundedLatticeHom ↑X ↑Y)
(a : ↑X)
:
(CategoryTheory.HasForget₂.forget₂.map f) a = f a
@[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
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 : ↑β)
:
(BoolAlg.Iso.mk e).inv.toSupHom a = e.symm a
@[simp]
theorem
BoolAlg.Iso.mk_hom_toLatticeHom_toSupHom_toFun
{α : BoolAlg}
{β : BoolAlg}
(e : ↑α ≃o ↑β)
(a : ↑α)
:
(BoolAlg.Iso.mk e).hom.toSupHom a = e a
@[simp]
theorem
BoolAlg.dual_map
{X : BoolAlg}
{Y : BoolAlg}
(a : BoundedLatticeHom ↑X.toBddDistLat.toBddLat.toLat ↑Y.toBddDistLat.toBddLat.toLat)
:
BoolAlg.dual.map a = BoundedLatticeHom.dual a
OrderDual
as a functor.
Equations
- BoolAlg.dual = { obj := fun (X : BoolAlg) => BoolAlg.of (↑X)ᵒᵈ, map := fun {X Y : BoolAlg} => ⇑BoundedLatticeHom.dual, map_id := BoolAlg.dual.proof_1, map_comp := @BoolAlg.dual.proof_2 }