Rings

ClassRing #

A ring is a set with two binary operations, addition and multiplication, such that the set is an abelian group under addition, the multiplication is associative and has an identity element, and multiplication distributes over addition. Rings capture the arithmetic shared by the integers, the integers modulo $n$, polynomials and square matrices: one can add, subtract and multiply, but not necessarily divide. Commutative rings are the basic objects of commutative algebra and algebraic number theory, and rings in general are the setting in which divisibility, factorisation and congruences make sense.

Definition

A ring is a set $R$ with operations $(a, b) \mapsto a + b$ and $(a, b) \mapsto ab$ and elements $0, 1 \in R$ such that:

$R$ is an abelian group under addition, with identity $0$; the additive inverse of $a$ is written $-a$, and $a - b$ means $a + (-b)$;
multiplication is associative, $(ab)c = a(bc)$, and $1a = a = a1$ for all $a$;
multiplication distributes over addition on both sides: $a(b + c) = ab + ac$ and $(a + b)c = ac + bc$.

Multiplication need not be commutative. A ring in which $ab = ba$ for all $a$ and $b$ is a commutative ring. The list of axioms is longer than it needs to be: associativity of addition, a left additive identity, left additive inverses, associativity of multiplication, a two-sided multiplicative identity and the two distributive laws already determine a ring. Commutativity of addition then follows by expanding $(1 + 1)(a + b)$ with each distributive law in turn and comparing the two results.

A map between rings that preserves addition, multiplication and $1$ is a ring morphism, and a subset containing $0$ and $1$ and closed under addition, negation and multiplication is a subring.

Examples

The integers form a commutative ring under the usual operations (see the ring structure of the integers). The natural numbers do not, since they lack additive inverses.
For every natural number $n$, the integers modulo $n$ form a commutative ring; for $n = 0$ this is the ring of integers itself.
The rational, real and complex numbers are commutative rings, and in fact fields: every nonzero element has a multiplicative inverse.
If $R$ is a ring, the polynomials in one indeterminate with coefficients in $R$ form a ring, which is commutative when $R$ is.
For a positive integer $n$ and a ring $R$, the $n \times n$ matrices with entries in $R$ form a ring under matrix addition and multiplication. For $n \ge 2$ and $R$ nonzero it is not commutative: with $E$ the matrix whose only nonzero entry is a $1$ in the top left corner and $F$ the one with a $1$ just to the right of it, $EF = F$ but $FE = 0$.
The additive endomorphisms of an abelian group $A$, that is, the maps $f : A \to A$ with $f(x + y) = f(x) + f(y)$, form a ring with pointwise addition and composition as multiplication.
For any family of rings, the product of the family is a ring with componentwise operations. In particular the functions from any set to a ring form a ring.
The quaternions over the real numbers form a division ring: every nonzero element is invertible, yet multiplication is not commutative.
A set with one element is a ring, the zero ring, in which $0 = 1$.

Basic properties

Multiplying by zero gives zero: $0a = 0 = a0$, since $0a = (0 + 0)a = 0a + 0a$. Signs behave as in the integers: $(-a)b = -(ab)$, $(-a)(-b) = ab$ and $(-1)a = -a$. Multiplication also distributes over subtraction, for instance $a(b - c) = ab - ac$.

The zero ring is the only ring in which $0$ and $1$ coincide: $0 = 1$ holds exactly when $R$ has at most one element.

The elements of a ring that have a two-sided multiplicative inverse are its units, and they form a group under multiplication; for matrices over a field this is the general linear group.

For any ring $R$ there is a ring morphism from the integers to $R$, sending a natural number $n$ to the sum of $n$ copies of $1$ and $-n$ to the negative of that sum, and it is the only ring morphism from the integers to $R$. The characteristic of $R$ is the nonnegative generator of the kernel of this morphism.

In a commutative ring the binomial theorem holds: for all $x$, $y$ and every natural number $n$,

\[(x + y)^n = \sum_{m=0}^{n} \binom{n}{m} x^m y^{n-m}.\]

The same formula holds in any ring whenever $xy = yx$; without that hypothesis it can fail already for $n = 2$, where $(x + y)^2 = x^2 + xy + yx + y^2$.

The structure of a commutative ring is studied through its ideals, which are the kernels of ring morphisms and give rise to quotient rings. Prime and maximal ideals are those whose quotients are integral domains and fields respectively. An integral domain is a nontrivial commutative ring in which a product of nonzero elements is nonzero. Mathlib's notion of a domain, stated more generally for semirings, is a nontrivial ring in which nonzero elements can be cancelled from either side of an equation; for rings this is equivalent to having no zero divisors, and it does not require commutativity. Special classes of rings include Euclidean domains, unique factorisation domains, Noetherian rings and local rings.

Dropping additive inverses gives a semiring, such as the natural numbers; dropping the multiplicative identity or associativity gives non-unital or non-associative rings. An abelian group with a scalar multiplication by a ring that is associative, unital and distributive over both additions is a module, and a ring that is also a module over a commutative ring, compatibly, is an algebra. Rings and ring morphisms form the category of rings.

In Mathlib

In Mathlib a ring is a structure placed on a type, and is always associative and has a multiplicative identity; commutativity is a separate, stronger structure, and the variants without identity or without associativity are declared alongside. A ring is built as a semiring whose addition forms an abelian group, so facts proved for semirings apply to rings without change. Mathlib's semiring axioms include $0a = 0$ and $a0 = 0$, which are redundant for rings, and the structure also carries subtraction, integer and natural-number multiples, powers and the map from the integers, each with a default definition that a particular ring may replace by a better-behaved one. The zero ring is a ring: when an argument needs $0 \ne 1$, nontriviality is assumed separately. Many basic identities, such as the sign rules and the binomial theorem for commuting elements, are stated for weaker structures than rings and apply to rings as a special case.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibRing

Uses 2 · Used by 52

Statement usesGroup · Set

Used byErdős–Ginzburg–Ziv theorem · Associative algebra over a commutative ring · Free algebra of a commutative ring · Lie algebra · Tensor product of algebras · Coprime element · Euclidean domain · Greatest common divisor · Irreducible element · Least common multiple · Lucas-Lehmer primality test · Principal ideal domain · Unique factorisation domain · Characteristic of a ring · Characteristic p · Characteristic zero · Field · Field of fractions of an integral domain · Frobenius morphism · Perfect closure · First isomorphism theorem for commutative rings · Ideal of a commutative ring · Maximal ideal · Prime ideal · Quotient ring · Arithmetic functions · Perfection of a ring · Ring of Witt vectors · Multiplicity · Polynomial in one indeterminate · Polynomial in several indeterminates · Power series · Local ring · Localization · Noetherian ring · Ordered ring · Ring morphism · Subring · The category of rings · Affine subspace · Finite-dimensionality · Quotient space (Fundamentals) · The category of modules over a ring · Completion of a topological ring · Binomial inverse theorem · General linear group (Classical automorphism groups) · Orthogonal group · Complementary subspaces · Vector subspace · $\Z/n\Z$ and its invertible elements · Product of rings · Ring structure $\Z$

