Documentation

Mathlib.Order.Category.BoolAlg

The category of boolean algebras #

This defines BoolAlg, the category of boolean algebras.

source
def BoolAlg :
Type (u_1 + 1)

The category of boolean algebras.

Equations
Instances For
    source
    instance BoolAlg.instCoeSortBoolAlgType :
    CoeSort BoolAlg (Type u_1)
    Equations
    source
    instance BoolAlg.instBooleanAlgebra (X : BoolAlg) :
    BooleanAlgebra ↑X
    Equations
    source
    def BoolAlg.of (α : Type u_1) [BooleanAlgebra α] :
    BoolAlg

    Construct a bundled BoolAlg from a BooleanAlgebra.

    Equations
    Instances For
      source
      @[simp]
      theorem BoolAlg.coe_of (α : Type u_1) [BooleanAlgebra α] :
      ↑(BoolAlg.of α) = α
      source
      instance BoolAlg.instInhabitedBoolAlg :
      Inhabited BoolAlg
      Equations
      source
      def BoolAlg.toBddDistLat (X : BoolAlg) :
      BddDistLat

      Turn a BoolAlg into a BddDistLat by forgetting its complement operation.

      Equations
      Instances For
        source
        @[simp]
        theorem BoolAlg.coe_toBddDistLat (X : BoolAlg) :
        ↑(BoolAlg.toBddDistLat X).toDistLat = ↑X
        source
        instance BoolAlg.instLargeCategoryBoolAlg :
        CategoryTheory.LargeCategory BoolAlg
        Equations
        source
        instance BoolAlg.instConcreteCategoryBoolAlgInstLargeCategoryBoolAlg :
        CategoryTheory.ConcreteCategory BoolAlg
        Equations
        source
        instance BoolAlg.hasForgetToBddDistLat :
        CategoryTheory.HasForget₂ BoolAlg BddDistLat
        Equations
        source
        @[simp]
        theorem BoolAlg.hasForgetToHeytAlg_forget₂_obj_α (X : BoolAlg) :
        ↑(CategoryTheory.HasForget₂.forget₂.toPrefunctor.obj X) = ↑X
        source
        @[simp]
        theorem BoolAlg.hasForgetToHeytAlg_forget₂_obj_str (X : BoolAlg) :
        (CategoryTheory.HasForget₂.forget₂.toPrefunctor.obj X).str = inferInstance
        source
        @[simp]
        theorem BoolAlg.hasForgetToHeytAlg_forget₂_map_toFun {X : BoolAlg} {Y : BoolAlg} (f : BoundedLatticeHom ↑X ↑Y) (a : ↑X) :
        (CategoryTheory.HasForget₂.forget₂.toPrefunctor.map f) a = f a
        source
        instance BoolAlg.hasForgetToHeytAlg :
        CategoryTheory.HasForget₂ BoolAlg HeytAlg
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[simp]
        theorem BoolAlg.Iso.mk_inv_toLatticeHom_toSupHom_toFun {α : BoolAlg} {β : BoolAlg} (e : ↑α ≃o ↑β) (a : ↑β) :
        (BoolAlg.Iso.mk e).inv.toSupHom a = (OrderIso.symm e) a
        source
        @[simp]
        theorem BoolAlg.Iso.mk_hom_toLatticeHom_toSupHom_toFun {α : BoolAlg} {β : BoolAlg} (e : ↑α ≃o ↑β) (a : ↑α) :
        (BoolAlg.Iso.mk e).hom.toSupHom a = e a
        source
        def BoolAlg.Iso.mk {α : BoolAlg} {β : BoolAlg} (e : ↑α ≃o ↑β) :
        α ≅ β

        Constructs an equivalence between 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 BoolAlg.dual_obj (X : BoolAlg) :
          BoolAlg.dual.toPrefunctor.obj X = BoolAlg.of (↑X)ᵒᵈ
          source
          @[simp]
          theorem BoolAlg.dual_map {X : BoolAlg} {Y : BoolAlg} (a : BoundedLatticeHom ↑(BddDistLat.toBddLat (BoolAlg.toBddDistLat X)).toLat ↑(BddDistLat.toBddLat (BoolAlg.toBddDistLat Y)).toLat) :
          BoolAlg.dual.toPrefunctor.map a = BoundedLatticeHom.dual a
          source
          def BoolAlg.dual :
          CategoryTheory.Functor BoolAlg BoolAlg

          OrderDual as a functor.

          Equations
          Instances For
            source
            @[simp]
            theorem BoolAlg.dualEquiv_inverse :
            BoolAlg.dualEquiv.inverse = BoolAlg.dual
            source
            @[simp]
            theorem BoolAlg.dualEquiv_functor :
            BoolAlg.dualEquiv.functor = BoolAlg.dual
            source
            def BoolAlg.dualEquiv :
            BoolAlg ≌ BoolAlg

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

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem boolAlg_dual_comp_forget_to_bddDistLat :
              CategoryTheory.Functor.comp BoolAlg.dual (CategoryTheory.forget₂ BoolAlg BddDistLat) = CategoryTheory.Functor.comp (CategoryTheory.forget₂ BoolAlg BddDistLat) BddDistLat.dual