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.3 + 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₂_obj_str
(X : BoolAlg)
:
(CategoryTheory.HasForget₂.forget₂.obj X).str = inferInstance
@[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
Equations
- One or more equations did not get rendered due to their size.
@[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.Iso.mk_inv_toLatticeHom_toSupHom_toFun
{α : BoolAlg}
{β : BoolAlg}
(e : ↑α ≃o ↑β)
(a : ↑β)
:
(BoolAlg.Iso.mk e).inv.toSupHom a = e.symm 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 }
Instances For
@[simp]
@[simp]
theorem
typeToBoolAlgOp_map
{X : Type u}
{Y : Type u}
(f : X ⟶ Y)
:
typeToBoolAlgOp.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 contravariant functor.
Equations
- One or more equations did not get rendered due to their size.