Groups, automorphisms and invariants

The Galois connection (Aut, sInv) between structures and permutations

In any category, the group of automorphisms Aut(E) of an object E, is the group of invertible elements in its monoid of endomorphisms End(E).

For any set E, the relation of strong preservation between defined as I = ⋃n I(n)R×B where
I(n)={(r,f)∈℘(EnB |∀xEn, xrfxr}:
induces a Galois connection between their powersets: from a given set LR of structures to the automorphism group AutL(E) of permutations which preserve these structures (and thus also all other structures definable from them).

When extending a theory by a definition, the model is modified (as it interprets one more symbol), but keeps the interpretation of types in each model and the sets of isomorphisms between models. This is similar to the case of proofs as follows.

Now can we rebuild a theory by the return way of this Galois connection: starting with a set G of permutations of a set E, looking for the structures preserved by all permutations in G, and finding a few of them from which the others can be defined, letting G be its automorphism group ? This idea is a key to the Erlangen Program for the foundations of geometry.

So to any set GB of permutations, we associate the set of strong invariants of G,
sInv (G) = {rR |{rGI}
satisfying the characteristic property of Galois connections
LR,∀GB, L⊂sInv (G) ⇔ G⊂AutL (E)

This set sInv (G) of strong invariants (relations "strongly preserved" by all elements of G, i.e. for which elements of G are embeddings, and thus automorphisms since GB), may be smaller than the set Inv G of all (weak) invariants that are only "preserved" (for which elements of G are endomorphisms), that will be used later : GB ⇒ sInv (G) = Inv (G ∪{g-1|gG}).

For any model of a theory with several types, its automorphism group is effective on the whole system, but its action (by restriction) on each type it not always effective; then it also acts on each further type that \can be constructed from available ones (as we explained with developments of theories). Thus, constructions of new types preserve the automorphism group of the model seen as an abstract group, separately from its action on specific types.

Closures given by this connection

The composites of these functions give two closures :

For every set LR of relations (i.e. every system based on E), its closure, the set of invariants Inv(AutL(E)) ⊃ L (taking strong or weak invariants gives the same result since AutL(E) is a group), contains every relation definable from L, because isomorphisms preserve all defined structures.
Conversely, a structure r ∈ Inv(AutL(E)) can only distinguish tuples that cannot be moved one to the other by a permutation preserving each structure in L. This intuitively suggests that they are "not similar to each other for the chosen L", so that their distinction by r expresses a dissimilarity that would be expressible from structures in L. However, this reasoning is not rigorous, and the conclusion is not exactly true: both concepts of "invariants" can differ in a way we shall further comment below.

For every set GB, its closure is the automorphism group Aut(sInv G)(E) ⊃ G (the set of all permutations strongly preserving all strong invariants of G). It includes the group G' generated by G, but differs from G' .

Precisely, Aut(sInv G)(E) is the group of permutations that coincide on any n-tuple with some element of the group G' algebraically generated by G, for every number n that we accepted as an arity of a structure : denoting sInv(n)(G) = {rEn | G×{r} ⊂ I(n)},
f∈Aut(sInv(n)(G)(E) ⇔ ∀xEn, ∃ gG',  fx = gx.
Draft of proof :
For every set GB,
For every explicit natural number n = 1+...+1,
For every permutation fB,
the following formulas are equivalent:
f∈Aut(E, sInv(n)(G))
rS(n), r ∈ sInv(n)(G) ⇒ (f,r)∈R(n)
rS(n), G ⊂ Aut(E,{r}) ⇒ (f,r)∈R(n)
rS(n), G' ⊂ Aut(E,{r}) ⇒ (f,r)∈R(n)
s ∈ sInv(n)(G), ∀x1,..,xnE, s(x1,..,xn) ⇔ s(f(x1),...,f(xn))
sS(n), (∀gG, ∀x1,..,xnE, (x1,..,xn)∈s ⇔ (g(x1),..,g(xn))∈s) ⇒ (∀x1,..,xnE, (x1,..,xn)∈s ⇔ (f(x1),...,f(xn))∈s)
⇔(...to be continued) (This can be proven using orbits).
x1,..,xnE, ∃ gG', (f(x1),...,f(xn)) = (g(x1),...,g(xn))

(to be completed)
⟳⤿↻↺↷⟲⤹

Back to Set theory and foundations homepage