The Buechler dichotomy theorem says that if is a type of Lascar rank 1 in a superstable theory, then has Morley rank 1, or the pregeometry on the set of realizations of is locally modular. This isn't strictly a dichotomy, as may have both properties. The dichotomy theorem can be seen as a trade-off between model theoretic simplicity (Morley rank 1) and geometric simplicity (local modularity).

## Consequences

The dichotomy theorem implies that any type with and is locally modular. Consequently, when checking the Zilber trichotomy principal for types of Lascar rank 1, it suffices to merely check the case of types of Morley rank 1.

As unidimensional theories are controlled by types of rank 1, the dichotomy theorem can be used to show that any unidimensional theory is 1-based or totally transcendental (or both).

## Proof structure

In Pillay's Geometric Stability Theory, a relatively short proof is given, which breaks into two steps:

• In a superstable theory: if and the pregeometry on is non-trivial, then , where is Shelah's continuous infinity-rank. This amounts to showing that in some neighborhood of , all non-algebraic types have Lascar rank 1.
• If and the pregeometry on isn't locally modular, then . This amounts to showing that in some neighborhood of , there are only finitely many non-algebraic types.

For the first point, one uses non-triviality to find three realizations of which are pairwise independent, with each algebraic over the third. If is a formula witnessing the interalgebraicity, and is a neighborhood of having the same -rank, it turns out that the formula gives the desired neighborhood of containing only types of Lascar rank at most 1.

The second point is more complicated, and involves using the characterization of non-local-modularity in terms of plane curves, as well as the definability of rank in sets of -rank 1. The rough idea is to take a 2-dimensional family of plane curves, and show that if and are two generic curves in this family, then is finite, and that the finitely many types of the elements of over the code for yield all the non-algebraic types in . This makes have Morley rank 1, and its projection onto one of the two coordinates will be a neighborhood of the original type , also of Morley rank 1. The argument boils down to a series or rank calculations, and careful management of the issue of formulas versus types. ::: ::: :::