The category of boolean algebras

This defines BoolAlg, the category of boolean algebras.

def BoolAlg : Type (u_1 + 1)

The category of boolean algebras.

Equations

• BoolAlg = CategoryTheory.Bundled BooleanAlgebra

instance BoolAlg.instCoeSortType : CoeSort BoolAlg (Type u_1)

Equations

• BoolAlg.instCoeSortType = CategoryTheory.Bundled.coeSort

instance BoolAlg.instBooleanAlgebra (X : BoolAlg) : BooleanAlgebra ↑X

Equations

• X.instBooleanAlgebra = X.str

def BoolAlg.of (α : Type u_1) [BooleanAlgebra α] : BoolAlg

Construct a bundled BoolAlg from a BooleanAlgebra.

Equations

• BoolAlg.of α = CategoryTheory.Bundled.of α

@[simp]

theorem BoolAlg.coe_of (α : Type u_1) [BooleanAlgebra α] : ↑(BoolAlg.of α) = α

instance BoolAlg.instInhabited : Inhabited BoolAlg

Equations

• BoolAlg.instInhabited = { default := BoolAlg.of PUnit.{?u.3 + 1} }

def BoolAlg.toBddDistLat (X : BoolAlg) : BddDistLat

Turn a BoolAlg into a BddDistLat by forgetting its complement operation.

Equations

• X.toBddDistLat = BddDistLat.of ↑X

@[simp]

theorem BoolAlg.coe_toBddDistLat (X : BoolAlg) : ↑X.toBddDistLat.toDistLat = ↑X

instance BoolAlg.instLargeCategory : CategoryTheory.LargeCategory BoolAlg

Equations

• BoolAlg.instLargeCategory = CategoryTheory.InducedCategory.category BoolAlg.toBddDistLat

instance BoolAlg.instConcreteCategory : CategoryTheory.ConcreteCategory BoolAlg

Equations

• BoolAlg.instConcreteCategory = CategoryTheory.InducedCategory.concreteCategory BoolAlg.toBddDistLat

instance BoolAlg.hasForgetToBddDistLat : CategoryTheory.HasForget₂ BoolAlg BddDistLat

Equations

• BoolAlg.hasForgetToBddDistLat = CategoryTheory.InducedCategory.hasForget₂ BoolAlg.toBddDistLat

instance BoolAlg.hasForgetToHeytAlg : CategoryTheory.HasForget₂ BoolAlg HeytAlg

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BoolAlg.hasForgetToHeytAlg_forget₂_map_toFun {X Y : BoolAlg} (f : BoundedLatticeHom ↑X ↑Y) (a : ↑X) : (CategoryTheory.HasForget₂.forget₂.map f) a = f a

@[simp]

theorem BoolAlg.hasForgetToHeytAlg_forget₂_obj_str (X : BoolAlg) : (CategoryTheory.HasForget₂.forget₂.obj X).str = inferInstance

@[simp]

theorem BoolAlg.hasForgetToHeytAlg_forget₂_obj_α (X : BoolAlg) : ↑(CategoryTheory.HasForget₂.forget₂.obj X) = ↑X

def BoolAlg.Iso.mk {α β : BoolAlg} (e : ↑α ≃o ↑β) : α ≅ β

Constructs an equivalence between Boolean algebras from an order isomorphism between them.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BoolAlg.Iso.mk_hom_toLatticeHom_toSupHom_toFun {α β : BoolAlg} (e : ↑α ≃o ↑β) (a : ↑α) : (BoolAlg.Iso.mk e).hom.toSupHom a = e a

@[simp]

theorem BoolAlg.Iso.mk_inv_toLatticeHom_toSupHom_toFun {α β : BoolAlg} (e : ↑α ≃o ↑β) (a : ↑β) : (BoolAlg.Iso.mk e).inv.toSupHom a = e.symm a

def BoolAlg.dual : CategoryTheory.Functor BoolAlg BoolAlg

OrderDual as a functor.

Equations

• BoolAlg.dual = { obj := fun (X : BoolAlg) => BoolAlg.of (↑X)ᵒᵈ, map := fun {x x_1 : BoolAlg} => ⇑BoundedLatticeHom.dual, map_id := BoolAlg.dual.proof_1, map_comp := @BoolAlg.dual.proof_2 }

@[simp]

theorem BoolAlg.dual_map {x✝ x✝¹ : BoolAlg} (a : BoundedLatticeHom ↑x✝.toBddDistLat.toBddLat.toLat ↑x✝¹.toBddDistLat.toBddLat.toLat) : BoolAlg.dual.map a = BoundedLatticeHom.dual a

@[simp]

theorem BoolAlg.dual_obj (X : BoolAlg) : BoolAlg.dual.obj X = BoolAlg.of (↑X)ᵒᵈ

def BoolAlg.dualEquiv : BoolAlg ≌ BoolAlg

The equivalence between BoolAlg and itself induced by OrderDual both ways.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BoolAlg.dualEquiv_inverse : BoolAlg.dualEquiv.inverse = BoolAlg.dual

@[simp]

theorem BoolAlg.dualEquiv_functor : BoolAlg.dualEquiv.functor = BoolAlg.dual

theorem boolAlg_dual_comp_forget_to_bddDistLat : BoolAlg.dual.comp (CategoryTheory.forget₂ BoolAlg BddDistLat) = (CategoryTheory.forget₂ BoolAlg BddDistLat).comp BddDistLat.dual

def typeToBoolAlgOp : CategoryTheory.Functor (Type u) BoolAlgᵒᵖ

The powerset functor. Set as a contravariant functor.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem typeToBoolAlgOp_map {X 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' := ⋯ })

@[simp]

theorem typeToBoolAlgOp_obj (X : Type u) : typeToBoolAlgOp.obj X = Opposite.op (BoolAlg.of (Set X))