The category of Boolean rings

This file defines BoolRing, the category of Boolean rings.

TODO

Finish the equivalence with BoolAlg.

structure BoolRing : Type (u + 1)

The category of Boolean rings.

• of :: (
• carrier : Type u

  The underlying type.

• booleanRing : BooleanRing ↑self
• )

@[implicit_reducible]

instance BoolRing.instCoeSortType : CoeSort BoolRing (Type u_1)

theorem BoolRing.coe_of (α : Type u_1) [BooleanRing α] : ↑{ carrier := α, booleanRing := inst✝ } = α

@[implicit_reducible]

instance BoolRing.instInhabited : Inhabited BoolRing

structure BoolRing.Hom (R : BoolRing) (S : BoolRing) : Type (max u_1 u_2)

The type of morphisms in BoolRing.

• hom' : ↑R →+* ↑S

  The underlying ring hom.

theorem BoolRing.Hom.ext_iff {R : BoolRing} {S : BoolRing} {x y : R.Hom S} : x = y ↔ x.hom' = y.hom'

theorem BoolRing.Hom.ext {R : BoolRing} {S : BoolRing} {x y : R.Hom S} (hom' : x.hom' = y.hom') : x = y

@[implicit_reducible]

instance BoolRing.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} BoolRing

@[implicit_reducible]

instance BoolRing.instConcreteCategoryRingHomCarrier : CategoryTheory.ConcreteCategory BoolRing fun (x1 x2 : BoolRing) => ↑x1 →+* ↑x2

@[reducible, inline]

abbrev BoolRing.Hom.hom {X Y : BoolRing} (f : X.Hom Y) : ↑X →+* ↑Y

Turn a morphism in BoolRing back into a RingHom.

@[reducible, inline]

abbrev BoolRing.ofHom {R S : Type u} [BooleanRing R] [BooleanRing S] (f : R →+* S) : { carrier := R, booleanRing := inst✝ } ⟶ { carrier := S, booleanRing := inst✝¹ }

Typecheck a RingHom as a morphism in BoolRing.

theorem BoolRing.hom_ext {R S : BoolRing} {f g : R ⟶ S} (hf : Hom.hom f = Hom.hom g) : f = g

theorem BoolRing.hom_ext_iff {R S : BoolRing} {f g : R ⟶ S} : f = g ↔ Hom.hom f = Hom.hom g

@[implicit_reducible]

instance BoolRing.hasForgetToCommRing : CategoryTheory.HasForget₂ BoolRing CommRingCat

def BoolRing.Iso.mk {α β : BoolRing} (e : ↑α ≃+* ↑β) : α ≅ β

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

@[simp]

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

@[simp]

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

Equivalence between BoolAlg and BoolRing

@[implicit_reducible]

instance instBooleanAlgebraCarrierToBddLatToBddDistLat {X : BoolAlg} : BooleanAlgebra ↑X.toBddDistLat.toBddLat.toLat

@[implicit_reducible]

instance instBooleanRingCarrierToBddLatToBddDistLatOfAsBoolAlg {R : Type u} [BooleanRing R] : BooleanRing ↑{ carrier := AsBoolAlg R, str := instBooleanAlgebraAsBoolAlg }.toBddDistLat.toBddLat.toLat

@[implicit_reducible]

instance BoolRing.hasForgetToBoolAlg : CategoryTheory.HasForget₂ BoolRing BoolAlg

@[simp]

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

@[simp]

theorem BoolRing.hasForgetToBoolAlg_forget₂_map {X✝ Y✝ : BoolRing} (f : X✝ ⟶ Y✝) : CategoryTheory.HasForget₂.forget₂.map f = BoolAlg.ofHom (Hom.hom f).asBoolAlg

@[implicit_reducible]

instance BoolAlg.hasForgetToBoolRing : CategoryTheory.HasForget₂ BoolAlg BoolRing

@[simp]

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

@[simp]

theorem BoolAlg.hasForgetToBoolRing_forget₂_map {X✝ Y✝ : BoolAlg} (f : X✝ ⟶ Y✝) : CategoryTheory.HasForget₂.forget₂.map f = BoolRing.ofHom (Hom.hom f).asBoolRing

def boolRingCatEquivBoolAlg : BoolRing ≌ BoolAlg

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

@[simp]

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

@[simp]

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