StructureRing morphism #

A ring morphism, or ring homomorphism, is a map between two rings that respects addition, multiplication and the multiplicative identity. Ring morphisms are the means of comparing rings: reduction of integers modulo $n$, evaluation of polynomials at a point and passage to a quotient ring are all ring morphisms, and the notions of ideal, quotient and isomorphism of rings are organized around them.

Definition

Let $R$ and $S$ be rings with identity. A map $f \colon R \to S$ is a ring morphism if, for all $x, y \in R$,

\[f(x + y) = f(x) + f(y), \qquad f(xy) = f(x)\,f(y), \qquad f(1) = 1.\]

The first condition says that $f$ is a morphism of additive groups, so it also gives $f(0) = 0$: from $f(0) = f(0 + 0) = f(0) + f(0)$ one cancels $f(0)$. The second and third say that $f$ is a morphism of multiplicative monoids. The condition $f(1) = 1$ does not follow from the other two. The zero map $\mathbb{Z} \to \mathbb{Z}$ preserves sums and products but sends $1$ to $0$, and the map $x \mapsto (x, 0)$ from $\mathbb{Z}$ to $\mathbb{Z} \times \mathbb{Z}$ preserves sums and products but sends $1$ to $(1, 0)$, which is not the identity $(1, 1)$. A map that preserves only sums and products is called a morphism of rings without identity.

An isomorphism of rings is a ring morphism with an inverse ring morphism. As for groups, the inverse map of a bijective ring morphism automatically preserves the operations, so every bijective ring morphism is an isomorphism.

Examples

The identity map of a ring is a ring morphism, and the composite of two ring morphisms is a ring morphism, so rings and their morphisms form a category.
For every ring $R$ there is a ring morphism from the integers to $R$, sending $n$ to $n \cdot 1$, and any two ring morphisms from $\mathbb{Z}$ to $R$ are equal. Its image is the smallest subring of $R$, and for $R = \mathbb{Z}/n\mathbb{Z}$ this morphism is reduction modulo $n$.
For an ideal $I$ of a commutative ring $R$, the map sending $x$ to its class $x + I$ is a surjective ring morphism from $R$ onto the quotient ring $R/I$, and its kernel is $I$.
For a commutative ring $R$ and an element $a \in R$, evaluation at $a$ is a ring morphism from the polynomial ring $R[X]$ to $R$, sending $p$ to the value $p(a)$.
For rings $R$ and $S$, the projection from the product ring $R \times S$ to $R$ is a ring morphism (see product of rings, of which $R \times S$ is the case of two factors).
If $R$ is a commutative ring of prime characteristic $p$, the binomial coefficients $\binom{p}{k}$ with $0 < k < p$ vanish in $R$, so $(x + y)^p = x^p + y^p$ and the map $x \mapsto x^p$ is a ring morphism of $R$ to itself, the Frobenius morphism.
Complex conjugation is a ring isomorphism of the complex numbers to themselves; it fixes every real number, so it is even an isomorphism of algebras over the real numbers.

Properties

Let $f \colon R \to S$ be a ring morphism. Besides $f(0) = 0$ and $f(1) = 1$, it preserves negatives and differences, $f(x - y) = f(x) - f(y)$, and natural-number powers, $f(x^n) = f(x)^n$. Since $f(u)f(u^{-1}) = f(u^{-1})f(u) = f(1) = 1$, it sends units to units, with $f(u)^{-1} = f(u^{-1})$.

If $S$ is not the zero ring then neither is $R$, because $f(1) = 1 \neq 0 = f(0)$ forces $1 \neq 0$ in $R$; equivalently, a ring with a morphism to a nonzero ring is nonzero. A ring morphism from a field $K$ to a nonzero ring is injective: its kernel is an ideal of $K$ not containing $1$, hence zero. Mathlib proves this for every simple ring, a nonzero ring whose only two-sided ideals are $0$ and the whole ring, which includes all fields and division rings.

For the rest of this section $R$ and $S$ are commutative. Two sets are attached to $f$: an ideal of $R$ and a subring of $S$.

The kernel $\ker f = \{ x \in R : f(x) = 0 \}$ is an ideal of $R$, and $f$ is injective exactly when its kernel is zero, since $f(x) = f(y)$ if and only if $x - y \in \ker f$. If $S$ is nonzero and has no zero divisors, for instance if $S$ is a field, then the kernel is a prime ideal.
The image $f(R)$ is a subring of $S$ (see subring).

More generally, the preimage of an ideal of $S$ is an ideal of $R$, and the preimage of a prime ideal is a prime ideal (see prime ideal). The image of an ideal need not be an ideal: the image of $\mathbb{Z}$ under the inclusion into $\mathbb{Q}$ is not an ideal of $\mathbb{Q}$. The first isomorphism theorem joins kernel and image: $R / \ker f$ is isomorphic to the image of $f$. Since every ideal is the kernel of its quotient map, the ideals of $R$ are exactly the kernels of ring morphisms out of $R$.

A ring morphism $i \colon R \to S$ from a commutative ring $R$ whose image commutes with every element of $S$ makes $S$ an algebra over $R$, with $r \cdot s = i(r)\,s$; see associative algebra. Ring morphisms are in particular monoid morphisms for multiplication and group morphisms for addition, and the kernel, image and first isomorphism theorem above parallel those of group theory.

In Mathlib

Mathlib defines ring morphisms in greater generality than rings with identity: the source and target need only be semirings in which multiplication is not assumed associative, so negatives are not required and the same structure serves for semirings such as the natural numbers. Because addition need not be cancellative in this setting, a morphism is required to preserve $0$ as well as $1$, sums and products. Morphisms are bundled: a morphism is a function packaged with proofs of these four properties, and it can be viewed as a monoid morphism, an additive monoid morphism or a morphism without identity. General results are usually stated for any type of maps that behaves like ring morphisms, so they apply equally to ring isomorphisms and to morphisms of algebras. Mathlib's ideals of a noncommutative ring are left ideals; the kernel is moreover recorded as a two-sided ideal, and the injectivity criterion and the first isomorphism theorem are stated without commutativity. The Frobenius morphism is defined for a commutative semiring of exponential characteristic $p$, which covers both prime characteristic $p$ and characteristic zero with $p = 1$.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibRingHom

Uses 2 · Used by 22

Statement usesRing · Group morphism

StructureThe category of rings #

The category of rings, usually written $\mathbf{Ring}$, is the category whose objects are rings and whose morphisms are ring morphisms. Viewing rings this way puts constructions such as products, quotients and polynomial rings in a common language of universal properties, and lets one compare rings with other algebraic structures through functors, for instance the functor that forgets the multiplication of a ring and remembers only its additive group.

Definition

Here a ring is associative and has a multiplicative identity $1$, but need not be commutative, and a ring morphism $f \colon R \to S$ preserves addition, multiplication and the identity: $f(1) = 1$. Mathlib defines the category of rings with these data:

