The category of Boolean rings #
This file defines BoolRing
, the category of Boolean rings.
TODO #
Finish the equivalence with BoolAlg
.
The category of Boolean rings.
Equations
Instances For
Equations
- BoolRing.instCoeSortType = CategoryTheory.Bundled.coeSort
Equations
- X.instBooleanRingα = X.str
Equations
- BoolRing.instInhabited = { default := BoolRing.of PUnit.{?u.3 + 1} }
Equations
- BoolRing.instConcreteCategory = id inferInstance
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
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
@[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.
@[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.