Introduction

Mappings play a fundamental role in algebra and, indeed, throughout mathematics. Reflecting this importance, mappings are one of the fundamental datatypes in our language. The most general way to define a mapping f: A -> B in a programming language is to write a function which, given any element of A, will return its image under f in B. While this approach to the definition of mappings is completely general, it is desirable to have mappings as an independent datatype. It is then possible to provide a very compact notation for specifying important classes of mappings such as homomorphisms. Further, a range of operations peculiar to the mapping type can be provided.

Mappings are created either through use of mapping constructors as described in this Chapter, or through use of certain standard functions that return mappings as either primary or secondary values.

All mappings are objects in the Magma category Map.

Contents

The Map Constructors

There are three main mapping constructors: the general map constructor map< >, the homomorphism constructor hom< >, and the partial map constructor pmap< >. The general form of all constructors is the same: inside the angle brackets there are two components separated by a pipe |. To the left the user specifies a domain A and a codomain B, separated by ->; to the right of the pipe the user specifies how images are obtained for elements of the domain. The latter can be done in one of several ways: one specifies either the graph of the map, or a rule describing how images are to be formed, or for homomorphisms, one specifies generator images. We will describe each in the next subsections. The result is something like map< A -> B | expr >.

The domain and codomain of the map can be arbitrary magmas. When a full map (as opposed to a partial map) is constructed by use of a graph, the domain is necessarily finite.

The main difference between maps and partial maps is that a partial map need not be defined for every element of the domain. The main difference between these two types of map and homomorphisms is that the latter are supposed to provide structure-preserving maps between algebraic structures. On the one hand this makes it possible to allow the specification of images for homomorphisms in a different fashion: homomorphism can be given via images for generators of the domain. On the other hand homomorphisms are restricted to cases where domain and (image in the) codomain have a similar structure. The generator image form only makes sense for domains that are finitely presented. Homomorphisms are described in more detail below.

The Graph of a Map

Let A and B be structures. A subgraph of the cartesian product C = A x B is a subset G of C such that each element of A appears at most once among the first components of the pairs <a, b> of G. A subgraph having the additional property that every element of A appears as the first component of some pair <a, b> of G is called a graph of A x B.

A mapping between A and B can be identified with a graph G of A x B, a partial map can be identified with a subgraph. We now describe how a graph may be represented in the context of the map constructor. An element of the graph of A x B can be given either as a tuple <a, b>, or as an arrow pair a -> b. The specification of a (sub)graph in a map constructor should then consist of either a (comma separated) list, a sequence, or a set of such tuples or arrow pairs (a mixture is permitted).

Rules for Maps

The specification of a rule in the map constructor involves a free variable and an expression, usually involving the free variable, separated by :->, for example x :-> 3*x - 1. The scope of the free variable is restricted to the map constructor (so the use of x does not interfere with values of x outside the constructor). A general expression is allowed in the rule, which may involve intrinsic or user functions, and even in-line definitions of such functions.

Homomorphisms

Probably the most useful form of the map-constructor is the version for homomorphisms. Most interesting mappings in algebra are homomorphisms, and if an algebraic structure A belongs to a family of algebraic structures which form a variety we have the fundamental result that a homomorphism is uniquely determined by the images of any generating set. This provides us with a particularly compact way of defining and representing homomorphisms. While the syntax of the homomorphism constructor is similar to that of the general mapping constructor, the semantics are sometimes different.

The kind of homomorphism built by the hom-constructor is determined entirely by the domain: thus, a group homomorphism results from applying hom to a domain A that is one of the types of group in Magma, a ring homomorphism results when A is a ring, etc. As a consequence, the requirements on the specification of homomorphisms are dependent on the category to which A belongs. Often, the codomain of a homomorphism is required to belong to the same variety. But even within a category the specification may depend on the type of structure; for details we refer the reader to the specific chapters.

A homomorphism can be specified using either a rule map or by generator images. In the latter case the processor will seek to express an element as a word in the generators of A when asked to compute its image. Thus A needs to be finitely presented.

Checking of Maps

It should be pointed out that checking the `correctness' of mappings can be done to a limited extent only. If the mapping is given by means of a graph, Magma will check that no multiple images are specified, and that an image is given for every element of the domain (unless a partial map is defined). If a rule is given, it cannot be checked that it is defined on all of the domain. Also, it is in general the responsibility of the user to ensure that the images provided for a hom constructor do indeed define a homomorphism.

V2.28, 13 July 2023