an object is a ring $R$;
a morphism from $R$ to $S$ is a ring morphism $R \to S$;
the identity morphism of $R$ is the identity map of $R$, and the composite of $f \colon R \to S$ and $g \colon S \to T$ is the composite map $g \circ f$.

The category axioms hold because composition of functions is associative and the identity map is neutral for it.

Examples

Initial and terminal objects. For every ring $R$ there is exactly one ring morphism $\mathbb{Z} \to R$, sending $n$ to $n \cdot 1$, so the integers form an initial object (one with exactly one morphism to every object). The zero ring, in which $0 = 1$, receives exactly one morphism from every ring, so it is a terminal object (one with exactly one morphism from every object). A zero object, one that is both initial and terminal, would be isomorphic to the zero ring, since terminal objects are unique up to isomorphism; but the zero ring is not initial, as there is no ring morphism from it to $\mathbb{Z}$. So $\mathbf{Ring}$ has no zero object.
Products and equalizers. The product of a family of rings is their cartesian product with componentwise operations, together with the projections. The equalizer of two morphisms $f, g \colon R \to S$, the universal morphism into $R$ whose composites with $f$ and $g$ agree, is the inclusion of the subring $\{ r \in R : f(r) = g(r) \}$.
Coproducts. The coproduct of two rings, the universal ring receiving a morphism from each, is their free product, which need not be commutative even when both factors are commutative: the coproduct of $\mathbb{Z}[x]$ and $\mathbb{Z}[y]$ is the ring of polynomials in two non-commuting variables. For commutative rings the tensor product over $\mathbb{Z}$ is the coproduct only within the category of commutative rings.
Quotients. For a two-sided ideal $I$ of $R$, the projection $R \to R/I$ onto the quotient ring is the universal morphism out of $R$ that sends every element of $I$ to $0$.

Properties

Isomorphisms. The isomorphisms of $\mathbf{Ring}$ are the ring isomorphisms: every ring isomorphism is an isomorphism in the category, and every isomorphism in the category yields a ring isomorphism. Moreover, a morphism whose underlying function is bijective is an isomorphism, because the inverse function is automatically a ring morphism.
Monomorphisms and epimorphisms. A monomorphism is a morphism $f$ that can be cancelled on the left: $f \circ g = f \circ h$ implies $g = h$; an epimorphism is one that can be cancelled on the right. A morphism $f \colon R \to S$ is a monomorphism exactly when it is injective. An injective morphism is clearly a monomorphism. Conversely, morphisms $\mathbb{Z}[x] \to R$ correspond to elements of $R$, by evaluation at $x$; the variable $x$ may be sent to any element, because the image of $\mathbb{Z}$ in $R$ commutes with everything. If $f(a) = f(b)$, the morphisms sending $x$ to $a$ and to $b$ have the same composite with $f$, so they are equal and $a = b$. Epimorphisms need not be surjective. The inclusion $\mathbb{Z} \to \mathbb{Q}$ is an epimorphism, since a ring morphism out of $\mathbb{Q}$ must send $1/n$, for $n \neq 0$, to the inverse of the image of $n$ and is therefore determined by its values on $\mathbb{Z}$.
Limits. A limit of a diagram is a universal object with compatible morphisms to every object of the diagram; products and equalizers are examples. The category of rings has all small limits, and the forgetful functor to sets preserves them: the underlying set of a limit of rings is the limit of the underlying sets, with the operations defined pointwise. The same holds for the forgetful functor to abelian groups.
Colimits. Colimits are the dual notion, with morphisms from the diagram into the universal object. The category of rings has all small colimits. The forgetful functor does not preserve them in general: the coproduct of $\mathbb{Z}$ with itself is $\mathbb{Z}$, since $\mathbb{Z}$ is initial, while the coproduct of the underlying sets, the disjoint union of two copies of $\mathbb{Z}$, maps onto $\mathbb{Z}$ by identifying the two copies, and this comparison map is not injective. It does preserve filtered colimits, colimits over nonempty diagrams in which any two objects map to a common one and any two parallel arrows are made equal by a further arrow, so a directed union of rings is computed on underlying sets.
Free rings. The forgetful functor to sets has a left adjoint: a functor $F$ from sets to rings such that ring morphisms $F(X) \to R$ correspond to functions from $X$ to the underlying set of $R$, naturally in $X$ and $R$. It sends a set $X$ to the free ring on $X$, the ring of polynomials with integer coefficients in non-commuting variables indexed by $X$: ring morphisms from the free ring on $X$ to a ring $R$ correspond bijectively to functions from $X$ to $R$, the morphism attached to a function agrees with it on $X$, and a morphism out of the free ring is determined by its values on $X$.

Commutative rings form a full subcategory of $\mathbf{Ring}$, one that keeps every ring morphism between its objects. In other words, the forgetful functor from commutative rings to rings is fully faithful: it is bijective on each set of morphisms. Likewise, the forgetful functor from rings to semirings is fully faithful, because a semiring morphism between rings automatically preserves additive inverses. Fields form a further full subcategory, in which every morphism is injective, because every ring morphism from a field to a nonzero ring is injective. For a commutative ring $k$, the category of $k$-algebras maps to $\mathbf{Ring}$ by forgetting the structure map, and every ring $R$ has its own category of modules; a morphism of rings $R \to S$ turns every $S$-module into an $R$-module by restriction of scalars.

In Mathlib

Mathlib bundles each object as a type together with a ring structure on it. Morphisms are wrapped in a separate structure rather than being ring morphisms themselves, with translations in both directions: turning a ring morphism into a morphism of the category and back returns it, and turning a morphism into a ring morphism and back also returns it. This keeps the category's composition, written in diagrammatic order, apart from the composition of functions. The category is indexed by a universe level: it contains the rings whose underlying type lives in a fixed universe, and "small" limits and colimits are those indexed by categories of that size. Commutative rings, semirings and commutative semirings each have a parallel category, with forgetful functors between them.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibRingCat

Uses 3

Statement usesRing · Ring morphism · Category

StructureSubring #

A subring of a ring $R$ is a subset of $R$ that contains the identity $1$ and is closed under addition, negation and multiplication, so that it is a ring in its own right under the operations of $R$. Subrings are the substructures of ring theory, as subgroups are for groups: the integers inside the rational numbers, the Gaussian integers inside the complex numbers, and the image of any ring homomorphism are all subrings, and many constructions in algebra and number theory consist of finding the right subring of a larger, better understood ring.

Definition

Let $R$ be a ring with identity. A subset $S \subseteq R$ is a subring if

$0 \in S$ and $1 \in S$;
$a + b \in S$ and $-a \in S$ whenever $a, b \in S$;
$ab \in S$ whenever $a, b \in S$.

(The condition $0 \in S$ follows from the others, since $0 = 1 + (-1)$.)

Equivalently, $S$ is an additive subgroup of $R$ that is closed under multiplication and contains the identity of $R$. With the operations restricted from $R$, a subring is itself a ring, and the inclusion $S \to R$ is a ring homomorphism.

