Groups, automorphisms and invariants

Groups

Groups are algebras with the same properties as permutation groups.
For any set G⊂⤹E, the permutation group generated by G, is the generated subalgebra of ⤹E with these 3 symbols, and is also transformation monoid generated by G ∪{ f -1 |f G}.
For any relational system E with any language L, the set of automorphisms of an L-system E, is a permutation group

AutL(E) ={f∈ EndL(E)∩⤹E|f -1∈EndL(E)}.

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

The formula of cancellativity works in a monoid on elements having an inverse:
(xz = yzzt=e)⇒ (x = xzt = yzt = y)

If y has both a left inverse x and a right inverse z then x=z:
(xy = e = yz) ⇒ x = xe = x•(yz) = (xy)•z = ez = 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): xx=e.

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

Since x and (x-1)-1 are two inverses of x-1, they are equal : (x-1)-1=(x-1)-1x-1x =x.
Thus, inversion is an involution in the transformation monoid of G. It is also a semi-endomorphism:
(xy) -1=y-1x-1. The proof goes like in 2.6, i.e. from the fact that y-1x-1 is an inverse of xy.

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 A of a group G that is stable by composition, may not be a subgroup; but (as G is cancellative) we have the equivalence:
(A behaves as a group (as expressed with ∃)) ⇔ (A is a subgroup (i.e. stable by identity and inversion)).
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 G on a set X, as expressing a group morphism from G to the group of permutations of X. Actually both concepts of action coincide: if f: GXX is a morphism of monoid then ∀aG, f(a)०f(a-1)= f(aa-1)=f(e)=IdX= f(a-1a)=f(a-1)०f(a), thus f(a) is bijective and f is a morphism of groups (f(a-1) = f(a)-1).

Inversion reverses the order of composition, so that left and right actions of G on X are exchanged by inversion (one • can be defined from the other ▪ by ∀xX, ∀gG, x•g = g-1▪x ; these actions usually do not commute...).

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

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

Indeed for any LR, the automorphism group AutL(E), is defined as { fB | L×{f} ⊂ I} from the relation of "strong preservation" I = ⋃n I(n)R×B where
I(n)={(r,f)∈℘(EnB |∀xEn, xrfxr}:

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.

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.

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