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 FinBoolAlg : Type (u_1 + 1)

The category of finite boolean algebras with bounded lattice morphisms.

• toBoolAlg : BoolAlg
• isFintype : Fintype ↑self.toBoolAlg

instance FinBoolAlg.instCoeSortType : CoeSort FinBoolAlg (Type u_1)

Equations

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

instance FinBoolAlg.instBooleanAlgebraαToBoolAlg (X : FinBoolAlg) : BooleanAlgebra ↑X.toBoolAlg

Equations

• X.instBooleanAlgebraαToBoolAlg = X.toBoolAlg.str

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

Construct a bundled FinBoolAlg from BooleanAlgebra + Fintype.

Equations

• FinBoolAlg.of α = FinBoolAlg.mk { α := α, str := inferInstance }

@[simp]

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

instance FinBoolAlg.instInhabited : Inhabited FinBoolAlg

Equations

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

instance FinBoolAlg.largeCategory : CategoryTheory.LargeCategory FinBoolAlg

Equations

• FinBoolAlg.largeCategory = CategoryTheory.InducedCategory.category FinBoolAlg.toBoolAlg

instance FinBoolAlg.concreteCategory : CategoryTheory.ConcreteCategory FinBoolAlg

Equations

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

instance FinBoolAlg.instFunLike {X Y : FinBoolAlg} : FunLike (X ⟶ Y) ↑X.toBoolAlg ↑Y.toBoolAlg

Equations

• FinBoolAlg.instFunLike = BoundedLatticeHom.instFunLike

instance FinBoolAlg.instBoundedLatticeHomClass {X Y : FinBoolAlg} : BoundedLatticeHomClass (X ⟶ Y) ↑X.toBoolAlg ↑Y.toBoolAlg

instance FinBoolAlg.hasForgetToBoolAlg : CategoryTheory.HasForget₂ FinBoolAlg BoolAlg

Equations

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

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

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 (X : FinBoolAlg) : CategoryTheory.HasForget₂.forget₂.obj X = FinPartOrd.of ↑X.toBoolAlg

@[simp]

theorem FinBoolAlg.hasForgetToFinPartOrd_forget₂_map {X Y : FinBoolAlg} (f : X ⟶ Y) : CategoryTheory.HasForget₂.forget₂.map f = let_fun this := ↑(let_fun this := f; this); this

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_toLatticeHom_toSupHom_toFun {α β : FinBoolAlg} (e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg) (a : ↑β.toBoolAlg) : (FinBoolAlg.Iso.mk e).inv.toSupHom a = e.symm a

@[simp]

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

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_obj (X : FinBoolAlg) : FinBoolAlg.dual.obj X = FinBoolAlg.of (↑X.toBoolAlg)ᵒᵈ

@[simp]

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

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_functor : FinBoolAlg.dualEquiv.functor = FinBoolAlg.dual

@[simp]

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

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

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))

@[simp]

theorem fintypeToFinBoolAlgOp_map {X Y : FintypeCat} (f : X ⟶ Y) : fintypeToFinBoolAlgOp.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' := ⋯ })