# 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.str
def BoolRing.of (α : Type u_1) [] :

Construct a bundled BoolRing from a BooleanRing.

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

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

Equations
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 =
@[simp]
theorem BoolRing.hasForgetToBoolAlg_forget₂_obj (X : BoolRing) :
CategoryTheory.HasForget₂.forget₂.obj X = BoolAlg.of ()
Equations
• One or more equations did not get rendered due to their size.
Equations
• instBooleanAlgebraαLatticeToLatToBddLatToBddDistLat =
@[simp]
theorem BoolAlg.hasForgetToBoolRing_forget₂_obj (X : BoolAlg) :
CategoryTheory.HasForget₂.forget₂.obj X =
@[simp]
theorem BoolAlg.hasForgetToBoolRing_forget₂_map {X : BoolAlg} {Y : BoolAlg} (f : BoundedLatticeHom .toLat .toLat) :
CategoryTheory.HasForget₂.forget₂.map f =
Equations
• One or more equations did not get rendered due to their size.
@[simp]
@[simp]

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