∀*z,t*∈*M*, *y*•*z* = *t* ⇒ *x*•*t* = *z*

Similarly in any category, the inverse of any isomorphism (= invertible morphism) is unique.

As left invertible functions are injective, left invertible elements are left cancellative:

∀*z,t*∈*M*, (*y*•*z* = *y*•*t* ∧ *x*•*y*=*e*) ⇒
(*z* = *x*•*y*•*z* = *x*•*y*•*t*
= *t*)

If a left invertible element is also right cancellative then it is invertible.
Any left cancellative element of a finite monoid is invertible.

Proof: it acts as an injective transformation of
a finite set, thus a permutation, by which the preimage of *e* is a right inverse, thus an inverse.

*x*•*y*=*y*•*x* ⇔ *x*=*y*•*x*•*z* ⇔ *z*•*x*=*x*•*z*

The set of invertible elements in any monoid, is a group :

- it is a sub-monoid : if
*x*and*y*are invertible then*x*•*y*is invertible, with inverse*y*^{-1}•*x*^{-1}(like in 2.6). - Inverses are invertible (and by uniqueness of the inverse, inversion is an involutive transformation of any group).

- a sub-monoid which is a group, or
- a subalgebra for the
*language of groups*{*e*, •,^{-1}} extending the one {*e*, •} of monoids, with the function symbol^{-1}of inversion.

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

As inversion is an anti-morphism, it switches any left action ▪ of

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

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

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

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