A convenient test: a subset $S$ is a subring exactly when $1 \in S$ and $S$ is closed under subtraction and multiplication. Indeed a subring is closed under subtraction; conversely, from $1 \in S$ and closure under subtraction one gets $0 = 1 - 1$, then $-a = 0 - a$ and $a + b = a - (-b)$.

The requirement that $S$ contain the identity of $R$, not merely some identity of its own, is part of the definition. Without it one speaks of a non-unital subring.

Examples

In the chain $\mathbb{Z} \subset \mathbb{Q} \subset \mathbb{R} \subset \mathbb{C}$ of integers, rationals, real numbers and complex numbers, each ring is a subring of the next.
The Gaussian integers $\mathbb{Z}[i] = \{a + bi : a, b \in \mathbb{Z}\}$ form a subring of $\mathbb{C}$, since $i^2 = -1$ keeps products of this form.
In the polynomial ring $R[x]$ the constant polynomials form a subring, a copy of $R$.
In the ring of $n \times n$ matrices over a field, the upper triangular matrices form a subring, and so do the scalar matrices.
Every ring has a smallest subring: it consists of the integer multiples $n \cdot 1$ for $n \in \mathbb{Z}$, the image of the unique ring homomorphism $\mathbb{Z} \to R$.
Non-examples. The even integers $2\mathbb{Z}$ are closed under addition, negation and multiplication but do not contain $1$, so they are not a subring of $\mathbb{Z}$. In $\mathbb{Z} \times \mathbb{Z}$ the set $\mathbb{Z} \times \{0\}$ is a ring with identity $(1, 0)$, but it does not contain the identity $(1, 1)$ of the larger ring, so it is not a subring either.

Properties

Intersections. The intersection of any family of subrings of $R$ is a subring. Unions usually are not: the union of $\mathbb{Z}[i]$ and $\mathbb{Z}[\sqrt 2]$ in $\mathbb{C}$ contains $i$ and $\sqrt 2$ but not $i + \sqrt 2$. The union of a nonempty family that is directed under inclusion, such as an increasing chain, is a subring.
Generated subrings. For a subset $X \subseteq R$, the subring generated by $X$ is the intersection of all subrings containing $X$. It contains $X$, and it lies inside a subring $T$ exactly when $X \subseteq T$, so it is the smallest subring containing $X$. Concretely, it is the additive subgroup generated by the set of finite products of elements of $X$, including the empty product $1$. For instance $\mathbb{Z}[i]$ is the subring of $\mathbb{C}$ generated by $i$.
Homomorphisms. For a ring homomorphism $f : R \to R'$, the image of a subring of $R$ is a subring of $R'$ and the preimage of a subring of $R'$ is a subring of $R$. In particular the range of $f$ is a subring of $R'$. Given two homomorphisms $f, g : R \to R'$, the set where they agree is a subring of $R$.
The center. The center of $R$, the set of elements commuting with every element, is a subring; an element $z$ lies in it exactly when $gz = zg$ for all $g \in R$. The center of a division ring is a field.
Subrings and ideals. An ideal is closed under addition, negation and multiplication, but an ideal is the whole ring exactly when it contains $1$, so the only ideal that is a subring is $R$ itself.
Integral domains. A subring of an integral domain has no zero divisors, so it is again an integral domain; every subring of a field is an integral domain.

A subfield of a field is a subring that is also closed under taking inverses of nonzero elements. A subring of an associative algebra over a commutative ring $k$ that contains the image of $k$ is a subalgebra. Weakening the requirement on $1$ gives non-unital subrings, and dropping negation gives subsemirings, the analogous notion for semirings.

In Mathlib

Mathlib treats a subring as a bundled structure: a subset of the ring together with proofs that it is a subsemiring (it contains $0$ and $1$ and is closed under addition and multiplication) and an additive subgroup. The definition is stated for rings that need not be associative. A subring inherits a non-associative ring structure in general, and a ring structure when the ambient ring is associative. Subrings of a fixed ring are ordered by inclusion and form a complete lattice: the meet is the intersection, the least subring is the image of $\mathbb{Z}$, and the join of two subrings is the subring generated by their union; more generally, the subring generated by $X \cup Y$ is the join of the subrings generated by $X$ and by $Y$. A subring always shares the identity of the ambient ring; the version without that requirement is the separate non-unital subring structure, and a subsemiring that contains $-1$ can be turned into a subring.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibSubring

Uses 3 · Used by 3

Statement usesRing · Set · Subgroup

Used bySubfield · $p$-adic integer · Von Staudt–Clausen theorem

AbbreviationLocalization #

Localization is the construction that adjoins inverses to a chosen set of elements of a commutative ring. Given a multiplicatively closed subset $S$ of a ring $R$, it produces a ring $S^{-1}R$ of fractions $r/s$ with $r \in R$ and $s \in S$, in which every element of $S$ becomes invertible, and it does so in the most economical way. The passage from the integers to the rational numbers is the model case. Localization is one of the basic tools of commutative algebra and algebraic geometry: it lets one study a ring "near" a prime ideal by passing to a local ring, and many properties of rings and modules can be checked one prime at a time.

Definition

Let $R$ be a commutative ring and $S \subseteq R$ a submonoid of its multiplicative monoid: $1 \in S$, and $st \in S$ whenever $s, t \in S$. On pairs $(a, s)$ with $a \in R$ and $s \in S$, declare $(a, s)$ and $(b, t)$ equivalent when there is some $u \in S$ with

\[u\,t\,a = u\,s\,b.\]

The class of $(a, s)$ is written $a/s$, and the set of classes is the localization of $R$ at $S$, written $S^{-1}R$. In terms of the relation Mathlib uses, two fractions are equal exactly when their pairs are related, and the pairs $(a, s)$ and $(b, t)$ are related exactly when $u\,t\,a = u\,s\,b$ for some $u \in S$. The factor $u$ is needed for the relation to be transitive when $R$ has zero divisors. If $R$ is an integral domain and $0 \notin S$, it can be cancelled, and the condition becomes the familiar cross-multiplication rule $ta = sb$.

The operations are those of ordinary fractions: $\frac{a}{s} \cdot \frac{b}{t} = \frac{ab}{st}$ and $\frac{a}{s} + \frac{b}{t} = \frac{sb + ta}{st}$. These make $S^{-1}R$ a commutative ring, and $r \mapsto r/1$ is a ring homomorphism from $R$ to $S^{-1}R$ under which the image of every element of $S$ is a unit.

Universal property

The localization is characterized by a universal property. Let $g$ be a ring homomorphism from $R$ to a commutative ring $T$ that sends every element of $S$ to a unit. Then $g$ factors through $S^{-1}R$: there is a ring homomorphism $h$ from $S^{-1}R$ to $T$ with $h(r/1) = g(r)$ for every $r \in R$, namely $h(a/s) = g(a)\,g(s)^{-1}$, and any ring homomorphism from $S^{-1}R$ to $T$ with this property equals $h$.

