mathlib3 documentation

order.category.FinBoolAlg

The category of finite boolean algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines FinBoolAlg, the category of finite boolean algebras.

TODO #

Birkhoff's representation for finite Boolean algebras.

Fintype_to_FinBoolAlg_op.left_op ⋙ FinBoolAlg.dual ≅ Fintype_to_FinBoolAlg_op.left_op

FinBoolAlg is essentially small.

structure FinBoolAlg :

Type (u_1+1)

to_BoolAlg : BoolAlg
is_fintype : fintype ↥(self.to_BoolAlg)

The category of finite boolean algebras with bounded lattice morphisms.

Instances for FinBoolAlg

@[protected, instance]

def FinBoolAlg.has_coe_to_sort :

has_coe_to_sort FinBoolAlg (Type u_1)

Equations

FinBoolAlg.has_coe_to_sort = {coe := λ (X : FinBoolAlg), ↥(X.to_BoolAlg)}

@[protected, instance]

def FinBoolAlg.boolean_algebra (X : FinBoolAlg) :

boolean_algebra ↥X

Equations

X.boolean_algebra = X.to_BoolAlg.str

@[simp]

theorem FinBoolAlg.coe_to_BoolAlg (X : FinBoolAlg) :

↥(X.to_BoolAlg) = ↥X

def FinBoolAlg.of (α : Type u_1) [boolean_algebra α] [fintype α] :

Construct a bundled FinBoolAlg from boolean_algebra + fintype.

Equations

FinBoolAlg.of α = FinBoolAlg.mk {α := α, str := _inst_1}

@[simp]

theorem FinBoolAlg.coe_of (α : Type u_1) [boolean_algebra α] [fintype α] :

↥(FinBoolAlg.of α) = α

@[protected, instance]

def FinBoolAlg.inhabited :

inhabited FinBoolAlg

Equations

FinBoolAlg.inhabited = {default := FinBoolAlg.of punit punit.fintype}

@[protected, instance]

def FinBoolAlg.large_category :

category_theory.large_category FinBoolAlg

Equations

FinBoolAlg.large_category = category_theory.induced_category.category FinBoolAlg.to_BoolAlg

@[protected, instance]

def FinBoolAlg.concrete_category :

category_theory.concrete_category FinBoolAlg

Equations

FinBoolAlg.concrete_category = category_theory.induced_category.concrete_category FinBoolAlg.to_BoolAlg

@[protected, instance]

def FinBoolAlg.has_forget_to_BoolAlg :

category_theory.has_forget₂ FinBoolAlg BoolAlg

Equations

FinBoolAlg.has_forget_to_BoolAlg = category_theory.induced_category.has_forget₂ FinBoolAlg.to_BoolAlg

@[protected, instance]

def FinBoolAlg.has_forget_to_FinBddDistLat :

category_theory.has_forget₂ FinBoolAlg FinBddDistLat

Equations

FinBoolAlg.has_forget_to_FinBddDistLat = {forget₂ := {obj := λ (X : FinBoolAlg), FinBddDistLat.of ↥X, map := λ (X Y : FinBoolAlg) (f : X ⟶ Y), f, map_id' := FinBoolAlg.has_forget_to_FinBddDistLat._proof_1, map_comp' := FinBoolAlg.has_forget_to_FinBddDistLat._proof_2}, forget_comp := FinBoolAlg.has_forget_to_FinBddDistLat._proof_3}

@[protected, instance]

def FinBoolAlg.forget_to_BoolAlg_full :

category_theory.full (category_theory.forget₂ FinBoolAlg BoolAlg)

Equations

FinBoolAlg.forget_to_BoolAlg_full = category_theory.induced_category.full FinBoolAlg.to_BoolAlg

@[protected, instance]

def FinBoolAlg.forget_to_BoolAlg_faithful :

category_theory.faithful (category_theory.forget₂ FinBoolAlg BoolAlg)

@[simp]

theorem FinBoolAlg.has_forget_to_FinPartOrd_forget₂_obj (X : FinBoolAlg) :

category_theory.has_forget₂.forget₂.obj X = FinPartOrd.of ↥X

@[simp]

theorem FinBoolAlg.has_forget_to_FinPartOrd_forget₂_map (X Y : FinBoolAlg) (f : X ⟶ Y) :

category_theory.has_forget₂.forget₂.map f = show ↥X →o ↥Y, from ↑(show bounded_lattice_hom ↥X ↥Y, from f)

@[protected, instance]

def FinBoolAlg.has_forget_to_FinPartOrd :

category_theory.has_forget₂ FinBoolAlg FinPartOrd

Equations

