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*).

- the set
*R*= Rel_{E}of all relations ("possible structures") on*E*, - the symmetric group of
*E*, (the set*B=*⤹*E*of all permutations).

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.

- In the Galois connection between sets of axioms and classes of models, proofs explore the set of theorems (closure of a given set of axioms), and thus preserve the corresponding class of models.
- In the Galois connection between sets of structures and groups of automorphisms, definitions explore the set of invariant structures (closure of a given set of structures) and thus preserve the corresponding class of isomorphisms between models.

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.

sInv (*G*) = {*r*∈*R* |{*r*}×
*G* ⊂ *I*}

satisfying the characteristic property of Galois connections ∀*L*⊂*R*,∀*G*⊂*B*, *L*⊂sInv
(*G*) ⇔ *G*⊂Aut_{L} (*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
*G*⊂*B*), 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 : *G*⊂*B*
⇒ sInv (*G*) = Inv (*G* ∪{*g*^{-1}|*g*∈*G*}).

The composites of these functions give two closures :

For every set *L*⊂*R* of relations (i.e. every system
based on *E*), its closure, the set of invariants Inv(Aut_{L}(*E*))
⊃ *L* (taking strong or weak invariants gives the same
result since Aut_{L}(*E*) is a group),
contains every relation definable from *L*, because
isomorphisms preserve all defined structures.

Conversely, a structure *r *∈ Inv(Aut_{L}(*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 *G*⊂*B*, 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'* .

For every setG⊂B,

For every explicit natural numbern= 1+...+1,

For every permutationf∈B,

the following formulas are equivalent:

f∈Aut(E, sInv^{(n)}(G))

∀r∈S^{(n)},r∈ sInv^{(n)}(G) ⇒ (f,r)∈R^{(n)}

∀r∈S^{(n)},G⊂ Aut(E,{r}) ⇒ (f,r)∈R^{(n)}

∀r∈S^{(n)},G'⊂ Aut(E,{r}) ⇒ (f,r)∈R^{(n)}

∀s∈ sInv^{(n)}(G), ∀x_{1},..,x∈_{n}E,s(x_{1},..,x) ⇔_{n}s(f(x_{1}),...,f(x))_{n}

∀s∈S^{(n)}, (∀g∈G, ∀x_{1},..,x∈_{n}E, (x_{1},..,x)∈_{n}s⇔ (g(x_{1}),..,g(x))∈_{n}s) ⇒ (∀x_{1},..,x∈_{n}E, (x_{1},..,x)∈_{n}s⇔ (f(x_{1}),...,f(x))∈_{n}s)

⇔(...to be continued) (This can be proven using orbits).

∀x_{1},..,x∈_{n}E, ∃g∈G', (f(x_{1}),...,f(x)) = (_{n}g(x_{1}),...,g(x))_{n}

(to be completed)

⟳⤿↻↺↷⟲⤹

Back to Set theory and foundations homepage