<p>I give it a try to answer my own question after having read more carefully the material in the text by Abramsky and Jung (AJ). I believe there are two reasons why we turn to the category of embeddings:</p>
<ol>
<li><p><span class="math-container">${\bf Practicality:}$</span> As it is mentioned in AJ, page 71, &quot;<em>Continuity of a functor is a hard condition to verify. Luckily there is a property which is stronger but nevertheless much easier to check</em>&quot;. Applying the basic lemma directly to a functor <span class="math-container">$F$</span> is a tedious task because verifying the condition of the lemma is very similar to verifying continuity of the functor. Instead of following this tedious road, we define the notion of <em>local continuity</em> (see AJ for details). It is generally straightforward to verify that an everyday functor is locally continuous: almost all the basic constructors that arise in domain equations, are locally continuous and the composition of locally continuous functors is also locally continuous. Now comes the interesting part: as it is shown in AJ (Proposition 5.2.4), a locally continuous functor <span class="math-container">$F : {\bf D} \rightarrow {\bf D}$</span> restricts to a continuous functor <span class="math-container">$F^e: {\bf D}^e \rightarrow {\bf D}^e$</span>. In other words, local continuity implies continuity in the category of embeddings. Now, we can apply the Smyth-Plotkin basic lemma directly on <span class="math-container">$F^e$</span> (because every continuous functor satisfies the conditions of the lemma).</p>
</li>
<li><p><strong>Mixed-variant functors:</strong> The second reason we don't use directly the basic lemma is that it ony applies to covariant functors. Therefore, the basic lemma can not be applied to mixed variant functors, such as the &quot;arrow&quot; one, or more generally functors of the form <span class="math-container">$F: {\bf D}^{op} \times {\bf D} \rightarrow {\bf D}$</span>. It turns out that we can define a notion of local continuity that covers such functors. Then, it can be shown that we can define a functor <span class="math-container">$F^e: {\bf D}^{e} \times {\bf D}^{e} \rightarrow {\bf D}^{e}$</span>, ie., a covariant functor in the category of embeddings. This functor is continuous and therefore the basic lemma is again applicable.</p>
</li>
</ol>

CC BY-SA 4.0
2023-01-31T09:39:49.923Z
Excellent answer, you should accept it :-)
Andrej Bauer
CC BY-SA 4.0
2023-01-31T10:51:39.927Z
Thanks for pressing me to work harder :-)
LaR
CC BY-SA 4.0
2023-01-30T17:16:30.123Z
2023-01-30T17:23:09.680Z
2023-01-30T17:23:09.680Z
LaR
<p>In Section 5.2 of the text  on Domain Theory by S. Abramsky and A. Jung, it is mentioned that:</p>
<p><em>&quot;Suppose we are given a recursive domain equation <span class="math-container">$X \cong F(X)$</span> where the right hand
side defines a functor on a suitable category of domains. As suggested by the example in Section 5.1.2, we want to repeat the trick which gave us fixpoints for Scott-continuous functions, namely, to take a (bi-)limit of the sequence <span class="math-container">$\mathbb{I}, F(\mathbb{I}), F(F(\mathbb{I})),\ldots$</span>.
Remember that bilimits are defined in terms of e-p-pairs. This makes it necessary that
we, at least temporarily, switch to a different category.&quot;</em></p>
<p>I don't understand why we need to switch to the category of embeddings in order to compute the least fixpoint of <span class="math-container">$F$</span>. More specifically, why don't we just apply the Smyth-Plotkin basic lemma on <span class="math-container">$F$</span> in the initial category in order to find the fixpoint?</p>

CC BY-SA 4.0
2023-01-27T11:32:26.800Z
Assuming you're referring to Lemma 2 in [The category-theoretic solution of recursive domain equations](https://homepages.inf.ed.ac.uk/gdp/publications/Category_Theoretic_Solution.pdf),  you have to check the condition about colimiting cocones. Have you checked it?
Andrej Bauer
CC BY-SA 4.0
2023-01-27T14:03:58.213Z
Thanks for your response. Yes, I am referring to Lemma 2 of the mentioned paper. So, what you mean is that if we restrict attention to the category of embeddings, we don't need to check the requirement for the colimiting cones?
LaR
CC BY-SA 4.0
2023-01-27T16:10:19.313Z
I don't actually know all possible ways in which the basic lemma can fail or succeed. What I am suggesting is that you should actually attempt to use the lemma in the way you are suggesting and see if it goes through, checking all the details. Have you done so?
Andrej Bauer
CC BY-SA 4.0
2023-01-27T16:17:41.763Z
Concretely, if you keep reading all the way to Definition 3, they require that every $\omega$-chain have a colimit. This is not going to be true if we take all continuous maps as morphisms (I have not checked the details, just going on gut feeling), but will be true if take embeddings.
Andrej Bauer
CC BY-SA 4.0
2023-01-27T16:48:36.327Z
But the basic lemma does not require all $\omega$-chains. It just requires a particular one which starts from $< \perp, \perp_{F(\perp)}>$, where $\perp_{F(\perp)}$ is the unique morphism from $\perp$ to $F(\perp)$. So, if I am not mistaken, the basic lemma produces at each step of its construction the same object and morphism as if we were working in the category of embeddings.
LaR
CC BY-SA 4.0
2023-01-28T10:36:47.847Z
This discusssion would be a great deal more constructive if you let us know what I've asked twice before: have you actually attempted to wite down the proof supporting your idea? We are never going to get to the truth by giving opinions about suggestions – and I feel the most interested party (you) should should the willingness to do the work. If and when you get stuck concretely, I am more than happy to contribute.
Andrej Bauer
<ct.category-theory>
Fixpoint of a functor in the category of embeddings
LaR
# Fixpoint of a functor in the category of embeddings

