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.
- carrier : Type u
The underlying type.
- booleanRing : BooleanRing ↑self
Instances For
Equations
- BoolRing.instCoeSortType = { coe := BoolRing.carrier }
@[reducible, inline]
Construct a bundled BoolRing
from a BooleanRing
.
Equations
- BoolRing.of α = BoolRing.mk✝ α
Instances For
Equations
- BoolRing.instInhabited = { default := BoolRing.of PUnit.{?u.3 + 1} }
@[reducible, inline]
abbrev
BoolRing.ofHom
{R S : Type u}
[BooleanRing R]
[BooleanRing S]
(f : R →+* S)
:
BoolRing.of R ⟶ BoolRing.of S
Typecheck a RingHom
as a morphism in BoolRing
.
Equations
- BoolRing.ofHom f = { hom := f }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Constructs an isomorphism of Boolean rings from a ring isomorphism between them.
Equations
- BoolRing.Iso.mk e = { hom := { hom := ↑e }, inv := { hom := ↑e.symm }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
@[simp]
@[simp]
theorem
BoolRing.Iso.mk_inv_hom
{α β : BoolRing}
(e : ↑α ≃+* ↑β)
:
(BoolRing.Iso.mk e).inv.hom = ↑e.symm
instance
instBooleanAlgebraαLatticeToLatToBddLatToBddDistLat
{X : BoolAlg}
:
BooleanAlgebra ↑X.toBddDistLat.toBddLat.toLat
Equations
- instBooleanAlgebraαLatticeToLatToBddLatToBddDistLat = X.instBooleanAlgebra
instance
instBooleanRingαLatticeToLatToBddLatToBddDistLatOfAsBoolAlg
{R : Type u}
[BooleanRing R]
:
BooleanRing ↑(BoolAlg.of (AsBoolAlg R)).toBddDistLat.toBddLat.toLat
Equations
- instBooleanRingαLatticeToLatToBddLatToBddDistLatOfAsBoolAlg = inferInstanceAs (BooleanRing R)
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
BoolRing.hasForgetToBoolAlg_forget₂_map
{R S : BoolRing}
(f : R ⟶ S)
:
CategoryTheory.HasForget₂.forget₂.map f = f.hom.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.
@[simp]
theorem
BoolAlg.hasForgetToBoolRing_forget₂_obj_carrier
(X : BoolAlg)
:
↑(CategoryTheory.HasForget₂.forget₂.obj X) = AsBoolRing ↑X
@[simp]
theorem
BoolAlg.hasForgetToBoolRing_forget₂_map_hom
{x✝ x✝¹ : BoolAlg}
(f : x✝ ⟶ x✝¹)
:
(CategoryTheory.HasForget₂.forget₂.map f).hom = BoundedLatticeHom.asBoolRing f
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
@[simp]
@[simp]