General algebraic systems

Start here

• ConceptUniversal algebra

  Universal algebra is the part of algebra that studies algebraic structures in general, rather than groups, rings or lattices one at a time. Its objects are sets with a family of finitary operations, described by a signature. It treats homomorphisms, subalgebras, congruences and products for all such structures at once. Its central results, such as Birkhoff's HSP theorem, describe the classes of algebras defined by identities.

• ConceptAlgebraic structure

  An algebraic structure, or algebra, is a set together with a family of finitary operations on it. The names and arities of the operations form a signature with no relation symbols, so an algebraic structure is a structure of a special kind. Groups, rings, fields, lattices and vector spaces are the main examples. A kind of algebraic structure is usually fixed by its signature and by a list of axioms, often identities, that the operations satisfy.

• ConceptSignature

  A signature lists the non-logical symbols of a first-order language: function symbols, relation symbols and constant symbols, each with its number of arguments. It fixes what one can talk about, before any axioms are chosen. Terms, formulas and structures are always taken over a given signature. Another name is vocabulary, and in Mathlib it is called a first-order language.

• ConceptSignature

  A signature lists the non-logical symbols of a first-order language: function symbols, relation symbols and constant symbols, each with its number of arguments. It fixes what one can talk about, before any axioms are chosen. Terms, formulas and structures are always taken over a given signature. Another name is vocabulary, and in Mathlib it is called a first-order language.

• ConceptArity

  The arity of an operation, a function or a relation is the number of arguments it takes. An operation of arity $n$ is called $n$-ary: nullary for $0$, unary for $1$, binary for $2$ and ternary for $3$. Arities are part of every signature, and they tell what kind of interpretation each symbol gets in a structure.

• ConceptFinitary operation

  A finitary operation on a set $A$ takes $n$ elements of $A$ and returns an element of $A$, for a fixed natural number $n$. The number $n$ is its arity. Binary operations such as addition are the most common case, but unary, nullary and ternary operations also occur. Algebraic structures are sets equipped with finitary operations.