(Asked by: username_0 on 2023-01-26)

In Section 5.2 of the text on Domain Theory by S. Abramsky and A. Jung, it is mentioned that:

*"Suppose we are given a recursive domain equation $X \cong F(X)$ where the right hand
side defines a functor on a suitable category of domains. As suggested by the example in Section 5.1.2, we want to repeat the trick which gave us fixpoints for Scott-continuous functions, namely, to take a (bi-)limit of the sequence $\mathbb{I}, F(\mathbb{I}), F(F(\mathbb{I})),\ldots$.
Remember that bilimits are defined in terms of e-p-pairs. This makes it necessary that
we, at least temporarily, switch to a different category."*

I don't understand why we need to switch to the category of embeddings in order to compute the least fixpoint of $F$. More specifically, why don't we just apply the Smyth-Plotkin basic lemma on $F$ in the initial category in order to find the fixpoint?

**Tags:** ct.category-theory
> **Comments:**
> **username_1**: Assuming you're referring to Lemma 2 in [The category-theoretic solution of recursive domain equations](https://homepages.inf.ed.ac.uk/gdp/publications/Category_Theoretic_Solution.pdf),  you have to check the condition about colimiting cocones. Have you checked it?  
> **username_0**: Thanks for your response. Yes, I am referring to Lemma 2 of the mentioned paper. So, what you mean is that if we restrict attention to the category of embeddings, we don't need to check the requirement for the colimiting cones?  
> **username_1**: I don't actually know all possible ways in which the basic lemma can fail or succeed. What I am suggesting is that you should actually attempt to use the lemma in the way you are suggesting and see if it goes through, checking all the details. Have you done so?  
> **username_1**: Concretely, if you keep reading all the way to Definition 3, they require that every $\omega$-chain have a colimit. This is not going to be true if we take all continuous maps as morphisms (I have not checked the details, just going on gut feeling), but will be true if take embeddings.  
> **username_0**: But the basic lemma does not require all $\omega$-chains. It just requires a particular one which starts from $< \perp, \perp_{F(\perp)}>$, where $\perp_{F(\perp)}$ is the unique morphism from $\perp$ to $F(\perp)$. So, if I am not mistaken, the basic lemma produces at each step of its construction the same object and morphism as if we were working in the category of embeddings.  
> **username_1**: This discusssion would be a great deal more constructive if you let us know what I've asked twice before: have you actually attempted to wite down the proof supporting your idea? We are never going to get to the truth by giving opinions about suggestions – and I feel the most interested party (you) should should the willingness to do the work. If and when you get stuck concretely, I am more than happy to contribute.  

---

## 1 answers

### Answer by username_0 on 2023-01-30. Score: 5

I give it a try to answer my own question after having read more carefully the material in the text by Abramsky and Jung (AJ). I believe there are two reasons why we turn to the category of embeddings:

1. ${\bf Practicality:}$ As it is mentioned in AJ, page 71, "*Continuity of a functor is a hard condition to verify. Luckily there is a property which is stronger but nevertheless much easier to check*". Applying the basic lemma directly to a functor $F$ is a tedious task because verifying the condition of the lemma is very similar to verifying continuity of the functor. Instead of following this tedious road, we define the notion of *local continuity* (see AJ for details). It is generally straightforward to verify that an everyday functor is locally continuous: almost all the basic constructors that arise in domain equations, are locally continuous and the composition of locally continuous functors is also locally continuous. Now comes the interesting part: as it is shown in AJ (Proposition 5.2.4), a locally continuous functor $F : {\bf D} \rightarrow {\bf D}$ restricts to a continuous functor $F^e: {\bf D}^e \rightarrow {\bf D}^e$. In other words, local continuity implies continuity in the category of embeddings. Now, we can apply the Smyth-Plotkin basic lemma directly on $F^e$ (because every continuous functor satisfies the conditions of the lemma).
2. **Mixed-variant functors:** The second reason we don't use directly the basic lemma is that it ony applies to covariant functors. Therefore, the basic lemma can not be applied to mixed variant functors, such as the "arrow" one, or more generally functors of the form $F: {\bf D}^{op} \times {\bf D} \rightarrow {\bf D}$. It turns out that we can define a notion of local continuity that covers such functors. Then, it can be shown that we can define a functor $F^e: {\bf D}^{e} \times {\bf D}^{e} \rightarrow {\bf D}^{e}$, ie., a covariant functor in the category of embeddings. This functor is continuous and therefore the basic lemma is again applicable.

> **Comments:**
> **username_1**: Excellent answer, you should accept it :-)  
> **username_0**: Thanks for pressing me to work harder :-)  

---