Equivalently, a commutative $R$-algebra $A$ with structure map $f$ is a localization of $R$ at $S$ exactly when three conditions hold: $f(s)$ is a unit for each $s \in S$; every element $z$ of $A$ satisfies $z\,f(s) = f(a)$ for some $a \in R$ and $s \in S$; and $f(x) = f(y)$ implies $ux = uy$ for some $u \in S$. Any two $R$-algebras with these properties are isomorphic as $R$-algebras, so one may speak of the localization.

Examples

Fractions. The rationals are the localization of the integers at the nonzero integers. More generally, localizing an integral domain at all of its nonzero elements gives its field of fractions, which is a field.
Localization at a prime. For a prime ideal $\mathfrak p$ of $R$, the complement $R \setminus \mathfrak p$ is multiplicatively closed, and the localization at it is written $R_{\mathfrak p}$. For a prime number $p$, the ring $\mathbb Z_{(p)}$ consists of the rationals whose denominator in lowest terms is prime to $p$.
Inverting one element. For $f \in R$, the localization at the powers of $f$ is written $R_f$ or $R[1/f]$. Inverting $2$ in $\mathbb Z$ gives the dyadic rationals, and inverting $x$ in the polynomial ring $k[x]$ over a field gives the Laurent polynomials $k[x, x^{-1}]$.
Degenerate cases. If $0 \in S$, the localization is the zero ring. Less drastically, inverting $2$ in $\mathbb Z/6\mathbb Z$ kills $3$, since $2 \cdot 3 = 0$, and the result is isomorphic to $\mathbb Z/3\mathbb Z$.

Properties

Kernel. For $r \in R$, $r/1 = 0$ exactly when $ur = 0$ for some $u \in S$. Hence the map $R \to S^{-1}R$ is injective exactly when every element of $S$ is cancellable, that is, a non-zero-divisor.
Integral domains. Localizing an integral domain at a submonoid of nonzero elements gives an integral domain.
Prime ideals. Taking preimages under $r \mapsto r/1$ gives an order-preserving bijection between the prime ideals of $S^{-1}R$ and the prime ideals of $R$ that do not meet $S$. For $S = R \setminus \mathfrak p$ the primes of $R$ disjoint from $S$ are those contained in $\mathfrak p$, so $R_{\mathfrak p}$ has a single maximal ideal: the localization at a prime ideal is a local ring.
Finiteness. A localization of a Noetherian ring is Noetherian (see Noetherian ring), since its ideals correspond to certain ideals of $R$ in an order-preserving, injective way.
Flatness. $S^{-1}R$ is a flat $R$-module: tensoring with it preserves injective linear maps. Since the localized module $S^{-1}M$ is isomorphic to $S^{-1}R \otimes_R M$, this is equivalent to the statement that localizing modules preserves exact sequences.

Where a quotient ring forces elements to become zero, a localization forces them to become invertible, and the two operations are often combined. The same fractions construction applied to a module $M$ over $R$ gives the localized module $S^{-1}M$. Applied to a commutative monoid it gives the monoid of fractions; localizing the additive monoid of natural numbers at all of its elements gives the additive group of integers, an instance of the Grothendieck group construction. For noncommutative rings, fractions can be formed at submonoids that satisfy the Ore condition together with a cancellation condition, the Ore sets. In algebraic geometry the rings $R_f$ are the rings of sections of the structure sheaf over the basic open subsets of the spectrum of $R$, which makes localization a basic ingredient in the definition of a scheme.

In Mathlib

Mathlib builds the localization in more generality than the ring version. The basic construction is the localization of a commutative monoid at a submonoid. Mathlib defines it as an instance of its more general Ore localization, a quotient of the set of pairs, and when the monoid is the multiplicative monoid of a commutative ring or semiring it carries the ring structure. Mathlib also defines a congruence on pairs, the smallest one that identifies $(1, 1)$ with $(s, s)$ for every $s \in S$, proves that two fractions are equal exactly when their pairs are related by it, and proves the explicit description with the factor $u$ as a lemma. Because reasoning up to isomorphism is awkward in a formal system, most results are stated not for this particular quotient but for any algebra that satisfies a characteristic predicate expressing the three conditions above; the quotient construction, the localization at a prime, the localization away from an element and the fraction ring are all instances. The fraction ring is defined for every commutative ring as the localization at its non-zero-divisors, and is a field when the ring is an integral domain.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibLocalization

Uses 2 · Used by 5

Statement usesRing · Ring morphism

Used byNullstellensatz · Structure theorem · Going-up and going-down theorems · Krull's principal ideal theorem · Rational fraction fields with one indeterminate over a field

ClassLocal ring #

A local ring is a commutative ring with exactly one maximal ideal. Equivalently, it is a nonzero ring in which the elements that are not units are closed under addition. Local rings are the algebraic counterpart of looking at a geometric object near a single point: the ring of germs of functions at a point (functions defined near it, identified when they agree near it), with the germs vanishing at the point as the maximal ideal, is the model case. Through localization many questions about arbitrary commutative rings reduce to questions about local rings, which is why they are central in commutative algebra and algebraic geometry.

Definition

Let $R$ be a commutative ring with $1 \neq 0$. The following conditions are equivalent, and $R$ is called local when they hold.

$R$ has a unique maximal ideal.
The nonunits of $R$ form an ideal.
Whenever $a + b = 1$ in $R$, at least one of $a$ and $b$ is a unit.

When $R$ is local, its maximal ideal is usually written $\mathfrak m$ (or $\mathfrak m_R$), and the quotient ring $k = R/\mathfrak m$ is a field, called the residue field. One often speaks of the local ring $(R, \mathfrak m)$ or $(R, \mathfrak m, k)$.

The equivalence is short. If the nonunits form an ideal, that ideal is proper and contains every proper ideal, so it is the only maximal ideal. If $\mathfrak m$ is the only maximal ideal, every nonunit generates a proper ideal, which, like every proper ideal, lies in some maximal ideal, and hence lies in $\mathfrak m$; so $\mathfrak m$ is exactly the set of nonunits. Condition 2 implies condition 3, because an ideal containing two elements with sum $1$ is the whole ring. Conversely, under condition 3 a multiple of a nonunit is a nonunit, and if nonunits $a$ and $b$ had a unit sum $u$, then $u^{-1}a + u^{-1}b = 1$ would be a sum of two nonunits; so the nonunits form an ideal.

Examples

Fields. A field is local, with maximal ideal $0$. Conversely, a commutative local ring is a field exactly when its maximal ideal is zero.
Residues modulo a prime power. For a prime $p$ and $n \ge 1$, the ring $\mathbb Z/p^n\mathbb Z$ is local: a residue is a unit precisely when it is prime to $p$, so the nonunits are the multiples of $p$, which form an ideal.
Localization at a prime. For a prime ideal $\mathfrak p$ of a commutative ring $R$, the localization $R_{\mathfrak p}$ is a local ring, and its maximal ideal is $\mathfrak p R_{\mathfrak p}$, the ideal generated by the image of $\mathfrak p$. For instance, for a prime number $p$, the localization $\mathbb Z_{(p)}$ consists of the rationals $a/b$ with $p \nmid b$; it is local, and its maximal ideal consists of those with $p \mid a$.
Power series. Over a field $k$, a power series is invertible exactly when its constant term is nonzero, so $k[[X]]$ is local and its maximal ideal is generated by $X$.
$p$-adic integers. For a prime $p$ the ring $\mathbb Z_p$ of $p$-adic integers is local, and its maximal ideal is generated by $p$.

