mathlib3 documentation

algebra.category.BoolRing

The category of Boolean rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines BoolRing, the category of Boolean rings.

TODO #

Finish the equivalence with BoolAlg.

source
def BoolRing  :
Type (u_1+1)

The category of Boolean rings.

Equations
Instances for BoolRing
source
@[protected, instance]
def BoolRing.has_coe_to_sort  :
has_coe_to_sort BoolRing (Type u_1)
Equations
source
@[protected, instance]
def BoolRing.boolean_ring (X : BoolRing) :
boolean_ring ↥X
Equations
source
def BoolRing.of (α : Type u_1) [boolean_ring α] :
BoolRing

Construct a bundled BoolRing from a boolean_ring.

Equations
source
@[simp]
theorem BoolRing.coe_of (α : Type u_1) [boolean_ring α] :
↥(BoolRing.of α) = α
source
@[protected, instance]
def BoolRing.inhabited  :
inhabited BoolRing
Equations
source
@[protected, instance]
def BoolRing.boolean_ring.to_comm_ring.category_theory.bundled_hom.parent_projection  :
category_theory.bundled_hom.parent_projection boolean_ring.to_comm_ring
Equations
source
@[protected, instance]
def BoolRing.large_category  :
category_theory.large_category BoolRing
source
@[protected, instance]
def BoolRing.concrete_category  :
category_theory.concrete_category BoolRing
source
@[simp]
theorem BoolRing.has_forget_to_CommRing_forget₂_obj_α (X : category_theory.bundled boolean_ring) :
↥(category_theory.has_forget₂.forget₂.obj X) = ↥X
source
@[simp]
theorem BoolRing.has_forget_to_CommRing_forget₂_obj_str_add (X : category_theory.bundled boolean_ring) (ᾰ ᾰ_1 : X.α) :
ᾰ + ᾰ_1 = ring.add ᾰ ᾰ_1
source
@[protected, instance]
def BoolRing.has_forget_to_CommRing  :
category_theory.has_forget₂ BoolRing CommRing
Equations
source
@[simp]
theorem BoolRing.has_forget_to_CommRing_forget₂_obj_str_zero (X : category_theory.bundled boolean_ring) :
0 = ring.zero
source
@[simp]
theorem BoolRing.has_forget_to_CommRing_forget₂_obj_str_nsmul (X : category_theory.bundled boolean_ring) (ᾰ : ℕ) (ᾰ_1 : X.α) :
comm_ring.nsmul ᾰ ᾰ_1 = ring.nsmul ᾰ ᾰ_1
source
@[simp]
theorem BoolRing.has_forget_to_CommRing_forget₂_obj_str_sub (X : category_theory.bundled boolean_ring) (ᾰ ᾰ_1 : X.α) :
ᾰ - ᾰ_1 = ring.sub ᾰ ᾰ_1
source
@[simp]
theorem BoolRing.has_forget_to_CommRing_forget₂_map (X Y : category_theory.bundled boolean_ring) (f : X ⟶ Y) :
category_theory.has_forget₂.forget₂.map f = f
source
@[simp]
theorem BoolRing.has_forget_to_CommRing_forget₂_obj_str_mul (X : category_theory.bundled boolean_ring) (ᾰ ᾰ_1 : X.α) :
ᾰ * ᾰ_1 = ring.mul ᾰ ᾰ_1
source
@[simp]
theorem BoolRing.has_forget_to_CommRing_forget₂_obj_str_neg (X : category_theory.bundled boolean_ring) (ᾰ : X.α) :
-ᾰ = ring.neg ᾰ
source
@[simp]
theorem BoolRing.has_forget_to_CommRing_forget₂_obj_str_npow (X : category_theory.bundled boolean_ring) (ᾰ : ℕ) (ᾰ_1 : X.α) :
comm_ring.npow ᾰ ᾰ_1 = ring.npow ᾰ ᾰ_1
source
@[simp]
theorem BoolRing.has_forget_to_CommRing_forget₂_obj_str_int_cast (X : category_theory.bundled boolean_ring) (ᾰ : ℤ) :
comm_ring.int_cast ᾰ = ring.int_cast ᾰ
source
@[simp]
theorem BoolRing.has_forget_to_CommRing_forget₂_obj_str_zsmul (X : category_theory.bundled boolean_ring) (ᾰ : ℤ) (ᾰ_1 : X.α) :
comm_ring.zsmul ᾰ ᾰ_1 = ring.zsmul ᾰ ᾰ_1
source
@[simp]
theorem BoolRing.has_forget_to_CommRing_forget₂_obj_str_nat_cast (X : category_theory.bundled boolean_ring) (ᾰ : ℕ) :
comm_ring.nat_cast ᾰ = ring.nat_cast ᾰ
source
@[simp]
theorem BoolRing.has_forget_to_CommRing_forget₂_obj_str_one (X : category_theory.bundled boolean_ring) :
1 = ring.one
source
def BoolRing.iso.mk {α β : BoolRing} (e : ↥α ≃+* ↥β) :
α ≅ β

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

Equations
source
@[simp]
theorem BoolRing.iso.mk_inv {α β : BoolRing} (e : ↥α ≃+* ↥β) :
(BoolRing.iso.mk e).inv = ↑(e.symm)
source
@[simp]
theorem BoolRing.iso.mk_hom {α β : BoolRing} (e : ↥α ≃+* ↥β) :
(BoolRing.iso.mk e).hom = ↑e

Equivalence between BoolAlg and BoolRing #

source
@[protected, instance]
def BoolRing.has_forget_to_BoolAlg  :
category_theory.has_forget₂ BoolRing BoolAlg
Equations
source
@[simp]
theorem BoolRing.has_forget_to_BoolAlg_forget₂_map (X Y : BoolRing) (f : ↥X →+* ↥Y) :
category_theory.has_forget₂.forget₂.map f = f.as_boolalg
source
@[simp]
theorem BoolRing.has_forget_to_BoolAlg_forget₂_obj (X : BoolRing) :
category_theory.has_forget₂.forget₂.obj X = BoolAlg.of (as_boolalg ↥X)
source
@[protected, instance]
def BoolAlg.has_forget_to_BoolRing  :
category_theory.has_forget₂ BoolAlg BoolRing
Equations
source
@[simp]
theorem BoolAlg.has_forget_to_BoolRing_forget₂_map (X Y : BoolAlg) (f : bounded_lattice_hom ↥(X.to_BddDistLat.to_BddLat) ↥(Y.to_BddDistLat.to_BddLat)) :
category_theory.has_forget₂.forget₂.map f = f.as_boolring
source
@[simp]
theorem BoolAlg.has_forget_to_BoolRing_forget₂_obj (X : BoolAlg) :
category_theory.has_forget₂.forget₂.obj X = BoolRing.of (as_boolring ↥X)
source
@[simp]
theorem BoolRing_equiv_BoolAlg_functor  :
BoolRing_equiv_BoolAlg.functor = category_theory.forget₂ BoolRing BoolAlg
source
def BoolRing_equiv_BoolAlg  :
BoolRing ≌ BoolAlg

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

Equations
source
@[simp]
theorem BoolRing_equiv_BoolAlg_inverse  :
BoolRing_equiv_BoolAlg.inverse = category_theory.forget₂ BoolAlg BoolRing