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.

• carrier : Type u

  The underlying type.

• booleanRing : BooleanRing ↑self

instance BoolRing.instCoeSortType : CoeSort BoolRing (Type u_1)

Equations

• BoolRing.instCoeSortType = { coe := BoolRing.carrier }

@[reducible, inline]

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

Construct a bundled BoolRing from a BooleanRing.

Equations

• BoolRing.of α = BoolRing.mk✝ α

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

instance BoolRing.instInhabited : Inhabited BoolRing

Equations

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

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 {R : BoolRing} {S : BoolRing} {x y : R.Hom S} (hom' : x.hom' = y.hom') : x = y

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

Equations

• BoolRing.instCategory = CategoryTheory.Category.mk @BoolRing.instCategory.proof_1 @BoolRing.instCategory.proof_2 @BoolRing.instCategory.proof_3

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

Equations

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

@[reducible, inline]

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

Turn a morphism in BoolRing back into a RingHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev BoolRing.ofHom {R S : Type u} [BooleanRing R] [BooleanRing S] (f : R →+* S) : of R ⟶ of S

Typecheck a RingHom as a morphism in BoolRing.

Equations

• BoolRing.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

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

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 := { hom' := ↑e }, inv := { hom' := ↑e.symm }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[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

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)

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 {R S : BoolRing} (f : R ⟶ S) : CategoryTheory.HasForget₂.forget₂.map f = (Hom.hom f).asBoolAlg

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_carrier (X : BoolAlg) : ↑(CategoryTheory.HasForget₂.forget₂.obj X) = AsBoolRing ↑X

@[simp]

theorem BoolAlg.hasForgetToBoolRing_forget₂_map {x✝ x✝¹ : BoolAlg} (f : x✝ ⟶ x✝¹) : CategoryTheory.HasForget₂.forget₂.map f = BoolRing.ofHom (BoundedLatticeHom.asBoolRing f)

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