Many familiar rings are not local. The integers have the distinct maximal ideals $(2)$ and $(3)$, and for a field $k$, in the polynomial ring $k[X]$ the nonunits $X$ and $1 - X$ add up to $1$. More generally, a product of two nonzero rings is never local, since $(1, 0) + (0, 1) = (1, 1)$ is a sum of two nonunits.

Properties

Let $(R, \mathfrak m)$ be a commutative local ring.

Characterizations. A nonzero ring is local as soon as its nonunits are closed under addition, and conversely in a local ring a sum of two nonunits is a nonunit. In a local ring, for every $a$ either $a$ or $1 - a$ is a unit. A local ring has exactly one maximal ideal, and a commutative ring with exactly one maximal ideal is local.
The maximal ideal. An element lies outside $\mathfrak m$ if and only if it is a unit, and every proper ideal is contained in $\mathfrak m$. In particular the Jacobson radical of $R$, the intersection of all its maximal ideals, equals $\mathfrak m$.
Residue field. The residue field is the quotient $R/\mathfrak m$, and it is a field because $\mathfrak m$ is maximal.
Quotients. The image of a local ring under a surjective ring homomorphism onto a nonzero ring is local; in particular $R/I$ is local for every proper ideal $I$.
Local homomorphisms. A ring homomorphism $f \colon R \to S$ is called local if every element whose image is a unit is itself a unit. For local rings $(R, \mathfrak m)$ and $(S, \mathfrak n)$, $f$ is local if and only if $f(\mathfrak m) \subseteq \mathfrak n$, and if and only if $f^{-1}(\mathfrak n) = \mathfrak m$. A locally ringed space is a ringed space whose stalks are local rings, and its morphisms are required to induce local homomorphisms on stalks.
Nakayama's lemma. For a finitely generated module $M$ over $R$, a submodule $N$ equals $M$ if and only if its image in $M/\mathfrak m M$ is all of $M/\mathfrak m M$. Consequently, elements of $M$ generate $M$ exactly when their images span the vector space $M/\mathfrak m M$ over the residue field.
Flat modules. A module is free when it has a basis, and flat when tensoring with it preserves injective maps. Every finitely generated flat module over a local ring is free. Projective modules (direct summands of free modules) are flat, so the same holds for finitely generated projective modules.

Important special classes of local rings include discrete valuation rings (local principal ideal domains that are not fields), such as $k[[X]]$ and $\mathbb Z_p$, and Noetherian local rings, which are local rings that are also Noetherian and carry a well-behaved dimension theory. A semilocal ring is one with finitely many maximal ideals. In algebraic geometry, the stalk of the structure sheaf of a scheme at a point is a local ring, and the residue field at the point is its residue field.

In Mathlib

Mathlib defines being local as a property of a semiring that need not be commutative: a semiring is local when it is nontrivial (that is, $0 \neq 1$) and, whenever $a + b = 1$, $a$ or $b$ is a unit. This is condition 3 above, a form that does not mention ideals and so needs neither commutativity nor a choice between left, right and two-sided ideals. For noncommutative rings it is stronger than having a unique maximal two-sided ideal: the ring of $2 \times 2$ matrices over a field has $0$ as its only maximal two-sided ideal, but it is not local. The maximal ideal is defined, for commutative semirings, as the set of nonunits, and the equivalence with having a unique maximal ideal is proved as a theorem in that setting. The residue field is defined for commutative rings. Local homomorphisms are defined more generally, for maps between arbitrary monoids, by the same condition that only units map to units.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibIsLocalRing

Uses 3 · Used by 14

Statement usesRing · Ideal of a commutative ring · Maximal ideal

Used byThe Solution of a Cubic · The Solution of the General Quartic Equation · Finite-dimensional normed spaces over complete normed fields are complete · Heine-Borel theorem (finite-dimensional normed spaces are proper) · Locally ringed space · Nullstellensatz · Diagonalization of self-adjoint endomorphisms · Primitive element theorem · Going-up and going-down theorems · Krull's principal ideal theorem · Schur's lemma (1000+ theorems) · Weierstrass preparation theorem · Ax–Grothendieck theorem · Ostrowski's theorem

AbbreviationNoetherian ring #

A Noetherian ring is a ring in which every ideal is finitely generated; equivalently, every increasing chain of ideals eventually stops growing. The condition is a finiteness hypothesis that covers most rings met in number theory and algebraic geometry, including the integers, fields, and polynomial rings in finitely many variables over them. It is preserved by the usual constructions of commutative algebra, and it is the standing assumption under which much of the subject's structure theory holds: primary decomposition, finiteness of minimal primes, and the dimension theory of rings.

Definition

Let $R$ be a commutative ring. The following conditions on $R$ are equivalent.

Every ideal $I$ of $R$ is finitely generated: there are $a_1, \dots, a_n \in I$ with $I = (a_1, \dots, a_n)$.
(Ascending chain condition.) For every chain of ideals $I_1 \subseteq I_2 \subseteq I_3 \subseteq \cdots$ there is an $N$ with $I_n = I_N$ for all $n \ge N$.
(Maximal condition.) Every nonempty set of ideals of $R$ has a maximal element with respect to inclusion.

The ring $R$ is Noetherian if it satisfies them. In Mathlib's terms, $R$ is Noetherian when it is a Noetherian module over itself, and this holds if and only if every ideal of $R$ is finitely generated. Mathlib proves the other two characterizations for an arbitrary module: a module is Noetherian if and only if every increasing chain of submodules stabilizes, and if and only if every nonempty set of submodules has a maximal member. Taking the module to be $R$ itself, whose submodules are its ideals, gives conditions 2 and 3.

To see that condition 1 gives condition 2, note that the union $I$ of a chain of ideals is again an ideal. Its finitely many generators all lie in some $I_N$, so $I = I_N$ and the chain is constant from $N$ on. Conversely, if an ideal $I$ were not finitely generated, one could choose $a_1, a_2, \dots \in I$ with each $a_{n+1}$ outside $(a_1, \dots, a_n)$, producing a chain that never stops. Condition 3 gives condition 2 by applying it to the set of ideals $\{I_n\}$ in a chain: a maximal member $I_N$ forces $I_n = I_N$ for $n \ge N$. Conversely, a nonempty set of ideals with no maximal member contains a strictly increasing infinite chain, so condition 2 gives condition 3.

Examples

