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 FinBoolAlg :
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
    instance FinBoolAlg.instBooleanAlgebraαToBoolAlg (X : FinBoolAlg) :
    BooleanAlgebra ↑X.toBoolAlg
    Equations
    • X.instBooleanAlgebraαToBoolAlg = X.toBoolAlg.str
    source
    def FinBoolAlg.of (α : Type u_1) [BooleanAlgebra α] [Fintype α] :
    FinBoolAlg

    Construct a bundled FinBoolAlg from BooleanAlgebra + Fintype.

    Equations
    Instances For
      source
      @[simp]
      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.hasForget :
      CategoryTheory.HasForget FinBoolAlg
      Equations
      source
      instance FinBoolAlg.instFunLike {X Y : FinBoolAlg} :
      FunLike (X ⟶ Y) ↑X.toBoolAlg ↑Y.toBoolAlg
      Equations
      source
      instance FinBoolAlg.instBoundedLatticeHomClass {X Y : FinBoolAlg} :
      BoundedLatticeHomClass (X ⟶ Y) ↑X.toBoolAlg ↑Y.toBoolAlg
      source
      instance FinBoolAlg.hasForgetToBoolAlg :
      CategoryTheory.HasForget₂ FinBoolAlg BoolAlg
      Equations
      source
      instance FinBoolAlg.hasForgetToFinBddDistLat :
      CategoryTheory.HasForget₂ FinBoolAlg FinBddDistLat
      Equations
      • One or more equations did not get rendered due to their size.
      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
      • One or more equations did not get rendered due to their size.
      source
      @[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
      source
      @[simp]
      theorem FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj (X : FinBoolAlg) :
      CategoryTheory.HasForget₂.forget₂.obj X = FinPartOrd.of ↑X.toBoolAlg
      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
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem FinBoolAlg.Iso.mk_inv_toLatticeHom_toSupHom_toFun {α β : FinBoolAlg} (e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg) (a : ↑β.toBoolAlg) :
        (mk e).inv.toSupHom a = e.symm a
        source
        @[simp]
        theorem FinBoolAlg.Iso.mk_hom_toLatticeHom_toSupHom_toFun {α β : FinBoolAlg} (e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg) (a : ↑α.toBoolAlg) :
        (mk e).hom.toSupHom a = e a
        source
        def FinBoolAlg.dual :
        CategoryTheory.Functor FinBoolAlg FinBoolAlg

        OrderDual as a functor.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem FinBoolAlg.dual_obj (X : FinBoolAlg) :
          dual.obj X = of (↑X.toBoolAlg)ᵒᵈ
          source
          @[simp]
          theorem FinBoolAlg.dual_map {x✝ x✝¹ : FinBoolAlg} (a : BoundedLatticeHom ↑x✝.toBoolAlg.toBddDistLat.toBddLat.toLat ↑x✝¹.toBoolAlg.toBddDistLat.toBddLat.toLat) :
          dual.map a = BoundedLatticeHom.dual a
          source
          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.
          Instances For
            source
            @[simp]
            theorem FinBoolAlg.dualEquiv_functor :
            dualEquiv.functor = dual
            source
            @[simp]
            theorem FinBoolAlg.dualEquiv_inverse :
            dualEquiv.inverse = 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
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[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' := ⋯ })
              source
              @[simp]
              theorem fintypeToFinBoolAlgOp_obj (X : FintypeCat) :
              fintypeToFinBoolAlgOp.obj X = Opposite.op (FinBoolAlg.of (Set ↑X))