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.instCoeSortFinBoolAlgType : CoeSort FinBoolAlg (Type u_1)

Equations

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

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

Equations

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

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

Construct a bundled FinBoolAlg from BooleanAlgebra + Fintype.

Equations

• FinBoolAlg.of α = FinBoolAlg.mk (CategoryTheory.Bundled.mk α)

@[simp]

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

instance FinBoolAlg.instInhabitedFinBoolAlg : Inhabited FinBoolAlg

Equations

• FinBoolAlg.instInhabitedFinBoolAlg = { default := FinBoolAlg.of PUnit.{u_1 + 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 : FinBoolAlg} {Y : FinBoolAlg} : FunLike (X ⟶ Y) ↑X.toBoolAlg ↑Y.toBoolAlg

Equations

• FinBoolAlg.instFunLike = BoundedLatticeHom.instFunLike

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

Equations

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

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.forgetToBoolAlgFull : CategoryTheory.Full (CategoryTheory.forget₂ FinBoolAlg BoolAlg)

Equations

• FinBoolAlg.forgetToBoolAlgFull = CategoryTheory.InducedCategory.full FinBoolAlg.toBoolAlg

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

Equations

• FinBoolAlg.forgetToBoolAlgFaithful = (_ : CategoryTheory.Faithful (CategoryTheory.inducedFunctor FinBoolAlg.toBoolAlg))

@[simp]

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

@[simp]

theorem FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj (X : FinBoolAlg) : CategoryTheory.HasForget₂.forget₂.toPrefunctor.obj X = FinPartOrd.of ↑X.toBoolAlg

instance FinBoolAlg.hasForgetToFinPartOrd : CategoryTheory.HasForget₂ FinBoolAlg FinPartOrd

Equations

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

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

Equations

• FinBoolAlg.forgetToFinPartOrdFaithful = (_ : CategoryTheory.Faithful (CategoryTheory.forget₂ FinBoolAlg FinPartOrd))

@[simp]

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

@[simp]

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

def FinBoolAlg.Iso.mk {α : FinBoolAlg} {β : 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.dual_obj (X : FinBoolAlg) : FinBoolAlg.dual.toPrefunctor.obj X = FinBoolAlg.of (↑X.toBoolAlg)ᵒᵈ

@[simp]

theorem FinBoolAlg.dual_map {X : FinBoolAlg} {Y : FinBoolAlg} (a : BoundedLatticeHom ↑(BddDistLat.toBddLat (BoolAlg.toBddDistLat X.toBoolAlg)).toLat ↑(BddDistLat.toBddLat (BoolAlg.toBddDistLat Y.toBoolAlg)).toLat) : FinBoolAlg.dual.toPrefunctor.map a = BoundedLatticeHom.dual a

def FinBoolAlg.dual : CategoryTheory.Functor FinBoolAlg FinBoolAlg

OrderDual as a functor.

Equations

• FinBoolAlg.dual = CategoryTheory.Functor.mk { obj := fun (X : FinBoolAlg) => FinBoolAlg.of (↑X.toBoolAlg)ᵒᵈ, map := fun {X Y : FinBoolAlg} => ⇑BoundedLatticeHom.dual }

@[simp]

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

@[simp]

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

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.

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

@[simp]

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

@[simp]

theorem fintypeToFinBoolAlgOp_map {X : FintypeCat} {Y : FintypeCat} (f : X ⟶ Y) : fintypeToFinBoolAlgOp.toPrefunctor.map f = (let src := { toSupHom := { toFun := ⇑(CompleteLatticeHom.setPreimage f), map_sup' := (_ : ∀ (a b : Set ↑Y), (CompleteLatticeHom.setPreimage f) (a ⊔ b) = (CompleteLatticeHom.setPreimage f) a ⊔ (CompleteLatticeHom.setPreimage f) b) }, map_inf' := (_ : ∀ (a b : Set ↑Y), (CompleteLatticeHom.setPreimage f) (a ⊓ b) = (CompleteLatticeHom.setPreimage f) a ⊓ (CompleteLatticeHom.setPreimage f) b) }; { toLatticeHom := { toSupHom := { toFun := ⇑(CompleteLatticeHom.setPreimage f), map_sup' := (_ : ∀ (a b : Set ↑Y), { toSupHom := { toFun := ⇑(CompleteLatticeHom.setPreimage f), map_sup' := (_ : ∀ (a b : Set ↑Y), (CompleteLatticeHom.setPreimage f) (a ⊔ b) = (CompleteLatticeHom.setPreimage f) a ⊔ (CompleteLatticeHom.setPreimage f) b) }, map_inf' := (_ : ∀ (a b : Set ↑Y), (CompleteLatticeHom.setPreimage f) (a ⊓ b) = (CompleteLatticeHom.setPreimage f) a ⊓ (CompleteLatticeHom.setPreimage f) b) }.toSupHom.toFun (a ⊔ b) = { toSupHom := { toFun := ⇑(CompleteLatticeHom.setPreimage f), map_sup' := (_ : ∀ (a b : Set ↑Y), (CompleteLatticeHom.setPreimage f) (a ⊔ b) = (CompleteLatticeHom.setPreimage f) a ⊔ (CompleteLatticeHom.setPreimage f) b) }, map_inf' := (_ : ∀ (a b : Set ↑Y), (CompleteLatticeHom.setPreimage f) (a ⊓ b) = (CompleteLatticeHom.setPreimage f) a ⊓ (CompleteLatticeHom.setPreimage f) b) }.toSupHom.toFun a ⊔ { toSupHom := { toFun := ⇑(CompleteLatticeHom.setPreimage f), map_sup' := (_ : ∀ (a b : Set ↑Y), (CompleteLatticeHom.setPreimage f) (a ⊔ b) = (CompleteLatticeHom.setPreimage f) a ⊔ (CompleteLatticeHom.setPreimage f) b) }, map_inf' := (_ : ∀ (a b : Set ↑Y), (CompleteLatticeHom.setPreimage f) (a ⊓ b) = (CompleteLatticeHom.setPreimage f) a ⊓ (CompleteLatticeHom.setPreimage f) b) }.toSupHom.toFun b) }, map_inf' := (_ : ∀ (a b : Set ↑Y), { toSupHom := { toFun := ⇑(CompleteLatticeHom.setPreimage f), map_sup' := (_ : ∀ (a b : Set ↑Y), (CompleteLatticeHom.setPreimage f) (a ⊔ b) = (CompleteLatticeHom.setPreimage f) a ⊔ (CompleteLatticeHom.setPreimage f) b) }, map_inf' := (_ : ∀ (a b : Set ↑Y), (CompleteLatticeHom.setPreimage f) (a ⊓ b) = (CompleteLatticeHom.setPreimage f) a ⊓ (CompleteLatticeHom.setPreimage f) b) }.toSupHom.toFun (a ⊓ b) = { toSupHom := { toFun := ⇑(CompleteLatticeHom.setPreimage f), map_sup' := (_ : ∀ (a b : Set ↑Y), (CompleteLatticeHom.setPreimage f) (a ⊔ b) = (CompleteLatticeHom.setPreimage f) a ⊔ (CompleteLatticeHom.setPreimage f) b) }, map_inf' := (_ : ∀ (a b : Set ↑Y), (CompleteLatticeHom.setPreimage f) (a ⊓ b) = (CompleteLatticeHom.setPreimage f) a ⊓ (CompleteLatticeHom.setPreimage f) b) }.toSupHom.toFun a ⊓ { toSupHom := { toFun := ⇑(CompleteLatticeHom.setPreimage f), map_sup' := (_ : ∀ (a b : Set ↑Y), (CompleteLatticeHom.setPreimage f) (a ⊔ b) = (CompleteLatticeHom.setPreimage f) a ⊔ (CompleteLatticeHom.setPreimage f) b) }, map_inf' := (_ : ∀ (a b : Set ↑Y), (CompleteLatticeHom.setPreimage f) (a ⊓ b) = (CompleteLatticeHom.setPreimage f) a ⊓ (CompleteLatticeHom.setPreimage f) b) }.toSupHom.toFun b) }, map_top' := (_ : (CompleteLatticeHom.setPreimage f) ⊤ = ⊤), map_bot' := (_ : (CompleteLatticeHom.setPreimage f) ⊥ = ⊥) }).op

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.