FinBoolAlg.has_forget_to_FinPartOrd = {forget₂ := {obj := λ (X : FinBoolAlg), FinPartOrd.of ↥X, map := λ (X Y : FinBoolAlg) (f : X ⟶ Y), show ↥X →o ↥Y, from ↑(show bounded_lattice_hom ↥X ↥Y, from f), map_id' := FinBoolAlg.has_forget_to_FinPartOrd._proof_1, map_comp' := FinBoolAlg.has_forget_to_FinPartOrd._proof_2}, forget_comp := FinBoolAlg.has_forget_to_FinPartOrd._proof_3}

@[protected, instance]

def FinBoolAlg.forget_to_FinPartOrd_faithful :

category_theory.faithful (category_theory.forget₂ FinBoolAlg FinPartOrd)

@[simp]

theorem FinBoolAlg.iso.mk_hom {α β : FinBoolAlg} (e : ↥α ≃o ↥β) :

(FinBoolAlg.iso.mk e).hom = ↑e

@[simp]

theorem FinBoolAlg.iso.mk_inv {α β : FinBoolAlg} (e : ↥α ≃o ↥β) :

(FinBoolAlg.iso.mk e).inv = ↑(e.symm)

def FinBoolAlg.iso.mk {α β : FinBoolAlg} (e : ↥α ≃o ↥β) :

α ≅ β

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

Equations

FinBoolAlg.iso.mk e = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}

def FinBoolAlg.dual :

FinBoolAlg ⥤ FinBoolAlg

order_dual as a functor.

Equations

FinBoolAlg.dual = {obj := λ (X : FinBoolAlg), FinBoolAlg.of (↥X)ᵒᵈ, map := λ (X Y : FinBoolAlg), ⇑bounded_lattice_hom.dual, map_id' := FinBoolAlg.dual._proof_1, map_comp' := FinBoolAlg.dual._proof_2}

@[simp]

theorem FinBoolAlg.dual_obj (X : FinBoolAlg) :

FinBoolAlg.dual.obj X = FinBoolAlg.of (↥X)ᵒᵈ

@[simp]

theorem FinBoolAlg.dual_map (X Y : FinBoolAlg) (ᾰ : bounded_lattice_hom ↥(X.to_BoolAlg.to_BddDistLat.to_BddLat) ↥(Y.to_BoolAlg.to_BddDistLat.to_BddLat)) :

FinBoolAlg.dual.map ᾰ = ⇑bounded_lattice_hom.dual ᾰ

@[simp]

theorem FinBoolAlg.dual_equiv_functor :

FinBoolAlg.dual_equiv.functor = FinBoolAlg.dual

def FinBoolAlg.dual_equiv :

FinBoolAlg ≌ FinBoolAlg

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

Equations

FinBoolAlg.dual_equiv = category_theory.equivalence.mk FinBoolAlg.dual FinBoolAlg.dual (category_theory.nat_iso.of_components (λ (X : FinBoolAlg), FinBoolAlg.iso.mk (order_iso.dual_dual ↥X)) FinBoolAlg.dual_equiv._proof_1) (category_theory.nat_iso.of_components (λ (X : FinBoolAlg), FinBoolAlg.iso.mk (order_iso.dual_dual ↥X)) FinBoolAlg.dual_equiv._proof_2)

@[simp]

theorem FinBoolAlg.dual_equiv_inverse :

FinBoolAlg.dual_equiv.inverse = FinBoolAlg.dual

theorem FinBoolAlg_dual_comp_forget_to_FinBddDistLat :

FinBoolAlg.dual ⋙ category_theory.forget₂ FinBoolAlg FinBddDistLat = category_theory.forget₂ FinBoolAlg FinBddDistLat ⋙ FinBddDistLat.dual

@[simp]

theorem Fintype_to_FinBoolAlg_op_obj (X : Fintype) :

Fintype_to_FinBoolAlg_op.obj X = opposite.op (FinBoolAlg.of (set ↥X))

@[simp]

theorem Fintype_to_FinBoolAlg_op_map (X Y : Fintype) (f : X ⟶ Y) :

Fintype_to_FinBoolAlg_op.map f = quiver.hom.op ↑(complete_lattice_hom.set_preimage f)

def Fintype_to_FinBoolAlg_op :

Fintype ⥤ FinBoolAlg ᵒᵖ

The powerset functor. set as a functor.

Equations

Fintype_to_FinBoolAlg_op = {obj := λ (X : Fintype), opposite.op (FinBoolAlg.of (set ↥X)), map := λ (X Y : Fintype) (f : X ⟶ Y), quiver.hom.op ↑(complete_lattice_hom.set_preimage f), map_id' := Fintype_to_FinBoolAlg_op._proof_1, map_comp' := Fintype_to_FinBoolAlg_op._proof_2}