Boolean rings

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-05-24.
Last modified on 2024-10-05.

module commutative-algebra.boolean-rings where
Imports 
open import commutative-algebra.commutative-rings

open import foundation.dependent-pair-types
open import foundation.universe-levels

open import ring-theory.idempotent-elements-rings

Idea

A boolean ring is a commutative ring in which every element is idempotent.

Definition

is-boolean-Commutative-Ring :
  {l : Level} (A : Commutative-Ring l) → UU l
is-boolean-Commutative-Ring A =
  (x : type-Commutative-Ring A) →
  is-idempotent-element-Ring (ring-Commutative-Ring A) x

Boolean-Ring : (l : Level) → UU (lsuc l)
Boolean-Ring l = Σ (Commutative-Ring l) is-boolean-Commutative-Ring

module _
  {l : Level} (A : Boolean-Ring l)
  where

  commutative-ring-Boolean-Ring : Commutative-Ring l
  commutative-ring-Boolean-Ring = pr1 A

Recent changes