Documentation

Mathlib.Order.Category.FinBoolAlg

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.

source
structure FinBoolAlgextends BoolAlg :
Type (u_1 + 1)

The category of finite boolean algebras with bounded lattice morphisms.

Instances For
    source
    instance FinBoolAlg.instCoeSortType :
    CoeSort FinBoolAlg (Type u_1)
    Equations
      source
      @[reducible, inline]
      abbrev FinBoolAlg.of (α : Type u_1) [BooleanAlgebra α] [Fintype α] :
      FinBoolAlg

      Construct a bundled FinBoolAlg from BooleanAlgebra + Fintype.

      Equations
        Instances For
          source
          theorem FinBoolAlg.coe_of (α : Type u_1) [BooleanAlgebra α] [Fintype α] :
          ↑(of α).toBoolAlg = α
          source
          instance FinBoolAlg.instInhabited :
          Inhabited FinBoolAlg
          Equations
            source
            instance FinBoolAlg.largeCategory :
            CategoryTheory.LargeCategory FinBoolAlg
            Equations
              source
              instance FinBoolAlg.concreteCategory :
              CategoryTheory.ConcreteCategory FinBoolAlg fun (x1 x2 : FinBoolAlg) => BoundedLatticeHom ↑x1.toBoolAlg ↑x2.toBoolAlg
              Equations
                source
                instance FinBoolAlg.hasForgetToBoolAlg :
                CategoryTheory.HasForget₂ FinBoolAlg BoolAlg
                Equations
                  source
                  instance FinBoolAlg.hasForgetToFinBddDistLat :
                  CategoryTheory.HasForget₂ FinBoolAlg FinBddDistLat
                  Equations
                    source
                    instance FinBoolAlg.forgetToBoolAlg_full :
                    (CategoryTheory.forget₂ FinBoolAlg BoolAlg).Full
                    source
                    instance FinBoolAlg.forgetToBoolAlgFaithful :
                    (CategoryTheory.forget₂ FinBoolAlg BoolAlg).Faithful
                    source
                    instance FinBoolAlg.hasForgetToFinPartOrd :
                    CategoryTheory.HasForget₂ FinBoolAlg FinPartOrd
                    Equations
                      source
                      @[simp]
                      theorem FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_str (X : FinBoolAlg) :
                      (CategoryTheory.HasForget₂.forget₂.obj X).str = BiheytingAlgebra.toCoheytingAlgebra.toSemilatticeInf.toPartialOrder
                      source
                      @[simp]
                      theorem FinBoolAlg.hasForgetToFinPartOrd_forget₂_map {X Y : FinBoolAlg} (f : X ⟶ Y) :
                      CategoryTheory.HasForget₂.forget₂.map f = PartOrd.ofHom ↑(BoolAlg.Hom.hom f)
                      source
                      @[simp]
                      theorem FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_carrier (X : FinBoolAlg) :
                      ↑(CategoryTheory.HasForget₂.forget₂.obj X).toPartOrd = ↑X.toBoolAlg
                      source
                      @[simp]
                      theorem FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_isFintype (X : FinBoolAlg) :
                      (CategoryTheory.HasForget₂.forget₂.obj X).isFintype = X.isFintype
                      source
                      instance FinBoolAlg.forgetToFinPartOrdFaithful :
                      (CategoryTheory.forget₂ FinBoolAlg FinPartOrd).Faithful
                      source
                      def FinBoolAlg.Iso.mk {α β : FinBoolAlg} (e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg) :
                      α ≅ β

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

                      Equations
                        Instances For
                          source
                          @[simp]
                          theorem FinBoolAlg.Iso.mk_inv {α β : FinBoolAlg} (e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg) :
                          (mk e).inv = BoolAlg.ofHom (have __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
                          source
                          @[simp]
                          theorem FinBoolAlg.Iso.mk_hom {α β : FinBoolAlg} (e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg) :
                          (mk e).hom = BoolAlg.ofHom (have __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
                          source
                          def FinBoolAlg.dual :
                          CategoryTheory.Functor FinBoolAlg FinBoolAlg

                          OrderDual as a functor.

                          Equations
                            Instances For
                              source
                              @[simp]
                              theorem FinBoolAlg.dual_map {X✝ Y✝ : FinBoolAlg} (f : X✝ ⟶ Y✝) :
                              dual.map f = BoolAlg.ofHom (BoundedLatticeHom.dual (BoolAlg.Hom.hom f))
                              source
                              def FinBoolAlg.dualEquiv :
                              FinBoolAlg ≌ FinBoolAlg

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

                              Equations
                                Instances For
                                  source
                                  @[simp]
                                  theorem FinBoolAlg.dualEquiv_inverse :
                                  dualEquiv.inverse = dual
                                  source
                                  @[simp]
                                  theorem FinBoolAlg.dualEquiv_functor :
                                  dualEquiv.functor = dual
                                  source
                                  theorem finBoolAlg_dual_comp_forget_to_finBddDistLat :
                                  FinBoolAlg.dual.comp (CategoryTheory.forget₂ FinBoolAlg FinBddDistLat) = (CategoryTheory.forget₂ FinBoolAlg FinBddDistLat).comp FinBddDistLat.dual
                                  source
                                  def fintypeToFinBoolAlgOp :
                                  CategoryTheory.Functor FintypeCat FinBoolAlgᵒᵖ

                                  The powerset functor. Set as a functor.

                                  Equations
                                    Instances For
                                      source
                                      @[simp]
                                      theorem fintypeToFinBoolAlgOp_obj (X : FintypeCat) :
                                      fintypeToFinBoolAlgOp.obj X = Opposite.op (FinBoolAlg.of (Set X.carrier))
                                      source
                                      @[simp]
                                      theorem fintypeToFinBoolAlgOp_map {X Y : FintypeCat} (f : X ⟶ Y) :
                                      fintypeToFinBoolAlgOp.map f = (BoolAlg.ofHom (have __src := { toFun := ⇑(CompleteLatticeHom.setPreimage f), map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑(CompleteLatticeHom.setPreimage f), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })).op