Documentation

Mathlib.Algebra.Category.BoolRing

The category of Boolean rings #

This file defines BoolRing, the category of Boolean rings.

TODO #

Finish the equivalence with BoolAlg.

def BoolRing :
Type (u_1 + 1)

The category of Boolean rings.

Equations
Instances For
    Equations
    Equations
    • X.instBooleanRingα = X.str
    def BoolRing.of (α : Type u_1) [BooleanRing α] :

    Construct a bundled BoolRing from a BooleanRing.

    Equations
    Instances For
      @[simp]
      theorem BoolRing.coe_of (α : Type u_1) [BooleanRing α] :
      (BoolRing.of α) = α
      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem BoolRing.Iso.mk_inv {α : BoolRing} {β : BoolRing} (e : α ≃+* β) :
      (BoolRing.Iso.mk e).inv = e.symm
      @[simp]
      theorem BoolRing.Iso.mk_hom {α : BoolRing} {β : BoolRing} (e : α ≃+* β) :
      (BoolRing.Iso.mk e).hom = e
      def BoolRing.Iso.mk {α : BoolRing} {β : BoolRing} (e : α ≃+* β) :
      α β

      Constructs an isomorphism of Boolean rings from a ring isomorphism between them.

      Equations
      • BoolRing.Iso.mk e = { hom := e, inv := e.symm, hom_inv_id := , inv_hom_id := }
      Instances For

        Equivalence between BoolAlg and BoolRing #

        @[simp]
        theorem BoolRing.hasForgetToBoolAlg_forget₂_map {X : BoolRing} {Y : BoolRing} (f : X →+* Y) :
        CategoryTheory.HasForget₂.forget₂.map f = f.asBoolAlg
        @[simp]
        theorem BoolRing.hasForgetToBoolAlg_forget₂_obj (X : BoolRing) :
        CategoryTheory.HasForget₂.forget₂.obj X = BoolAlg.of (AsBoolAlg X)
        Equations
        • One or more equations did not get rendered due to their size.
        instance instBooleanAlgebraαLatticeToLatToBddLatToBddDistLat {X : BoolAlg} :
        BooleanAlgebra X.toBddDistLat.toBddLat.toLat
        Equations
        • instBooleanAlgebraαLatticeToLatToBddLatToBddDistLat = X.instBooleanAlgebra
        @[simp]
        theorem BoolAlg.hasForgetToBoolRing_forget₂_map {X : BoolAlg} {Y : BoolAlg} (f : BoundedLatticeHom X.toBddDistLat.toBddLat.toLat Y.toBddDistLat.toBddLat.toLat) :
        CategoryTheory.HasForget₂.forget₂.map f = f.asBoolRing
        @[simp]
        theorem BoolAlg.hasForgetToBoolRing_forget₂_obj (X : BoolAlg) :
        CategoryTheory.HasForget₂.forget₂.obj X = BoolRing.of (AsBoolRing X)
        Equations
        • One or more equations did not get rendered due to their size.

        The equivalence between Boolean rings and Boolean algebras. This is actually an isomorphism.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For