A global invariant type is a type over the monster M which does not split over a small set A, or equivalently, is Aut(M/A)-invariant. We say that this global type is "A-invariant" (or "invariant over A") when we want to specify the set A.
In other words, suppose M is a structure, A ⊂ M is a subset, and suppose that M is |A|+-saturated and |A|+-strongly homogeneous. Then we are interested in (complete) types p(x) on M with the following property: for every from and formula , whether or not depends only on (and on ). Equivalently, whenever , we have
By strong homogeneity, the set of such that is exactly the orbit of under the automorphism group Aut(M/A). So an equivalent condition is that for every a, every formula , and every , we have
.
This is in turn equivalent to the condition that for every , i.e., that is invariant under Aut(M/A).
Global invariant types are essentially the same thing as what Poizat calls "special sons" in his Course in Model Theory.
A somewhat prototypical example of a global invariant type is the generic type of a geometrically irreducible variety in ACF. Let K be a field, and embed K in some very saturated and strongly homogeneous monster model M of ACF. If is a geometrically irreducible affine variety, then is irreducible over M, and we can talk about the generic type p(x) ∈ Sn(M). This is the type which says that the n-tuple x lies on V, but not on any strictly smaller M-definable closed subvarieties of V. This type is K-invariant, i.e., Aut(M/K)-invariant. This is fairly clear by symmetry considerations: if , then sends the variety V to itself, and sends proper subvarieties of V to proper subvarieties of V. Since is characterized as being the unique type over M which lies on V but not on any proper subvarieties, must be the same type as .
We should also point out that coheirs are invariant types: if a global type is a coheir of its restriction to a small model M, then is M-invariant.
Definable types are another source of global invariant types. (In fact, in stable theories, definable types and invariant types are the same thing.)
Work inside a monster model of some theory.
Theorem: Let M be a small model (i.e., small elementary substructure of ), and p(x) be a complete type over M. Then there is at least one global M-invariant type extending p.
Proof: Let be the (big) partial type over consisting of the statements
for every formula , and every from such that (i.e., such that a and b have the same type over M).
Note that is satisfied by every element of M. Indeed, if c ∈ M and , then so , and therefore
for every formula .
Now any finite subset is satisfied by some tuple c from M. This tuple satisfies . It follows that is consistent for every finite subset . Therefore is a consistent partial type over the monster .
Let be any complete type over the monster extending . Then is our desired global M-invariant type. Indeed, if a and b are two tuples from having the same type over M, then
because extends . But because is a complete type, it follows that
.
Given that this holds for any formula and any two tuples having the same type over M, it follows that is M-invariant, for reasons explained above.
QED.
From this we see that non-trivial examples of global invariant types exist in any theory.
A global type p(x) is A-definable if for every formula , there is a formula over A such that
,
for every b in M. We think of the map as a "definition schema." The formula is called the "-definition of p." If p is definable, then it is always A-definable over some small set A.
Now if , then
,
where the middle comes from the fact that is a formula over A. Thus p is A-definable; A-definable types are A-invariant. The notion of "A-invariant type" can be seen as a generalization of "A-definable type" in which the -definition of p is no longer given by a formula over A, but by a set of complete types over A. That is, there is some subset such that for every b,
.
If were the clopen set associated with some A-formula , then this would mean that
.
An A-definable type p(x) over a model M has a unique global extension q(x) which is A-definable. Essentially, the definition schema for q(x) must be the same as the definition schema for p(x). Something similar happens with invariant types:
Theorem: If M is |A|+-saturated and |A|+-strongly homogeneous, then each A-invariant type on M has a unique global extension which is A-invariant.
Proof: Let q(x) be the set of all formulas , where b is a tuple from the monster such that for some tuple c from M such that . We claim that q(x) is a consistent type, it is a complete type over the monster, that it is A-invariant, and that it is the only global A-invariant type.
First of all, we check consistency. Suppose for the sake of contradiction that
is inconsistent. By definition of q(x), we can find such that for each i, and .
Now because M is |A|+-saturated, we can find in M such that
.
Then for each i,
.
By strong homogeneity, some sends to . By invariance of p(x),
.
So for . Now by assumption
.
Since the bi's collectively have the same type as the di's,
.
But we just claimed that for each i, so p(x) is inconsistent, contradicting the fact that it is a complete type.
Next, we check that q is a complete type. Let be a formula and b be a tuple from the monster. By saturation of M, we can find some c in M such that . Because p is complete, either or is in p(x). Then by definition of q(x), either or is in q(x). So q is complete.
Next we check A-invariance. Suppose for in the monster. By saturation of M, we can find c in M realizing . Then by definition of q, for each formula
.
As explained above, this shows that q is A-invariant.
Finally, suppose r were some other A-invariant global type extending p. Then for any b in the monster and any formula , we have
where c is any realization of tp(b/A) in M.
QED.
Work in a monster model . Recall the following (standard) notation:
Lemma: Let A be a small subset, let q(x) be a (complete) type over A, and let p(y) be a global A-invariant type. Then
is the set of realizations (in the monster) of some complete type over A.
Proof: First of all, S is non-empty, because q and p are consistent types (and the monster is saturated).
Next, any two tuples in S have the same type over A. Indeed, suppose that . Then and both realize q, so there exists some automorphism over A sending to . Because p is A-invariant, . The fact that realizes implies therefore that realizes
.
Thus . But then
,
so and have the same type over A, as claimed.
Finally, suppose that is in S, and . Then , so realizes q. Also, there is some automorphism fixing A, and sending to . Then fixes p, so
.
Meanwhile,
,
so
.
Then since realizes , so does . Now we know that
and .
So , as claimed.
(A shorter way to see this is to argue from symmetry that S must be A-invariant, because it is defined using only A, a type over A, and an A-invariant global type. So any symmetry which fixes A must certainly send S to itself. Then if and , some automorphism over A sends to , and therefore is in S.)
At any rate, we have shown that S is non-empty, any two elements have the same type over A, and that any tuple having the same type over A as someone in S is itself in S. Therefore, S is exactly the set of realizations of some complete type r over A.
QED.
Theorem/Definition: Let p(x) and q(y) be two global A-invariant types. Then there is a unique global type with the following property: for every small set C containing A, and every a and b from the monster, the following are equivalent:
The type is A-invariant. Moreover, does not depend on the choice of A (i.e., it remains the same if we replace A with a bigger set.)
Proof: Note that for any small C containing A, p is C-invariant, because . By the Lemma, we can find a complete type over C such that the following are equivalent for a and b tuples from the monster of the appropriate lengths:
We claim that if , then extends . Equivalently, if , then . But this is clear because
and
.
Let be the union of the 's as C ranges over small supsersets of A. From what we have just seen, is a consistent type, hence a complete global type. It has the desired characterization that for any small set C containing A,
if and only if
This uniquely characterizes the type. Moreover, must be A-invariant, by symmetry. (It is defined only using A-invariant entities.)
Finally, let us verify that the choice of A does not matter. For small B ⊇ A, let denote the B-invariant tensor product of and viewed as B-invariant types. The conditions which uniquely characterize are clearly as strong as the conditions which uniquely characterize , so the two must be equal:
.
Now if A and B are two different small sets over which p and q are invariant, then
.
QED.
Now if and are two invariant types (over some small sets), then we can uniquely define the tensor product , by finding some A over which both p and q are invariant. (For example, if p is B-invariant and q is C-invariant, then any small A ⊇ B ∪ C works.)
The tensor product is usually denoted .
The tensor product operation on global invariant types generalizes the notion of taking the cartesian product of two varieties, in the following sense. Work in a monster model of ACF. Let V and W be two irreducible affine varieties, and let p and q denote the corresponding generic types, over the monster model. Then is the generic type of . Let's prove this.
Claim: Let V be an irreducible variety. Let p be the global generic type of V. Let K be any (small) field over which V is defined. Then a tuple a (from the monster) realizes if and only if a is on V and tr.deg(a/K) = dim(V).
Proof: First suppose that . The statement is certainly a formula over K, so it is in , and therefore . This ensures that tr.deg(a/K) ≤ dim(V). If the equality was strict, then a would lie on some K-definable variety W of dimension less than dim(V). (Of course W might not be irreducible.) Then V ∩ W is a K-definable proper closed subvariety of V. The type p(x) certainly contains the statement x ∉ V ∩ W, and since this statement is over K, it is in . Therefore a ∉ V ∩ W, a contradiction.
For the converse, let denote the algebraic closure of . This is a model of ACF, so an elementary substructure of the monster (by model completeness of ACF). The type says (among other things) that x is on V and not on any strictly smaller -definable subvarieties of V, if not more. But by the characterization of complete types over models of ACF, can be nothing but the generic type of V, as one would expect.
Now if a is on V and tr.deg(a/K) = dim(V), then a is on V, and not on any strictly smaller -definable subvarieties of V. (Indeed, if a is on -definable , then dim(W) < dim(V) and
,
a contradiction.) So a realizes the generic type of V over , i.e., a realizes . It certainly then also realizes the restriction of this to K, which is .
The claim is proven.
Theorem: Let V and W be irreducible varieties with global generic types p(x and q(y). Then is the generic type of .
Proof: Let K be a field over which V and W are defined. So p, q, and are all K-invariant. Let r be the global generic type of . The type r is also K-invariant.
For any small L ⊇ K, and tuples a and b of the appropriate lengths, we have the following series of equivalent statements
So we see that and have the same restriction to any small subfield. Therefore, they are equal.
QED.
The tensor-product operation on invariant types is associative, in the sense that is the same as . This follows by unwinding the definitions.
Indeed, if C is any small set over which p, q, and r are invariant, and if a, b, and c are appropriately-sized tuples, then the following conditions are equivalent:
Each of these conditions is equivalent to the next one, by the definition of .
Since associativity holds, we can write unambiguously.
In general, a realization of 's restriction to C is a sequence such that
And so on, down to
In the example of ACF, associativity means that the generic type of is the same as the generic type of , which is clear.
Two global invariant types p(x) and q(y) are said to commute if . In other words,
.
(This is not the same as saying that is ; the variables must be kept track of.)
Ideally, commutativity would always happen. This is the case in stable theories, and in NIP theories when one of the types is generically stable. In the example of ACF, this reflects the fact that if is a generic point on , then is a generic point on .
Here is an example of failure of commutativity. In the theory of dense linear orders, let p be the definable 1-type at +∞. This is Ø-invariant. If C is a small subset of the monster, then if b > C (i.e., b is bigger than every element of C) and a > b. But of course this is different from , which implies that b > a > C. So p does not even commute with itself.
If p is a global A-invariant type, a Morley sequence in the type p is a sequence where
for each i. This definition easily generalizes to Morley sequences of any ordinal length.
Theorem: A Morley sequence in the type p is indiscernible over A'. Any two Morley sequences in p have the same type over A (assuming they have the same length).
Proof: Let be a Morley sequence. Note that if then for 1 ≤ k ≤ n, realizes , because . It follows that
Consequently, if is some other ascending sequence, then
and both realize .
Therefore, we have indiscernibility. Also, if is some other Morley sequence, then for each n,
and both realize .
So . Since this happens for all n, the two Morley sequences have the same type over A. (This argument can easily be modified to handle the case of Morley sequences of length more than .)
QED.
Morley sequences of this type play a key role in elementary stability theory, where they can be used to prove the definability of types in stable theories.
Also, we can use this kind of Morley sequence to prove the existence of non-trivial indiscernible sequences.
Corollary: Let M be a structure with an infinite total ordering < (one one of the sorts). Then there is an elementary extension of M in which there is a strictly increasing indiscernible sequence .
Proof: Let be a monster model of the complete theory of M. Since M (or its totally ordered sort) is infinite, there is some complete type p over M which lives in the ordered sort, but is not realized in M (i.e., is not constant). Let q be a global M-invariant extension of p, which exists for reasons explained above. If q were realized in then q(x) would be a constant type of the form x = a for some a from . Then by M-invariance, a would need to be fixed by every automorphism which fixes M. This would force a to be in the definable closure of M, which is M. So q(x) includes the statement x = a, and so does p(x), contradicting the assumption that p is not a constant type.
So q is not a constant type. Then for any small set C and any c ∈ C, the formula x ≠ c is in .
In particular, if is a Morley sequence for q, then , so . In other words, no two elements of the Morley sequence are equal. Also, the sequence is M-indiscernible, hence indiscernible (over the empty set).
Because the ordering is total, either or . In the former case, indiscernibility implies that for every i, so the sequence is increasing and we are done. Otherwise, we can extract an indiscernible sequence of the same Ehrenfeucht-Mostowski type, but indexed by the negative integers
.
As part of the EM type, we see that
Then
is our desired increasing indiscernible sequence.
In more detail (without mentioning EM types), consider the infinitary partial type consisting of the statements asserting indiscernibility of together with . Then is consistent, because if is a finite subset, then only mentions for some n, and then
Any realization of the consistent type will yield our desired indiscernible sequence.
Having found the increasing indiscernible sequence, we can pass to a small model if we like, or just stick with the monster as our elementary extension of M.
QED.
From this, it is not hard to prove that indiscernible sequences can be extracted in general.
Corollary: Let M be a structure, and let be any infinite sequence (with I an ordered set). Then we can find an elementary extension of M in which there is an indiscernible sequence realizing the EM type of .
Proof: Consider the auxiliary structure obtained by adding I as a new sort, and adding symbols for the total ordering on I and a function symbol f for the map . By the previous Corollary, we can find an elementary extension containing an increasing indiscernible sequence in the new I sort. Then is certainly indiscernible in . Let N be the reduct of to the original language (dropping the extra I sort). Then N is an elementary extension of M. Also, is certainly indiscernible in N.
Finally, we check that this indiscernible sequence satisfies the correct EM type. Suppose that is a formula in the EM type of . This means that
whenever .
But then
.
Of course the same thing must hold in , which means that for any ,
,
because .
Then since was a formula in the original language,
.
As this holds for any , the sequence really does satisfy the correct EM type.
QED. ::: ::: :::