Identifying Mathematical Objects up to Canonical Isomorphpism
Motivation
Mathematics pervasively identifies objects if they are canonically isomorphic.
Examples:
- define the rationals as fractions (pairs of integers, quotiented by cancelling), then identify the integer z with the fraction z/1
- the entire number hierarchy N <: Z <: Q etc. is built like above
- elements of ring R are identified with constant polynomials over R
- elements of ring R are identified with elements in localizations over R
- polynomials are identified with the respective elements in the field of fractions
- generators of a group are identified with elements of the generated group (which are technically equivalence classes)
It is very common that
- the isomorphism is from a smaller to a subset of a bigger structure
- the bigger structure is built from the smaller one (i.e., we cannot simply define the smaller one as a subset of the bigger one because we need it to build the bigger one)
- the embedding of the smaller into the bigger structure preserves some operations (e.g., the embedding N -> Z is a semiring morphism, the embedding of R into R[X] is a ring moprhism) and can therefore not simply be represented as just a function
- the set preserved properties is extended later on as additional properties are considered (e.g., the embedding N -> Z is also an order morphism)
Virtually all tools for formalized mathematics cannot handle this at all, let alone elegantly. It requires fundamentally different formal systems that we have not designed yet.
Idea
For a certain special case, theory morphisms may be a solution:
- We can define the structures as theories and the embedding as a theory morphism, e.g.,
- N={n: type, z: n, s: n->n}
- Z={i: type, z:i, s:i->i, p:i->i, s(p(x)=x, p(s(x)=x, leq:i->i->prop}
- emb: N->Z = {n={x:i|z leq x}, z=z, s=s}
In particular, the theory morphism would capture which operations are preserved.
In this topic, you build a case study formalizing canonical isomorphisms in this way. You will identify and possibly solve any theoretical or practical problems that come up along the way.
Technical Problems
Weak Embeddings
Often the embedding function is not a theory morphism because it does not preserve all properties of a structure s. Such embeddings can only be expressed as theory morphism out of S if S is an inadequately weak formalization of s. Often the theory S amounts to specifying a category in which s is the initial object. More generally, we can think of s as the structure that is freely generated by the syntax of S.
An important special case are non-injective embeddings. For example, the embedding of the natural numbers into the theory of rings is not necessarily injective. This can only be expressed as a theory morphism if the natural numbers are formulated without the injectivity of successor.
Similarly, we may have to allow for non-surjective embeddings if we cannot capture the image of the embedding as a predicate subtype (e.g., when embedding natural numbers into real numbers, where the logic cannot express the needed predicate). In the case of natural numbers, this means the induction axiom should be optional as well.
Models as Theories
There are multiple ways to represent mathematical structures (here called models) in a formal system.
Concrete models of theory T are given as tuples of their universes and operations, e.g., (N,0,1+,*) for the semiring of natural numbers. (Technically, this tuple also includes proofs of all axioms.) Concrete models can be represented in two different way:
- internal models: models are represented as record values of a record type corresponding to T
- external models: models are represented as theory morphisms out of T
Abstract models of theory T are represented as theories. These theories contain undefined constants and axioms. Examples are the models for N and Z above. Typically, these theories M extend T or admit very simpl morphisms, usually injective renamings, T -> M.
The critical idea of this case study is to use abstract models. This is the only way that allow using theory morphisms for the embeddings.
It remains open how this relates to other, concrete, representations of models.