Commutative rings
module commutative-algebra.commutative-rings where
Imports
open import commutative-algebra.commutative-semirings open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.natural-numbers open import foundation.binary-embeddings open import foundation.binary-equivalences open import foundation.dependent-pair-types open import foundation.embeddings open import foundation.equivalences open import foundation.identity-types open import foundation.injective-maps open import foundation.interchange-law open import foundation.involutions open import foundation.negation open import foundation.propositions open import foundation.sets open import foundation.unital-binary-operations open import foundation.universe-levels open import group-theory.abelian-groups open import group-theory.commutative-monoids open import group-theory.groups open import group-theory.monoids open import group-theory.semigroups open import lists.concatenation-lists open import lists.lists open import ring-theory.rings open import ring-theory.semirings
Idea
A ring A is said to be commutative if its multiplicative operation is
commutative, i.e., if xy = yx for all x, y ∈ A.
Definition
Commutative rings
is-commutative-Ring : { l : Level} → Ring l → UU l is-commutative-Ring A = (x y : type-Ring A) → mul-Ring A x y ＝ mul-Ring A y x is-prop-is-commutative-Ring : { l : Level} (A : Ring l) → is-prop (is-commutative-Ring A) is-prop-is-commutative-Ring A = is-prop-Π ( λ x → is-prop-Π ( λ y → is-set-type-Ring A (mul-Ring A x y) (mul-Ring A y x))) Commutative-Ring : ( l : Level) → UU (lsuc l) Commutative-Ring l = Σ (Ring l) is-commutative-Ring module _ {l : Level} (A : Commutative-Ring l) where ring-Commutative-Ring : Ring l ring-Commutative-Ring = pr1 A ab-Commutative-Ring : Ab l ab-Commutative-Ring = ab-Ring ring-Commutative-Ring set-Commutative-Ring : Set l set-Commutative-Ring = set-Ring ring-Commutative-Ring type-Commutative-Ring : UU l type-Commutative-Ring = type-Ring ring-Commutative-Ring is-set-type-Commutative-Ring : is-set type-Commutative-Ring is-set-type-Commutative-Ring = is-set-type-Ring ring-Commutative-Ring
Addition in a commutative ring
has-associative-add-Commutative-Ring : has-associative-mul-Set set-Commutative-Ring has-associative-add-Commutative-Ring = has-associative-add-Ring ring-Commutative-Ring add-Commutative-Ring : type-Commutative-Ring → type-Commutative-Ring → type-Commutative-Ring add-Commutative-Ring = add-Ring ring-Commutative-Ring add-Commutative-Ring' : type-Commutative-Ring → type-Commutative-Ring → type-Commutative-Ring add-Commutative-Ring' = add-Ring' ring-Commutative-Ring ap-add-Commutative-Ring : {x x' y y' : type-Commutative-Ring} → (x ＝ x') → (y ＝ y') → add-Commutative-Ring x y ＝ add-Commutative-Ring x' y' ap-add-Commutative-Ring = ap-add-Ring ring-Commutative-Ring associative-add-Commutative-Ring : (x y z : type-Commutative-Ring) → ( add-Commutative-Ring (add-Commutative-Ring x y) z) ＝ ( add-Commutative-Ring x (add-Commutative-Ring y z)) associative-add-Commutative-Ring = associative-add-Ring ring-Commutative-Ring additive-semigroup-Commutative-Ring : Semigroup l additive-semigroup-Commutative-Ring = semigroup-Ab ab-Commutative-Ring is-group-additive-semigroup-Commutative-Ring : is-group additive-semigroup-Commutative-Ring is-group-additive-semigroup-Commutative-Ring = is-group-Ab ab-Commutative-Ring commutative-add-Commutative-Ring : (x y : type-Commutative-Ring) → Id (add-Commutative-Ring x y) (add-Commutative-Ring y x) commutative-add-Commutative-Ring = commutative-add-Ab ab-Commutative-Ring interchange-add-add-Commutative-Ring : (x y x' y' : type-Commutative-Ring) → ( add-Commutative-Ring ( add-Commutative-Ring x y) ( add-Commutative-Ring x' y')) ＝ ( add-Commutative-Ring ( add-Commutative-Ring x x') ( add-Commutative-Ring y y')) interchange-add-add-Commutative-Ring = interchange-add-add-Ring ring-Commutative-Ring right-swap-add-Commutative-Ring : (x y z : type-Commutative-Ring) → ( add-Commutative-Ring (add-Commutative-Ring x y) z) ＝ ( add-Commutative-Ring (add-Commutative-Ring x z) y) right-swap-add-Commutative-Ring = right-swap-add-Ring ring-Commutative-Ring left-swap-add-Commutative-Ring : (x y z : type-Commutative-Ring) → ( add-Commutative-Ring x (add-Commutative-Ring y z)) ＝ ( add-Commutative-Ring y (add-Commutative-Ring x z)) left-swap-add-Commutative-Ring = left-swap-add-Ring ring-Commutative-Ring is-equiv-add-Commutative-Ring : (x : type-Commutative-Ring) → is-equiv (add-Commutative-Ring x) is-equiv-add-Commutative-Ring = is-equiv-add-Ab ab-Commutative-Ring is-equiv-add-Commutative-Ring' : (x : type-Commutative-Ring) → is-equiv (add-Commutative-Ring' x) is-equiv-add-Commutative-Ring' = is-equiv-add-Ab' ab-Commutative-Ring is-binary-equiv-add-Commutative-Ring : is-binary-equiv add-Commutative-Ring pr1 is-binary-equiv-add-Commutative-Ring = is-equiv-add-Commutative-Ring' pr2 is-binary-equiv-add-Commutative-Ring = is-equiv-add-Commutative-Ring is-binary-emb-add-Commutative-Ring : is-binary-emb add-Commutative-Ring is-binary-emb-add-Commutative-Ring = is-binary-emb-add-Ab ab-Commutative-Ring is-emb-add-Commutative-Ring : (x : type-Commutative-Ring) → is-emb (add-Commutative-Ring x) is-emb-add-Commutative-Ring = is-emb-add-Ab ab-Commutative-Ring is-emb-add-Commutative-Ring' : (x : type-Commutative-Ring) → is-emb (add-Commutative-Ring' x) is-emb-add-Commutative-Ring' = is-emb-add-Ab' ab-Commutative-Ring is-injective-add-Commutative-Ring : (x : type-Commutative-Ring) → is-injective (add-Commutative-Ring x) is-injective-add-Commutative-Ring = is-injective-add-Ab ab-Commutative-Ring is-injective-add-Commutative-Ring' : (x : type-Commutative-Ring) → is-injective (add-Commutative-Ring' x) is-injective-add-Commutative-Ring' = is-injective-add-Ab' ab-Commutative-Ring
The zero element of a commutative ring
has-zero-Commutative-Ring : is-unital add-Commutative-Ring has-zero-Commutative-Ring = has-zero-Ring ring-Commutative-Ring zero-Commutative-Ring : type-Commutative-Ring zero-Commutative-Ring = zero-Ring ring-Commutative-Ring is-zero-Commutative-Ring : type-Commutative-Ring → UU l is-zero-Commutative-Ring = is-zero-Ring ring-Commutative-Ring is-nonzero-Commutative-Ring : type-Commutative-Ring → UU l is-nonzero-Commutative-Ring = is-nonzero-Ring ring-Commutative-Ring is-zero-commutative-ring-Prop : type-Commutative-Ring → Prop l is-zero-commutative-ring-Prop x = Id-Prop set-Commutative-Ring x zero-Commutative-Ring is-nonzero-commutative-ring-Prop : type-Commutative-Ring → Prop l is-nonzero-commutative-ring-Prop x = neg-Prop (is-zero-commutative-ring-Prop x) left-unit-law-add-Commutative-Ring : (x : type-Commutative-Ring) → add-Commutative-Ring zero-Commutative-Ring x ＝ x left-unit-law-add-Commutative-Ring = left-unit-law-add-Ring ring-Commutative-Ring right-unit-law-add-Commutative-Ring : (x : type-Commutative-Ring) → add-Commutative-Ring x zero-Commutative-Ring ＝ x right-unit-law-add-Commutative-Ring = right-unit-law-add-Ring ring-Commutative-Ring
Additive inverses in a commutative ring
has-negatives-Commutative-Ring : is-group' additive-semigroup-Commutative-Ring has-zero-Commutative-Ring has-negatives-Commutative-Ring = has-negatives-Ab ab-Commutative-Ring neg-Commutative-Ring : type-Commutative-Ring → type-Commutative-Ring neg-Commutative-Ring = neg-Ring ring-Commutative-Ring left-inverse-law-add-Commutative-Ring : (x : type-Commutative-Ring) → add-Commutative-Ring (neg-Commutative-Ring x) x ＝ zero-Commutative-Ring left-inverse-law-add-Commutative-Ring = left-inverse-law-add-Ring ring-Commutative-Ring right-inverse-law-add-Commutative-Ring : (x : type-Commutative-Ring) → add-Commutative-Ring x (neg-Commutative-Ring x) ＝ zero-Commutative-Ring right-inverse-law-add-Commutative-Ring = right-inverse-law-add-Ring ring-Commutative-Ring neg-neg-Commutative-Ring : (x : type-Commutative-Ring) → neg-Commutative-Ring (neg-Commutative-Ring x) ＝ x neg-neg-Commutative-Ring = neg-neg-Ab ab-Commutative-Ring distributive-neg-add-Commutative-Ring : (x y : type-Commutative-Ring) → neg-Commutative-Ring (add-Commutative-Ring x y) ＝ add-Commutative-Ring (neg-Commutative-Ring x) (neg-Commutative-Ring y) distributive-neg-add-Commutative-Ring = distributive-neg-add-Ab ab-Commutative-Ring
Multiplication in a commutative ring
has-associative-mul-Commutative-Ring : has-associative-mul-Set set-Commutative-Ring has-associative-mul-Commutative-Ring = has-associative-mul-Ring ring-Commutative-Ring mul-Commutative-Ring : (x y : type-Commutative-Ring) → type-Commutative-Ring mul-Commutative-Ring = mul-Ring ring-Commutative-Ring mul-Commutative-Ring' : (x y : type-Commutative-Ring) → type-Commutative-Ring mul-Commutative-Ring' = mul-Ring' ring-Commutative-Ring ap-mul-Commutative-Ring : {x x' y y' : type-Commutative-Ring} (p : Id x x') (q : Id y y') → Id (mul-Commutative-Ring x y) (mul-Commutative-Ring x' y') ap-mul-Commutative-Ring p q = ap-binary mul-Commutative-Ring p q associative-mul-Commutative-Ring : (x y z : type-Commutative-Ring) → mul-Commutative-Ring (mul-Commutative-Ring x y) z ＝ mul-Commutative-Ring x (mul-Commutative-Ring y z) associative-mul-Commutative-Ring = associative-mul-Ring ring-Commutative-Ring multiplicative-semigroup-Commutative-Ring : Semigroup l pr1 multiplicative-semigroup-Commutative-Ring = set-Commutative-Ring pr2 multiplicative-semigroup-Commutative-Ring = has-associative-mul-Commutative-Ring left-distributive-mul-add-Commutative-Ring : (x y z : type-Commutative-Ring) → ( mul-Commutative-Ring x (add-Commutative-Ring y z)) ＝ ( add-Commutative-Ring ( mul-Commutative-Ring x y) ( mul-Commutative-Ring x z)) left-distributive-mul-add-Commutative-Ring = left-distributive-mul-add-Ring ring-Commutative-Ring right-distributive-mul-add-Commutative-Ring : (x y z : type-Commutative-Ring) → ( mul-Commutative-Ring (add-Commutative-Ring x y) z) ＝ ( add-Commutative-Ring ( mul-Commutative-Ring x z) ( mul-Commutative-Ring y z)) right-distributive-mul-add-Commutative-Ring = right-distributive-mul-add-Ring ring-Commutative-Ring commutative-mul-Commutative-Ring : (x y : type-Commutative-Ring) → mul-Commutative-Ring x y ＝ mul-Commutative-Ring y x commutative-mul-Commutative-Ring = pr2 A
Multiplicative units in a commutative ring
is-unital-Commutative-Ring : is-unital mul-Commutative-Ring is-unital-Commutative-Ring = is-unital-Ring ring-Commutative-Ring multiplicative-monoid-Commutative-Ring : Monoid l multiplicative-monoid-Commutative-Ring = multiplicative-monoid-Ring ring-Commutative-Ring one-Commutative-Ring : type-Commutative-Ring one-Commutative-Ring = one-Ring ring-Commutative-Ring left-unit-law-mul-Commutative-Ring : (x : type-Commutative-Ring) → mul-Commutative-Ring one-Commutative-Ring x ＝ x left-unit-law-mul-Commutative-Ring = left-unit-law-mul-Ring ring-Commutative-Ring right-unit-law-mul-Commutative-Ring : (x : type-Commutative-Ring) → mul-Commutative-Ring x one-Commutative-Ring ＝ x right-unit-law-mul-Commutative-Ring = right-unit-law-mul-Ring ring-Commutative-Ring right-swap-mul-Commutative-Ring : (x y z : type-Commutative-Ring) → mul-Commutative-Ring (mul-Commutative-Ring x y) z ＝ mul-Commutative-Ring (mul-Commutative-Ring x z) y right-swap-mul-Commutative-Ring x y z = ( associative-mul-Commutative-Ring x y z) ∙ ( ( ap ( mul-Commutative-Ring x) ( commutative-mul-Commutative-Ring y z)) ∙ ( inv (associative-mul-Commutative-Ring x z y))) left-swap-mul-Commutative-Ring : (x y z : type-Commutative-Ring) → mul-Commutative-Ring x (mul-Commutative-Ring y z) ＝ mul-Commutative-Ring y (mul-Commutative-Ring x z) left-swap-mul-Commutative-Ring x y z = ( inv (associative-mul-Commutative-Ring x y z)) ∙ ( ( ap ( mul-Commutative-Ring' z) ( commutative-mul-Commutative-Ring x y)) ∙ ( associative-mul-Commutative-Ring y x z)) interchange-mul-mul-Commutative-Ring : (x y z w : type-Commutative-Ring) → mul-Commutative-Ring ( mul-Commutative-Ring x y) ( mul-Commutative-Ring z w) ＝ mul-Commutative-Ring ( mul-Commutative-Ring x z) ( mul-Commutative-Ring y w) interchange-mul-mul-Commutative-Ring = interchange-law-commutative-and-associative mul-Commutative-Ring commutative-mul-Commutative-Ring associative-mul-Commutative-Ring
The zero laws for multiplication of a commutative ring
left-zero-law-mul-Commutative-Ring : (x : type-Commutative-Ring) → mul-Commutative-Ring zero-Commutative-Ring x ＝ zero-Commutative-Ring left-zero-law-mul-Commutative-Ring = left-zero-law-mul-Ring ring-Commutative-Ring right-zero-law-mul-Commutative-Ring : (x : type-Commutative-Ring) → mul-Commutative-Ring x zero-Commutative-Ring ＝ zero-Commutative-Ring right-zero-law-mul-Commutative-Ring = right-zero-law-mul-Ring ring-Commutative-Ring
Commutative rings are commutative semirings
multiplicative-commutative-monoid-Commutative-Ring : Commutative-Monoid l pr1 multiplicative-commutative-monoid-Commutative-Ring = multiplicative-monoid-Ring ring-Commutative-Ring pr2 multiplicative-commutative-monoid-Commutative-Ring = commutative-mul-Commutative-Ring semiring-Commutative-Ring : Semiring l semiring-Commutative-Ring = semiring-Ring ring-Commutative-Ring commutative-semiring-Commutative-Ring : Commutative-Semiring l pr1 commutative-semiring-Commutative-Ring = semiring-Commutative-Ring pr2 commutative-semiring-Commutative-Ring = commutative-mul-Commutative-Ring
Computing multiplication with minus one in a ring
neg-one-Commutative-Ring : type-Commutative-Ring neg-one-Commutative-Ring = neg-one-Ring ring-Commutative-Ring mul-neg-one-Commutative-Ring : (x : type-Commutative-Ring) → mul-Commutative-Ring neg-one-Commutative-Ring x ＝ neg-Commutative-Ring x mul-neg-one-Commutative-Ring = mul-neg-one-Ring ring-Commutative-Ring mul-neg-one-Commutative-Ring' : (x : type-Commutative-Ring) → mul-Commutative-Ring x neg-one-Commutative-Ring ＝ neg-Commutative-Ring x mul-neg-one-Commutative-Ring' = mul-neg-one-Ring' ring-Commutative-Ring is-involution-mul-neg-one-Commutative-Ring : is-involution (mul-Commutative-Ring neg-one-Commutative-Ring) is-involution-mul-neg-one-Commutative-Ring = is-involution-mul-neg-one-Ring ring-Commutative-Ring is-involution-mul-neg-one-Commutative-Ring' : is-involution (mul-Commutative-Ring' neg-one-Commutative-Ring) is-involution-mul-neg-one-Commutative-Ring' = is-involution-mul-neg-one-Ring' ring-Commutative-Ring
Left and right negative laws for multiplication
left-negative-law-mul-Commutative-Ring : (x y : type-Commutative-Ring) → mul-Commutative-Ring (neg-Commutative-Ring x) y ＝ neg-Commutative-Ring (mul-Commutative-Ring x y) left-negative-law-mul-Commutative-Ring = left-negative-law-mul-Ring ring-Commutative-Ring right-negative-law-mul-Commutative-Ring : (x y : type-Commutative-Ring) → mul-Commutative-Ring x (neg-Commutative-Ring y) ＝ neg-Commutative-Ring (mul-Commutative-Ring x y) right-negative-law-mul-Commutative-Ring = right-negative-law-mul-Ring ring-Commutative-Ring mul-neg-Commutative-Ring : (x y : type-Commutative-Ring) → mul-Commutative-Ring (neg-Commutative-Ring x) (neg-Commutative-Ring y) ＝ mul-Commutative-Ring x y mul-neg-Commutative-Ring = mul-neg-Ring ring-Commutative-Ring
Scalar multiplication of elements of a commutative ring by natural numbers
mul-nat-scalar-Commutative-Ring : ℕ → type-Commutative-Ring → type-Commutative-Ring mul-nat-scalar-Commutative-Ring = mul-nat-scalar-Ring ring-Commutative-Ring ap-mul-nat-scalar-Commutative-Ring : {m n : ℕ} {x y : type-Commutative-Ring} → (m ＝ n) → (x ＝ y) → mul-nat-scalar-Commutative-Ring m x ＝ mul-nat-scalar-Commutative-Ring n y ap-mul-nat-scalar-Commutative-Ring = ap-mul-nat-scalar-Ring ring-Commutative-Ring left-zero-law-mul-nat-scalar-Commutative-Ring : (x : type-Commutative-Ring) → mul-nat-scalar-Commutative-Ring 0 x ＝ zero-Commutative-Ring left-zero-law-mul-nat-scalar-Commutative-Ring = left-zero-law-mul-nat-scalar-Ring ring-Commutative-Ring right-zero-law-mul-nat-scalar-Commutative-Ring : (n : ℕ) → mul-nat-scalar-Commutative-Ring n zero-Commutative-Ring ＝ zero-Commutative-Ring right-zero-law-mul-nat-scalar-Commutative-Ring = right-zero-law-mul-nat-scalar-Ring ring-Commutative-Ring left-unit-law-mul-nat-scalar-Commutative-Ring : (x : type-Commutative-Ring) → mul-nat-scalar-Commutative-Ring 1 x ＝ x left-unit-law-mul-nat-scalar-Commutative-Ring = left-unit-law-mul-nat-scalar-Ring ring-Commutative-Ring left-nat-scalar-law-mul-Commutative-Ring : (n : ℕ) (x y : type-Commutative-Ring) → mul-Commutative-Ring (mul-nat-scalar-Commutative-Ring n x) y ＝ mul-nat-scalar-Commutative-Ring n (mul-Commutative-Ring x y) left-nat-scalar-law-mul-Commutative-Ring = left-nat-scalar-law-mul-Ring ring-Commutative-Ring right-nat-scalar-law-mul-Commutative-Ring : (n : ℕ) (x y : type-Commutative-Ring) → mul-Commutative-Ring x (mul-nat-scalar-Commutative-Ring n y) ＝ mul-nat-scalar-Commutative-Ring n (mul-Commutative-Ring x y) right-nat-scalar-law-mul-Commutative-Ring = right-nat-scalar-law-mul-Ring ring-Commutative-Ring left-distributive-mul-nat-scalar-add-Commutative-Ring : (n : ℕ) (x y : type-Commutative-Ring) → mul-nat-scalar-Commutative-Ring n (add-Commutative-Ring x y) ＝ add-Commutative-Ring ( mul-nat-scalar-Commutative-Ring n x) ( mul-nat-scalar-Commutative-Ring n y) left-distributive-mul-nat-scalar-add-Commutative-Ring = left-distributive-mul-nat-scalar-add-Ring ring-Commutative-Ring right-distributive-mul-nat-scalar-add-Commutative-Ring : (m n : ℕ) (x : type-Commutative-Ring) → mul-nat-scalar-Commutative-Ring (m +ℕ n) x ＝ add-Commutative-Ring ( mul-nat-scalar-Commutative-Ring m x) ( mul-nat-scalar-Commutative-Ring n x) right-distributive-mul-nat-scalar-add-Commutative-Ring = right-distributive-mul-nat-scalar-add-Ring ring-Commutative-Ring
Addition of a list of elements in a commutative ring
add-list-Commutative-Ring : list type-Commutative-Ring → type-Commutative-Ring add-list-Commutative-Ring = add-list-Ring ring-Commutative-Ring preserves-concat-add-list-Commutative-Ring : (l1 l2 : list type-Commutative-Ring) → Id ( add-list-Commutative-Ring (concat-list l1 l2)) ( add-Commutative-Ring ( add-list-Commutative-Ring l1) ( add-list-Commutative-Ring l2)) preserves-concat-add-list-Commutative-Ring = preserves-concat-add-list-Ring ring-Commutative-Ring