Like in a set theoretical framework, for geometries with nontrivial automorphisms,
multiple models (spaces) may be interestingly considered in each isomorphic class
(instead of taking one to represent them all), for the following reason.
Any isomorphism *f* between 2 systems *E* and *F* induces a bijection
*g* ↦ *f*০*g* from Aut(*E*) to the set of isomorphisms
between *E* and *F*. Thus, a plurality of automorphisms
of *E* means a plurality of isomorphisms between *E*
and *F*. This plurality makes the difference between *E* and *F*
meaningful, as an object in *E* may correspond to several possible ones in
*F*, depending on the choice of isomorphism, so choosing an object in *E* does
not mean choosing an object in *F* in any invariant way. By contrast, the uniqueness of
isomorphism between standard models of ℕ or ℝ makes them unambiguously
play the role of each other (copies of each other), rendering their plurality superfluous.

sInv (*G*) = Inv (*G*
∪ -*G*) = Inv (*G*) ∩ Inv(-*G*)

∀*L*⊂Rel_{E}, ∀*G*⊂ ⤹*E*, *L*⊂sInv
(*G*) ⇔ *G*⊂Aut_{L}(*E*).

Like proofs explore truths (theorems), that is the closure of the set of axioms,
whose addition to axioms preserves the class of models,
definitions from a
language *L*⊂*R* explore its closure sInv(Aut_{L}(*E*))
= Inv(Aut_{L}(*E*)) ⊃ *L*, whose addition to
*L* leaves unchanged the set of automorphisms of each model
(among other isomorphisms between models).
Constructions leave unchanged the groups of automorphisms as abstract
groups, just providing more types on which these groups act.

Our last scheme
of constructions (set of all structures
defined by an expression with all values of parameters), was that of an
invariant second-order structure that is a set of non-invariant first-order
structures. Well-defined by that formula, its invariance by
automorphisms means that automorphisms preserve that set while acting as
permutations on it.
For example, Euclidean space geometry admits the type "plane", each plane is a set of points,
and automorphisms can move any plane to any other plane. On Earth,
"the sea level" names a plane, distinguishing its points from those above or below it,
but Euclidean geometry does not see it as invariant, i.e. does not accept the name "sea level"
in its language. A language accepting it, would form a different geometry.

A tuple

Both concepts of invariance can be still reconciled in different ways:

- For first-order logic, non-trivial automorphisms may externally exist over non-standard models of second-order arithmetic, thus also non-standard real closed fields (moving undefinable real numbers to infinitely close neighbors);
- In second-order logic, we may admit "second-order" ways of defining structures where any subset of ℕ is "defined" by the infinite data of all its elements(*).
- In the practice of geometry, "invariance" will be meant by automorphisms, and equivalently qualify structures defined with parameters in ℝ or among structures over ℝ only.

A core idea of Felix Klein's Erlangen
Program for the foundations of geometry, was to rebuild the geometry of
a space *E* from a permutation
group *G* of *E* intended as its group of
automorphisms: can we find a good list *L* of a few structures from
its set of invariants (Inv *G*), which would suffice to define other useful
invariant structures (yet not the uncountable set of them all), at least so that
*G*=Aut_{L} ?

As we saw with relations
defined by tuples, the set Inv(*G*) is made
of orbits of tuples, and any unions of these.

∀*u*∈*M ^{B}*, ∃!

The category has a natural action on this type on the same side as it acts on the space: for any spaces

Such constructions are interestingly similar to those of the representation theorem for categories.

First is the set {Im

Two invariant subsets of this (but which may not bring anything new depending on the geometry)
are the embeddings and the sections. As already
discussed, these are successive qualities for subspaces *A* = Im *f* to become
spaces on their own right, which means (instead of structures for *A*) to give its morphisms
with other spaces.
For example,
if a geometry admits a circle and a plane as spaces, the circle may have an embedding into the plane
but that is not a section. (In the case of differential geometry, this concept of embedding may be less strict than
the standard one, I did not check)

∀*f*∈Mor(*M*,*N*), ∀*A*∈*H _{M}*,

The similar concept to embeddings with reversed sides, is the concept of quotient space by a given relation.

(*)This bridge to Inv(Aut

Homepage : Set Theory and Foundations of Mathematics