symmetric monoidal (∞,1)-category of spectra
A local ring is a ring (with unit, usually also assumed commutative) such that:
$0 \ne 1$; and
whenever $a + b = 1$, $a$ or $b$ is invertible.
Here are a few equivalent ways to phrase the combined condition:
Whenever a (finite) sum equals $1$, at least one of the summands is invertible.
Whenever a sum is invertible, at least one of the summands is invertible.
Whenever a sum of products is invertible, for at least one of the summands, all of its multiplicands are invertible.
The non-invertible elements form an ideal. (Unlike the previous clauses, this requires excluded middle to be equivalent.)
The ideal of non-invertible elements is in fact a maximal ideal, so the quotient ring is a field. (This quotient can also be taken constructively, where one mods out by an anti-ideal.)
(Kaplansky) A projective module over a commutative local ring is free.
An exposition of the proof may be found here. A constructive proof of a finitary weakening of Kaplansky’s theorem proceeds as follows.
Let $A$ be a local ring. Let $\mathfrak{a}$ be a finitely generated idempotent ideal in $A$. Then $\mathfrak{a} = (0)$ or $\mathfrak{a} = (1)$.
Consider $\mathfrak{a}$ as a finitely generated $A$-module. Then, by Nakayama's lemma, there exists an element $x \in A$ such that $x \equiv 1$ modulo $\mathfrak{a}$ and $x \mathfrak{a} = 0$. Since $A$ is a local ring, $x$ is invertible or $1-x$ is invertible. In the first case it follows that $\mathfrak{a} = (0)$, in the second that $\mathfrak{a} = (1)$.
Let $A$ be a local ring. Let $P$ be an idempotent matrix over $A$. Then $P$ is equivalent to a diagonal matrix with entries $1$ and $0$.
Since $P$ is idempotent, so are its ideals $(\Lambda^i P)$ of $i$-minors:
By the previous lemma, they are therefore each equal to $(0)$ or $(1)$. Since they form a descending chain, there exists a stage $r$ such that $(\Lambda^r P) = (1)$ and $(\Lambda^{r+1} P) = (0)$. Therefore all $(r+1)$-minors of $P$ are zero, and – since $A$ is a local ring – there exists at least one invertible $r$-minor. Thus $P$ can be made into a diagonal matrix of the desired form by applying row and column transformations.
We can even show that $P$ is similar to a diagonal matrix with entries $1$ and $0$: By the lemma, image and kernel of $P$ are finite free. Combining bases of these subspaces, we obtain a basis of the full space; expressing $P$ with respect to this basis, we obtain a diagonal matrix of the desired form.
Let $M$ be a finitely generated module over a local ring $A$. Assume that $M$ is projective. Then $M$ is finite free.
Fix a linear surjection $p : A^n \to M$ and a section $s : M \to A^n$. The composition $P \coloneqq s \circ p$ is idempotent and $M$ is isomorphic to $A^n/\operatorname{ker}(P)$. Since $P$ is equivalent to a diagonal matrix with entries $1$ and $0$, this module is obviously finite free.
In algebraic geometry or synthetic differential geometry and commutative algebra, the most commonly used definition of a local commutative ring is a commutative ring $R$ with a unique maximal ideal. Hence the Spec of such an $R$ has a unique closed point. Intuitively it can be thought of as some kind of “infinitesimal neighborhood” of a closed point.
The spectrum of a ring $R$ is local, i.e. in any covering of $Spec R$ by open subsets one of the subsets is already the whole of $Spec R$, if and only if $R$ is a local ring. This provides some justification for the name.
The topos theory formulation of this is a local topos.
An important example of a local ring in algebraic geometry is $R = k[\epsilon]/\epsilon^2$. This ring is known as the ring of dual numbers. Intuitively, we can think of its spectrum as consisting of a closed point and a tangent vector. Indeed this is justified, as morphisms from $\operatorname{Spec} R$ to a scheme $X$ correspond exactly to pairs $(x,v)$, where $x \in X$ and $v$ is a (Zariski) tangent vector at $x$.
Local rings are also important in deformation theory. One might define an infinitesimal deformation of a scheme $X_0$ to be a deformation of $X_0$ over $\operatorname{Spec} R$ where $R$ is a local ring.
Local rings are often more useful than fields when doing mathematics internally. For one thing, the definition make sense in any coherent category. But unlike the definition of discrete field, which is also coherent, it is satisfied by rings such as the ring of (located Dedekind) real numbers. Rather than mod out by the ideal of non-invertible elements, you take care to use only properties that are invariant under multiplication by an invertible element.
In constructive mathematics, one could do the same thing, but it's more common to use the notion of Heyting field. This is closely related, however; the quotients of local rings are precisely the Heyting fields (which are themselves local rings). In fact, one can define an apartness relation (like that on a Heyting field) in any local ring: $x \# y$ iff $x - y$ is invertible. Then the local ring is a Heyting field if and only if this apartness relation is tight.