General formalization tools

If we have intuitive ideas of a kind of systems that we want to study, but we do not know which language (list of structures) would be good to formalize them, then how can we still find a method to "anyway simply formalize it no matter what a subtle kind of system it is" ?

Simple examples of kinds of systems that look natural to formalize, are
More subtle, seemingly less obvious examples, for which naive attempts would be inelegant, are concepts of manifolds : kinds of "spaces" where we can distinguish curves, surfaces and other "subspaces" (sub-manifolds) with any dimension, where we may specify diverse degrees of regularity, but no measure of distance or straightness.
There is a range of such possible kinds of "spaces":
There is a standard formalization of topology that works rather well, but it does not look intuitive, is not directly useful for physics, and it does not appear as a particular case that can be directly modified to similarly formalize the diverse further classes of manifolds. Also, it allows for "too many possibilities" that are not physically meaningful.

But, as surprising as it may seem, there is a very general method, with such a wide range of uses, and still rather simple.

First step is to have an idea of which functions between spaces will be accepted as "morphisms" (that, depending on the kind of systems, will mean to qualify functions as : continuous, differentiable, etc), so that any composite of morphisms will be a morphism. For example, no matter how topology may be formalized, we expect the concept of "continuous function" between spaces to make sense, and that a composite of continuous functions will be continuous. We have a clear intuition what it means for a function to be continuous, so there should exist a definite set of all continuous functions from a space to another. But to write a definition for it, would depend on the choice of formalization of the topological structure that we want these functions to preserve. Never mind, we will define this later.

So in the first step, let us admit as primitive data, the sets of intended morphisms between systems. This way, the intended kind of "spaces" are seen as the objects of a concrete category C. In this case, is there any general, systematic way to interpret its objects as systems with a kind of "structures", so that what we called the morphisms of C will preserve these structures ? The problem is not only to find all first-order structures if any can be found, but also, for the case it would not suffice, to find relevant second-order structures (as most topological spaces and manifolds cannot be described by any non-trivial invariant relations and operations). That is, a formalization as a weak second-order theory, with sets of structures playing the roles of structures.

First we need to pick up a fixed object (system) K in C, with the quality of being "flexible enough" to serve as the basis to formalize the structures of other objects of C. For many physically useful kinds of systems as listed above, we can take K= (the line of real numbers), which sometimes just needs to be completed by the case K=ℝ², as the resulting structures already suffice to define those that could be brought by further dimensions (ℝn). The main difference between categories with the same K, then, is about which structures are given to this K.

A fixed K allows to interpret any object M in C, as a system with structures that will be preserved by all morphisms of C, in 2 ways, corresponding to both sides of actions:

The set Mor(K,M) of all morphisms from K to M

For any objects M and N of a category C, any morphism from M to N maps the "structure" M0=Mor(K,M) to N0=Mor(K,N) by composition: a function f from M to N is said to preserve this second-order structure if ∀xM0, fxN0.

In the representation theorem for categories, the identification between sets of endomorphisms in the initial category and in the category of typed algebras thus constructed, suggests that if the objects we started with were already some systems and thus we want to see types as similar systems, then the initial object-systems will be mutually constructible with the new systems (sets of morphisms from types to algebras) finally built in the role of new interpretations of objects. For this, types need to be "blocked" by additional structures to not have any remaining internal morphisms (like constructions do not add more automorphisms, but in a sense adapted to the use of morphisms instead of isomorphisms), i.e. to be seen as if it was constructed ex nihilo (a type of constants). (The representation theorem could succeed by its opportunity to choose an action that makes it always work, but now the action is fixed so we have to adapt to it).
Anyway, whatever additional structures on types will keep unaffected (preserve) the action of morphisms between objects. For example if objects were vector spaces then the role of "types" (as systems whose morphisms to the "object" systems play the roles of the new elements of the objects), can be played by vector spaces with choices of basis, that is some ℝn.

We already sketched how first-order structures can be defined from a concrete category. But we only mentioned there about relations. What about operations ? In fact, they may come as particular cases of these relations, that is, when the relations so defined happen to be functional:


A subset BK is called a basis of an object K of a concrete category C if for any object M of C,
uMB,∃!f∈Mor(K,M), f|B=u
In other words, (K,IdB) is an initial object of the category of all (M,u) where M is an object of C and uMB.
Denoting fM,u this unique f, the set K plays the role of a set of B-ary operation symbols, interpreted in each object M of C by as
kK,∀uMB, kM(u)=fM,u(k)


The below is a draft

M is an affine space and M0 is the set of all affine maps from to M.
This condition on f means that f preserves every operation of barycenter between 2 points with any coefficients (because the barycenter of points x and y with coefficients (1-a) and a is the image of a by the unique affine map from to M which sends 0 to x and 1 to y), so that it is an affine map, mapping every straight line into a straight line.

(to be completed)

The set Mor(M,K) of all morphisms from M to K.

Any morphism from M to N maps, by composition, Mor(N,K) into Mor(M,K).
This can define some more rigid structures than would be possible by the first method. For example, morphisms so defined between infinite dimensional topological affine spaces are automatically "continuous", in a sense of "continuity" that is specific to infinite-dimensional spaces, a condition which the algebraic definition by barycenters does not ensure (while both concepts of morphism are equivalent in finite dimensional spaces).

It is very simple to introduce the notion of measure on a topological manifold M : take M* the vector space of continuous functions with real values, then the space of measures on M is the vector space of linear forms on M* that is "generated by M", i.e. the set of limits of sequences of linear combinations of elements of M in the dual of M*. Now taking as M a differential manifold and M* the set of smooth functions on M, then what we get in this construction (closed vector space generated by M) is the space of distributions on M.

Next : Varieties