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

• BoolRing = CategoryTheory.Bundled BooleanRing

instance BoolRing.instCoeSortType : CoeSort BoolRing (Type u_1)

Equations

• BoolRing.instCoeSortType = CategoryTheory.Bundled.coeSort

instance BoolRing.instBooleanRingα (X : BoolRing) : BooleanRing ↑X

Equations

• X.instBooleanRingα = X.str

def BoolRing.of (α : Type u_1) [BooleanRing α] : BoolRing

Construct a bundled BoolRing from a BooleanRing.

Equations

• BoolRing.of α = CategoryTheory.Bundled.of α

@[simp]

theorem BoolRing.coe_of (α : Type u_1) [BooleanRing α] : ↑(BoolRing.of α) = α

instance BoolRing.instInhabited : Inhabited BoolRing

Equations

• BoolRing.instInhabited = { default := BoolRing.of PUnit.{?u.3 + 1} }

instance BoolRing.instParentProjectionCommRingBooleanRingToCommRing : CategoryTheory.BundledHom.ParentProjection @BooleanRing.toCommRing

Equations

• BoolRing.instParentProjectionCommRingBooleanRingToCommRing = ⋯

instance instBoolRingLargeCategory : CategoryTheory.LargeCategory BoolRing

Equations

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

instance BoolRing.instConcreteCategory : CategoryTheory.ConcreteCategory BoolRing

Equations

• BoolRing.instConcreteCategory = id inferInstance

instance BoolRing.hasForgetToCommRing : CategoryTheory.HasForget₂ BoolRing CommRingCat

Equations

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

def BoolRing.Iso.mk {α β : 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 := ⋯ }

@[simp]

theorem BoolRing.Iso.mk_inv {α β : BoolRing} (e : ↑α ≃+* ↑β) : (BoolRing.Iso.mk e).inv = ↑e.symm

@[simp]

theorem BoolRing.Iso.mk_hom {α β : BoolRing} (e : ↑α ≃+* ↑β) : (BoolRing.Iso.mk e).hom = ↑e

Equivalence between BoolAlg and BoolRing

instance BoolRing.hasForgetToBoolAlg : CategoryTheory.HasForget₂ BoolRing BoolAlg

Equations

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

@[simp]

theorem BoolRing.hasForgetToBoolAlg_forget₂_obj (X : BoolRing) : CategoryTheory.HasForget₂.forget₂.obj X = BoolAlg.of (AsBoolAlg ↑X)

@[simp]

theorem BoolRing.hasForgetToBoolAlg_forget₂_map {x✝ x✝¹ : BoolRing} (f : ↑x✝ →+* ↑x✝¹) : CategoryTheory.HasForget₂.forget₂.map f = f.asBoolAlg

instance instBooleanAlgebraαLatticeToLatToBddLatToBddDistLat {X : BoolAlg} : BooleanAlgebra ↑X.toBddDistLat.toBddLat.toLat

Equations

• instBooleanAlgebraαLatticeToLatToBddLatToBddDistLat = X.instBooleanAlgebra

instance BoolAlg.hasForgetToBoolRing : CategoryTheory.HasForget₂ BoolAlg BoolRing

Equations

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

@[simp]

theorem BoolAlg.hasForgetToBoolRing_forget₂_obj (X : BoolAlg) : CategoryTheory.HasForget₂.forget₂.obj X = BoolRing.of (AsBoolRing ↑X)

@[simp]

theorem BoolAlg.hasForgetToBoolRing_forget₂_map {x✝ x✝¹ : BoolAlg} (f : BoundedLatticeHom ↑x✝.toBddDistLat.toBddLat.toLat ↑x✝¹.toBddDistLat.toBddLat.toLat) : CategoryTheory.HasForget₂.forget₂.map f = f.asBoolRing

def boolRingCatEquivBoolAlg : BoolRing ≌ BoolAlg

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.

@[simp]

theorem boolRingCatEquivBoolAlg_functor : boolRingCatEquivBoolAlg.functor = CategoryTheory.forget₂ BoolRing BoolAlg

@[simp]

theorem boolRingCatEquivBoolAlg_inverse : boolRingCatEquivBoolAlg.inverse = CategoryTheory.forget₂ BoolAlg BoolRing