A field has only two ideals, $0$ and the whole field, so it is Noetherian.
In a principal ideal domain every ideal is generated by one element, and indeed every principal ideal ring is Noetherian. This covers the integers and the polynomial ring $k[x]$ over a field $k$.
Every finite ring, such as $\mathbb{Z}/n\mathbb{Z}$ for $n \ge 1$, is Noetherian, as is more generally every module with finitely many elements.
Hilbert basis theorem. If $R$ is a commutative Noetherian ring, then the polynomial ring $R[x]$ is Noetherian. By induction, polynomial rings in finitely many variables over $R$ are Noetherian (see polynomial in several indeterminates). A variant of the argument shows that the ring $R[[x]]$ of formal power series is Noetherian, and by the same induction so is the ring of formal power series in finitely many variables over $R$ (see power series).
If $R$ is a commutative Noetherian ring and $I$ an ideal, then the quotient ring $R/I$ is Noetherian (see quotient ring), and every localization of $R$ is Noetherian (see localization). Since a finitely generated commutative $R$-algebra is a quotient of a polynomial ring in finitely many variables over $R$, every finitely generated commutative algebra over a commutative Noetherian ring is Noetherian.

The polynomial ring $k[x_1, x_2, x_3, \dots]$ in infinitely many variables is not Noetherian, since $(x_1) \subsetneq (x_1, x_2) \subsetneq (x_1, x_2, x_3) \subsetneq \cdots$ never stops. Because this ring is a subring of its field of fractions, which is Noetherian, the property does not pass to subrings.

Properties

Let $R$ be a commutative Noetherian ring.

Modules. Every finitely generated $R$-module is a Noetherian module: all of its submodules are finitely generated. In a Noetherian module, a surjective linear map from the module to itself is injective.
Factorization. If $R$ is an integral domain, strict divisibility in $R$ admits no infinite descending chains, and therefore every nonzero element is, up to a unit, a product of irreducible elements (see irreducible element). The factorization need not be unique: $\mathbb{Z}[\sqrt{-5}]$ is Noetherian but not a unique factorization domain, since $6 = 2 \cdot 3 = (1 + \sqrt{-5})(1 - \sqrt{-5})$.
Primary decomposition. By the Lasker–Noether theorem, every ideal of $R$, and more generally every submodule of a Noetherian module over a commutative ring, is a finite intersection of primary ones, the whole ring or module counting as the empty intersection.
Minimal primes and nilradical. $R$ has only finitely many minimal prime ideals (see prime ideal), and its nilradical, the ideal of nilpotent elements, is nilpotent: some power of it is the zero ideal.
Krull's intersection theorem. For a proper ideal $I$ of $R$, $$\bigcap_{n \ge 1} I^n = 0$$ holds when $R$ is an integral domain and when $R$ is a local ring (see local ring).
Dimension. By Krull's principal ideal theorem, a prime ideal of $R$ that is minimal among primes containing a principal ideal has height at most $1$. A commutative ring is Artinian, meaning that descending chains of ideals stop, if and only if it is Noetherian and every prime ideal is maximal (see maximal ideal).

Generalizations

The definition makes sense for a noncommutative ring, where the left and right versions differ: a ring is left Noetherian if its left ideals satisfy the ascending chain condition, and right Noetherian if its right ideals do. The module-theoretic version, a Noetherian module, is the condition that every submodule is finitely generated, and a ring is Noetherian exactly when it is a Noetherian module over itself. The dual condition on descending chains defines Artinian rings and modules.

In Mathlib

Mathlib defines the notion for any semiring, not only commutative rings, and makes it an abbreviation: a semiring is Noetherian when it is a Noetherian module over itself, a module being Noetherian when every submodule is finitely generated. Since Mathlib's ideals of a noncommutative ring are its left ideals, for such rings the definition means left Noetherian. The chain conditions are expressed through well-foundedness of strict inclusion, read in reverse, on the lattice of submodules. Being Noetherian is a class, so the property of polynomial rings in finitely many variables, quotients, the standard localization at a submonoid, and principal ideal rings is supplied automatically wherever it is needed. The Hilbert basis theorem and most of the structure theory are stated for commutative rings.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibIsNoetherianRing

Uses 3 · Used by 7

Statement usesRing · Ideal of a commutative ring · Generating sets

Used byHilbert basis theorem · Structure theorem · Krull's principal ideal theorem · Lie's theorem · Ax–Grothendieck theorem · Whitney embedding theorem · Schur's lemma (Linear representations)

ClassOrdered ring #

An ordered ring is a ring equipped with an order that is compatible with its addition and multiplication: adding the same element to both sides of an inequality preserves it, and so does multiplying both sides by a nonnegative element. The integers, the rational numbers and the real numbers are the basic examples. The notion isolates the algebraic rules used whenever one manipulates inequalities, so that facts such as "a product of two nonpositive elements is nonnegative" can be proved once for every ring that obeys those rules, and facts such as "squares are nonnegative" or Bernoulli's inequality once for every linearly ordered ring.

Definition

Let $R$ be a ring (associative, with identity, not necessarily commutative) and let $\le$ be a partial order on $R$. Then $R$ is an ordered ring if, for all $a, b, c \in R$:

if $a \le b$, then $a + c \le b + c$;
$0 \le 1$;
if $a \le b$ and $0 \le c$, then $ca \le cb$ and $ac \le bc$.

Condition 3 with $a = 0$ says that the nonnegative elements are closed under multiplication. Given conditions 1 and 2, this closure is also sufficient: if $0 \le c$ and $a \le b$, then $0 \le b - a$ by condition 1, so $cb - ca = c(b - a)$ and $bc - ac = (b - a)c$ are products of nonnegative elements, hence nonnegative, and adding $ca$ (respectively $ac$) to both sides by condition 1 gives $ca \le cb$ and $ac \le bc$. So it is enough to check that $0 \le x$ and $0 \le y$ imply $0 \le xy$.

The ring is linearly ordered when any two elements are comparable. In that case condition 2 follows from the others: if $1 < 0$, then $0 < -1$ by condition 1, and condition 3 with $c = -1$ gives $0 \le (-1)(-1) = 1$, a contradiction. For a merely partial order it is a genuine requirement: the order in which $a \le b$ only when $a = b$ satisfies conditions 1 and 3 on every ring.

A strictly ordered ring is a nontrivial ring with a partial order satisfying conditions 1 and 2 in which multiplication on either side by a positive element is strictly increasing: $a < b$ and $0 < c$ imply $ca < cb$ and $ac < bc$. Every strictly ordered ring is an ordered ring. Conventions in the literature vary: many texts reserve "ordered ring" for the linearly ordered case, and some build strictness into the definition.

Examples

