For any set

For any relational system

Aut_{L}(*E*) ={f∈ End_{L}(*E*)∩⤹*E*|*f*^{
-1}∈End_{L}(*E*)}.

In a monoid with identity element *e*, the formula *x*•*y*=*e*
is read "*x* is a left inverse of *y*", and "*y*
is a right inverse of *x*".

(

If *y* has both a left inverse *x* and a right
inverse *z* then *x*=*z*:

(*x*•*y* = *e* = *y*•*z*) ⇒ *x*
= *x*•*e* = *x*•(*y*•*z*) = (*x*•*y*)•*z*
= *e*•*z* = *z*

We say that *y* is an *inverse* of *x* if it is
both a left inverse and a right inverse; then it is the only right
or left inverse of *x*. The inverse of an isomorphism is always unique.

An element *x* of a monoid is called an *involution*
if it is its own inverse (equivalently on one or both sides): *x*•*x*=*e*.

The theory of (abstract) group is that of monoid *G* with
one more symbol: a function symbol called inversion, *x*↦*x*^{-1},
with axioms saying that *x*^{-1} is the inverse of *x*
(its interpretation is thus determined by that of •):

- ∀
*x*,*x*•*x*^{-1}=*x*^{-1}•*x*=*e*

Thus, inversion is an involution in the transformation monoid of

(

Groups are cancellative. Any submonoid of a cancellative monoid (such as a group) is cancellative, but (according to wikipedia - I don't know any example) a cancellative monoid cannot always be embedded in a group (i.e. be isomorphic to a submonoid of a group).

We only have this : any monoid both commutative and cancellative, can be embedded in a commutative group.

A subset

(

Thus any function between groups preserving composition, is also a morphism of groups (since its image behaves as a group).

We can similarly define a left action of a group

Inversion reverses the order of composition, so that left and right actions of

The automorphism group of a given system, was defined as the set
of permutations which preserve all structures of its language (and
thus also all other structures definable from them).

It is part of a Galois
connection between powersets of

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

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

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.

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