The category of boolean algebras.
Equations
@[protected, instance]
@[protected, instance]
Equations
- X.boolean_algebra = X.str
Construct a bundled BoolAlg
from a boolean_algebra
.
Equations
@[protected, instance]
Equations
Turn a BoolAlg
into a BoundedDistribLattice
by forgetting its complement operation.
Equations
@[simp]
Constructs an equivalence between boolean algebras from an order isomorphism between them.
Equations
- BoolAlg.iso.mk e = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
@[simp]
theorem
BoolAlg.dual_map
(X Y : BoolAlg)
(ᾰ : bounded_lattice_hom ↥(X.to_BoundedDistribLattice.to_BoundedLattice) ↥(Y.to_BoundedDistribLattice.to_BoundedLattice)) :
order_dual
as a functor.
Equations
- BoolAlg.dual = {obj := λ (X : BoolAlg), BoolAlg.of (↥X)ᵒᵈ, map := λ (X Y : BoolAlg), ⇑bounded_lattice_hom.dual, map_id' := BoolAlg.dual._proof_1, map_comp' := BoolAlg.dual._proof_2}
The equivalence between BoolAlg
and itself induced by order_dual
both ways.
Equations
- BoolAlg.dual_equiv = category_theory.equivalence.mk BoolAlg.dual BoolAlg.dual (category_theory.nat_iso.of_components (λ (X : BoolAlg), BoolAlg.iso.mk (order_iso.dual_dual ↥X)) BoolAlg.dual_equiv._proof_1) (category_theory.nat_iso.of_components (λ (X : BoolAlg), BoolAlg.iso.mk (order_iso.dual_dual ↥X)) BoolAlg.dual_equiv._proof_2)