With their usual orders, the integers, the rational numbers and the real numbers are strictly ordered rings, and their usual orders are linear (see order on the real numbers). The natural numbers form only a semiring, but they satisfy the axioms of a strictly ordered ring, which Mathlib states for semirings.
A subring of an ordered ring, with the restricted order, is again an ordered ring.
The polynomial ring $\mathbb{Z}[x]$, with a nonzero polynomial declared positive when its leading coefficient is positive, is linearly and strictly ordered. Here $x - n$ is positive for every integer $n$, so $x$ is larger than every integer.
A product of ordered rings, ordered coordinatewise, is an ordered ring. In $\mathbb{R}^2$ the elements $(1, 0)$ and $(0, 1)$ are incomparable, so the order is not linear; both are positive but their product is $0$, so the ring is not strictly ordered.
In $\mathbb{Z}[\varepsilon]$ with $\varepsilon^2 = 0$, order $a + b\varepsilon$ by the sign of $a$, and by the sign of $b$ when $a = 0$. This is a linearly ordered ring that is not strictly ordered, since $\varepsilon > 0$ but $\varepsilon^2 = 0$.
On the complex numbers, declare $z \le w$ when $w - z$ is a nonnegative real number. With this partial order the complex numbers form a strictly ordered ring. No total order does this, because squares would be nonnegative, giving both $0 \le 1$ and $0 \le i^2 = -1$, and adding $1$ to the second inequality forces $1 \le 0$, so $1 = 0$.

Properties

Let $R$ be an ordered ring.

The product of two nonnegative elements is nonnegative, and the product of two nonpositive elements is nonnegative.
The nonnegative elements form a subsemiring $P$ with $P \cap (-P) = \{0\}$. Conversely, if $P$ is a subsemiring of a ring with $P \cap (-P) = \{0\}$, declaring $a \le b$ when $b - a \in P$ makes the ring an ordered ring. The order is linear exactly when $P \cup (-P)$ is the whole ring.
If $R$ is nontrivial, then $0 < 1$, so the multiples $n \cdot 1$ strictly increase with $n$ and $R$ has characteristic zero (see characteristic zero). In particular no nonzero ring of positive characteristic, such as a finite field, carries an ordered ring structure.
If $R$ is linearly ordered, then every square is nonnegative, and the absolute value is multiplicative, $|ab| = |a|\,|b|$.
If $R$ is linearly and strictly ordered, then $R$ is a domain, that is, nontrivial with no zero divisors. In the other direction, for any partial order, a nontrivial ordered ring without zero divisors is strictly ordered.
If $R$ is strictly ordered, the product of two negative elements is positive.
Bernoulli's inequality. If $R$ is linearly ordered, $2 + a \ge 0$ (that is, $a \ge -2$) and $n$ is a natural number, then $(1 + a)^n \ge 1 + na$.

An ordered field is an ordered ring that is a field; the rationals and the reals are the standard examples. The polynomial example above shows that an ordered ring need not be Archimedean, meaning that for every element $a$ and every positive $b$ some multiple $nb$ with $n$ a natural number satisfies $a \le nb$: taking $b = 1$, the indeterminate $x$ of $\mathbb{Z}[x]$ exceeds every integer. The additive group of an ordered ring, with the same order, is an ordered abelian group: an abelian group with a partial order satisfying condition 1.

In Mathlib

Mathlib separates the three ingredients: the algebraic structure, the order, and a property that records how they interact. The ordered ring property is stated for semirings, so it covers the natural numbers as well as rings, and it requires monotonicity of multiplication on both sides because commutativity is not assumed. The axiom $0 \le 1$ is part of the definition; one consequence is that reversing the order of an ordered ring does not in general give an ordered ring. Linearly ordered rings are obtained by combining the property with a linear order, and strictly ordered rings form a separate, stronger property. Many lemmas about linearly ordered rings additionally assume the strict property. Many lemmas, including the statements about squares, domains, nonpositive products, negative products and Bernoulli's inequality above, are proved for semirings in which $a \le b$ implies $b = a + c$ for some $c$; every ring meets this condition with $c = b - a$. The order on the complex numbers described above is not imposed by default and is available only when explicitly requested; Mathlib states the strictly ordered ring result for both the real and the complex numbers at once.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibIsOrderedRing

Uses 1 · Used by 72

Statement usesRing

Used byFormula for Pythagorean Triples · Liouville’s Theorem and the Construction of Transcendental Numbers · Sum of the Angles of a Triangle · The Irrationality of the Square Root of 2 · Arithmetic Mean/Geometric Mean · Divergence of the Harmonic Series · Heron’s Formula · Product of Segments of Chords · Sum of the Reciprocals of the Triangular Numbers · The Ballot Problem · L’Hopital’s Rule · Sum of a Geometric Series · Sum of kth powers · The Perfect Number Theorem · Bertrand’s Postulate · Descartes Rule of Signs · The Birthday Problem · The Friendship Theorem · Carathéodory's theorem · Local extrema · Fatou's lemma · Heine-Borel theorem (finite-dimensional normed spaces are proper) · Behrend's construction · Cauchy-Davenport theorem · Small tripling implies small powers · Regularity lemma · Triangle counting lemma · Four functions theorem · Harris-Kleitman inequality · LYM inequality · Hyper-real number · Pointed cone · Jacobi/Leibniz identity · Sphere · Uniform time existence · Closed interval · Urysohn's lemma · Uniformly continuous function · Schwartz–Zippel theorem · Birkhoff–Von Neumann theorem · Gershgorin circle theorem · Bolzano–Weierstrass theorem (1000+ theorems) · Darboux's theorem (analysis) · Vitali convergence theorem · Cauchy–Hadamard theorem · Poincaré recurrence theorem · Hellinger–Toeplitz theorem · Akra–Bazzi theorem · Hahn embedding theorem · Apollonius's theorem · Intersecting secants theorem · Tangent-secant theorem · Thales's theorem · Krein–Milman theorem · Radon's theorem · Beatty's theorem · Glaisher's theorem · Niven's theorem · Ostrowski's theorem · Poisson limit theorem · Sylvester's law of inertia (uniqueness) · Approximation by step functions · Grönwall lemma · Continuity (Complex-valued series) · Holomorphic stability under uniform convergence · Convergence of $p$-series for $p>1$ · Weierstrass polynomial approximation theorem · Taylor's theorem with Lagrange form for remainder · Completeness of R · Completeness of $l^2$ · Limits of sequences · Topology of a metric space

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Rings

ClassRing#

Definition

Examples

Basic properties

Related concepts

In Mathlib

Sources

StructureRing morphism#

Definition

Examples

Properties

Related concepts

In Mathlib

Sources

StructureThe category of rings#

Definition

Examples

Properties

Related concepts

In Mathlib

Sources

StructureSubring#

Definition

Examples

Properties

Related concepts

In Mathlib

Sources

AbbreviationLocalization#

Definition

Universal property

Examples

Properties

Related concepts

In Mathlib

Sources

ClassLocal ring#

Definition

Examples

Properties

Related concepts

In Mathlib

Sources

AbbreviationNoetherian ring#

Definition

Examples

Properties

Generalizations

In Mathlib

Sources

ClassOrdered ring#

Definition

Examples

Properties

Related concepts

In Mathlib

Sources

ClassRing #

StructureRing morphism #

StructureThe category of rings #

StructureSubring #

AbbreviationLocalization #

ClassLocal ring #

AbbreviationNoetherian ring #

ClassOrdered ring #