I know 'Theorems as Definitions' as 'French definitions'.
In algebraic geometry the main objects of study are algebraic varieties and more generally schemes. Although the proper definition of schemes is famously involved one can best think of them as the space of solutions of polynomials equations ('zeroes of polynomials'). The natural topology on this space (the Zariski topology) is quite weird - it is generically non-Hausdorff and can even have non-closed points. For instance, the 'right way' of saying a scheme is Hausdorff is not asking for the underlying topological space to be Hausdorff [which only gives very trivial examples] but to ask for the diagonal map to be a closed subscheme.
This is an example of your abstract-concrete cycle: for ordinary topological spaces Hausdorff and closed diagonal are equivalent, but the latter can be defined more broadly for schemes.
Grothendieck is famous for his many French definitions. Many of the constructions he proposed were inspired by constructions and theorems in classicial differential and complex analytic geometry but then ported to the algebraic and arithmetic realm.
Grothendieck predecessors noted that many features of algebraic varieties resemble those of more traditionally geometric spaces. I.e. Andre Weil, in his Weil conjectures observed that the number of solutions of a variety over finite fields (i.e. modulo p) is closely related to the number of higher-dimensional holes ('Betti numbers') of the complex analytic manifold associated to the set of equations of the variety. This geometric shadow was a guiding motif for Grothendieck's work. He realized that the Zariski topology did not properly capture the 'inherent' geometric structure of algebraic equations.
The naive solution to this conundrum would be to look for a topology on the sets of solutions of polynomials that is Hausdorff to replace the Zariski topology. But this is the wrong move - there is no such topology. Instead Grothendieck noted that the properties that are required these geometric analogues are only a subset of the properies of a topological space. Roughly speaking, for (co)homological reasoning to go through one only needs to known when a collection of opens 'cover' another open. This is an instance of your 'Abstract-Concrete-Cycle'.
By pursuing this analogy He generalized the notion of topological space to Grothendieck topology (which leads to fancy things like sites and topoi). This leads to the famous etale topology and etale cohomology which eventually lead to the proof of the Weil conjectures.
An early triumph of the Grothendieckian way of thinking was his French definition of the etale fundamental group. Naively trying to define a fundamental group for an algebraic variety fails because there aren't enough loops, hence the usual fundamental group is almost always trivial. This is Zariski topology weirdness.
Instead, Grothendieck noted that there is a classical theorem that the fundamental group can also be seen as an automorphism group of locally trivial topological covers. He then identified a property 'etaleness' (following a suggestion by Serre) that is the analogy of locally trivial topological covers for algebraic varieties and schemes. The étale fundamental group is then simply defined in terms of automorphisms of these etale covers. This may strike one as just a mummer's trick - but it's actually profound because it turns out Galois theory becomes a special case of the theory of etale fundamental groups ('Grothendieck-Galois theory').
1
1
(crossposted from here)
I've noticed there are certain epistemic motifs (i.e. legible & consistent patterns of knowledge production) that come up in fairly wide circumstances across mathematics and philosophy. Here's one that I think is fairly powerful:
Abstract-Concrete Cycles and Domain Expansion
Given a particular object [structure/definition] that models some concept, we can modify it by either [abstracting out some of its features] or [instantiating a more concrete version of it] as we [modify the domain of discourse] that the object operates on, accompanied with [intuition juice from the real-world that guides our search]. Repeat this over various abstraction-levels, and you end up with a richer set of objects.
Examples of how this plays out
a) Space
Here's an example from mathematics (inspired from here). You have some concrete notion of a thing you want to capture, say, space. So you operationalize it using some immediately obvious definition like Rn which, being extremely concrete, comes equipped with a bunch of implicit structures (metric, angle, explicit coordinates, etc) - many of which you probably didn't explicitly intend or even superfluous to your aims.
Then you abstract away the structures one-by-one, e.g.,
And with this more abstract notion of space in hand, you can project it down to more concrete structures in domains different from that of original consideration, effectively using it as a generator. e.g.,
From here, the loop continues. With a concrete structure in hand that captures what you want, but now with a flavor of operating in a different domain, this may yield insight into how certain structures that were not originally under your consideration might further be abstracted away.
After you continue this process of abstracting/concretizing your structure over many different levels of abstraction (each being conducive to describing different sorts of domain of discourse), you end with an extremely rich notion of space, some far different from your original Rn.
b) Notion of "Optimization"
In philosophy, I think the case is much more obvious. Alex Flint's ground of optimization, for example, compares different definitions of optimization primarily by means of domain of discourse expansion, i.e. case analysis of the definition in "weird" scenarios, see which notions generalize better and fit our intuitive notion of what the word "optimization" should mean.
c) Epistemic motif of "Theorem as Definition"
Theorems in one structure can now become a definition in another. This is highly related to the earlier motif: we can consider some theorem as a consequence of the concrete [features/axioms] of the original structure, and view [the act of turning the theorem into a definition in a much more [relaxed/general] structure] as abstracting out [the particular concept that the theorem captured in the original structure]. e.g.,
It's The Rising Sea!
Why does it work?
I can think of a couple reasons why this process works (inspired from here), with "why" in the sense of the reason for its effectiveness as a human process for epistemology.
Just by selection, the concepts that we end up modeling (and with scientists building intuitions about what can be modeled in the first place) tend to be ones that can be captured by a small number of desiderata.
If the desiderata rule out all possibilities or rule in too much, we can correct our intuitions/desiderata, eg discovering assumptions that subtly restricted the form of our structures in ways which we haven't noticed.
And by finding such "minimal conditions" our structure must satisfy, it becomes more conducive to adding new structures back in, such that it could be made more concrete for applications into a new domain of discourse. From there, we can list examples and find new theorems, thus enriching our intuition that feeds back into this loop.