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.

structure FinBoolAlgextends BoolAlg : Type (u_1 + 1)

The category of finite Boolean algebras with bounded lattice morphisms.

• carrier : Type u_1
• str : BooleanAlgebra ↑self.toBoolAlg
• isFintype : Fintype ↑self.toBoolAlg

@[implicit_reducible]

instance FinBoolAlg.instCoeSortType : CoeSort FinBoolAlg (Type u_1)

Equations

• FinBoolAlg.instCoeSortType = { coe := fun (X : FinBoolAlg) => ↑X.toBoolAlg }

@[reducible, inline]

abbrev FinBoolAlg.of (α : Type u_1) [BooleanAlgebra α] [Fintype α] : FinBoolAlg

Construct a bundled FinBoolAlg from BooleanAlgebra + Fintype.

Equations

• FinBoolAlg.of α = { carrier := α, str := inst✝¹, isFintype := inst✝ }

theorem FinBoolAlg.coe_of (α : Type u_1) [BooleanAlgebra α] [Fintype α] : ↑(of α).toBoolAlg = α

@[implicit_reducible]

instance FinBoolAlg.instInhabited : Inhabited FinBoolAlg

Equations

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

@[implicit_reducible]

instance FinBoolAlg.largeCategory : CategoryTheory.LargeCategory FinBoolAlg

Equations

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

@[implicit_reducible]

instance FinBoolAlg.concreteCategory : CategoryTheory.ConcreteCategory FinBoolAlg fun (x1 x2 : FinBoolAlg) => BoundedLatticeHom ↑x1.toBoolAlg ↑x2.toBoolAlg

Equations

• FinBoolAlg.concreteCategory = CategoryTheory.InducedCategory.concreteCategory FinBoolAlg.toBoolAlg

@[implicit_reducible]

instance FinBoolAlg.hasForgetToBoolAlg : CategoryTheory.HasForget₂ FinBoolAlg BoolAlg

Equations

• FinBoolAlg.hasForgetToBoolAlg = CategoryTheory.InducedCategory.hasForget₂ FinBoolAlg.toBoolAlg

@[implicit_reducible]

instance FinBoolAlg.hasForgetToFinBddDistLat : CategoryTheory.HasForget₂ FinBoolAlg FinBddDistLat

Equations

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

instance FinBoolAlg.forgetToBoolAlg_full : (CategoryTheory.forget₂ FinBoolAlg BoolAlg).Full

instance FinBoolAlg.forgetToBoolAlgFaithful : (CategoryTheory.forget₂ FinBoolAlg BoolAlg).Faithful

@[implicit_reducible]

instance FinBoolAlg.hasForgetToFinPartOrd : CategoryTheory.HasForget₂ FinBoolAlg FinPartOrd

Equations

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

@[simp]

theorem FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_str (X : FinBoolAlg) : (CategoryTheory.HasForget₂.forget₂.obj X).str = BiheytingAlgebra.toCoheytingAlgebra.toSemilatticeInf.toPartialOrder

@[simp]

theorem FinBoolAlg.hasForgetToFinPartOrd_forget₂_map {X Y : FinBoolAlg} (f : X ⟶ Y) : CategoryTheory.HasForget₂.forget₂.map f = CategoryTheory.InducedCategory.homMk (PartOrd.ofHom ↑(BoolAlg.Hom.hom f.hom))

@[simp]

theorem FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_carrier (X : FinBoolAlg) : ↑(CategoryTheory.HasForget₂.forget₂.obj X).toPartOrd = ↑X.toBoolAlg

@[simp]

theorem FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_isFintype (X : FinBoolAlg) : (CategoryTheory.HasForget₂.forget₂.obj X).isFintype = X.isFintype

instance FinBoolAlg.forgetToFinPartOrdFaithful : (CategoryTheory.forget₂ FinBoolAlg FinPartOrd).Faithful

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

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.

@[simp]

theorem FinBoolAlg.Iso.mk_inv {α β : FinBoolAlg} (e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg) : (mk e).inv = CategoryTheory.InducedCategory.homMk (BoolAlg.ofHom (have __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }))

@[simp]

theorem FinBoolAlg.Iso.mk_hom {α β : FinBoolAlg} (e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg) : (mk e).hom = CategoryTheory.InducedCategory.homMk (BoolAlg.ofHom (have __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }))

def FinBoolAlg.dual : CategoryTheory.Functor FinBoolAlg FinBoolAlg

OrderDual as a functor.

Equations

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

@[simp]

theorem FinBoolAlg.dual_map {X✝ Y✝ : FinBoolAlg} (f : X✝ ⟶ Y✝) : dual.map f = CategoryTheory.InducedCategory.homMk (BoolAlg.ofHom (BoundedLatticeHom.dual (BoolAlg.Hom.hom f.hom)))

def FinBoolAlg.dualEquiv : FinBoolAlg ≌ FinBoolAlg

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

Equations

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

@[simp]

theorem FinBoolAlg.dualEquiv_inverse : dualEquiv.inverse = dual

@[simp]

theorem FinBoolAlg.dualEquiv_functor : dualEquiv.functor = dual

theorem finBoolAlg_dual_comp_forget_to_finBddDistLat : FinBoolAlg.dual.comp (CategoryTheory.forget₂ FinBoolAlg FinBddDistLat) = (CategoryTheory.forget₂ FinBoolAlg FinBddDistLat).comp FinBddDistLat.dual

noncomputable def fintypeToFinBoolAlgOp : CategoryTheory.Functor FintypeCat FinBoolAlgᵒᵖ

The powerset functor. Set as a functor.

Equations

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

@[simp]

theorem fintypeToFinBoolAlgOp_obj (X : FintypeCat) : fintypeToFinBoolAlgOp.obj X = Opposite.op (FinBoolAlg.of (Set X.obj))

@[simp]

theorem fintypeToFinBoolAlgOp_map {X Y : FintypeCat} (f : X ⟶ Y) : fintypeToFinBoolAlgOp.map f = (CategoryTheory.InducedCategory.homMk (BoolAlg.ofHom (have __src := { toFun := ⇑(CompleteLatticeHom.setPreimage ⇑(CategoryTheory.ConcreteCategory.hom f)), map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑(CompleteLatticeHom.setPreimage ⇑(CategoryTheory.ConcreteCategory.hom f)), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }))).op