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
    @[implicit_reducible]
    instance FinBoolAlg.instCoeSortType :
    CoeSort FinBoolAlg (Type u_1)
    source
    @[reducible, inline]
    abbrev FinBoolAlg.of (α : Type u_1) [BooleanAlgebra α] [Fintype α] :
    FinBoolAlg

    Construct a bundled FinBoolAlg from BooleanAlgebra + Fintype.

    Instances For
      source
      theorem FinBoolAlg.coe_of (α : Type u_1) [BooleanAlgebra α] [Fintype α] :
      ↑(of α).toBoolAlg = α
      source
      @[implicit_reducible]
      instance FinBoolAlg.instInhabited :
      Inhabited FinBoolAlg
      source
      @[implicit_reducible]
      instance FinBoolAlg.largeCategory :
      CategoryTheory.LargeCategory FinBoolAlg
      source
      @[implicit_reducible]
      instance FinBoolAlg.concreteCategory :
      CategoryTheory.ConcreteCategory FinBoolAlg fun (x1 x2 : FinBoolAlg) => BoundedLatticeHom ↑x1.toBoolAlg ↑x2.toBoolAlg
      source
      @[implicit_reducible]
      instance FinBoolAlg.hasForgetToBoolAlg :
      CategoryTheory.HasForget₂ FinBoolAlg BoolAlg
      source
      @[implicit_reducible]
      instance FinBoolAlg.hasForgetToFinBddDistLat :
      CategoryTheory.HasForget₂ FinBoolAlg FinBddDistLat
      source
      instance FinBoolAlg.forgetToBoolAlg_full :
      (CategoryTheory.forget₂ FinBoolAlg BoolAlg).Full
      source
      instance FinBoolAlg.forgetToBoolAlgFaithful :
      (CategoryTheory.forget₂ FinBoolAlg BoolAlg).Faithful
      source
      @[implicit_reducible]
      instance FinBoolAlg.hasForgetToFinPartOrd :
      CategoryTheory.HasForget₂ FinBoolAlg FinPartOrd
      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 = CategoryTheory.InducedCategory.homMk (PartOrd.ofHom ↑(BoolAlg.Hom.hom f.hom))
      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.

      Instances For
        source
        @[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' := ⋯ }))
        source
        @[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' := ⋯ }))
        source
        def FinBoolAlg.dual :
        CategoryTheory.Functor FinBoolAlg FinBoolAlg

        OrderDual as a functor.

        Instances For
          source
          @[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)))
          source
          def FinBoolAlg.dualEquiv :
          FinBoolAlg ≌ FinBoolAlg

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

          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
            noncomputable def fintypeToFinBoolAlgOp :
            CategoryTheory.Functor FintypeCat FinBoolAlgᵒᵖ

            The powerset functor. Set as a functor.

            Instances For
              source
              @[simp]
              theorem fintypeToFinBoolAlgOp_obj (X : FintypeCat) :
              fintypeToFinBoolAlgOp.obj X = Opposite.op (FinBoolAlg.of (Set X.obj))
              source
              @[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