Infra-Domain Proofs 2

post by Diffractor · 2021-03-28T09:15:15.284Z · LW · GW · 0 comments

Contents

No comments

Lemma 7: For  s.t.  and , and , and  is compact, LHC, and second-countable, then . The same result holds for .

This is the only spot where we need that  is LHC and not merely locally compact.

Here's how it's going to work. We're going to use the details of the proof of Theorem 2 to craft two special functions  and  of a certain form, which exceed  and . Then, of course,  as a result. We'll then show that  can be written as the supremum of finitely many functions in  (or ) which all approximate , so , establishing that .

From our process of constructing a basis for the function space back in Theorem 2, we have a fairly explicit method of crafting a directed set of approximating functions for  and . The only approximator functions you need to build any  are step functions of the form  with  being a finite rational number, and  being selected from the base of , and  where  is our compact hull operator. Any function of this form approximates , and taking arbitrary suprema of them,  itself is produced.

Since functions of this form (and suprema of finite collections of them) make a directed set with a supremum of  or above ( or above, respectively), we can isolate a  from the directed set of basis approximators for , s.t. , because . And similarly, we can isolate a  which approximates  s.t. , because 

Now, it's worthwhile to look at the exact form of  and . Working just with  (all the same stuff works for ), it's a finite supremum of atomic step functions, so

and, by how our atomic step functions of the directed set associated with  were built, we know that for all i, . (remember, the  are selected from the base, so we can take the compact hull of them).

There's a critical split here between the behavior of the  type signature, and the  type signature. 

For the  type signature, there's finitely many i, and everything not in the  gets mapped to . Since , and  is compact,  is bounded below (Lemma 1), so for this finite supremum to exceed , the  must cover .

For the  type signature, again there's finitely many i, but we can't guarantee that the  cover , because everything not in some  gets mapped to 0, and  might not be bounded above 0. So, we'll add in a "dummy" step function . This is just the constant-0 function, which approximates everything, so nothing changes. However, it ensures that  is indeed covered by the open sets of the finite collection of step functions.

So... Given that we have our , what does the function  look like? Well, it looks like

We could do this in the  case from adding in the "dummy" open sets to get the  family and  family to both cover .

Anyways,  equals . There's finitely many i's and finitely many j's by how g and g' were built, so this is a supremum of finitely many atomic step functions. Since , if we can just show that all these atomic step functions are approximators for  in  (or ), then  (supremum of finitely many approximators is an approximator), and we'd show our desired result that . So let's get started on showing that, regardless of  and 

Now, if , then this function maps everything to  or 0, which trivially approximates . Otherwise, everything in  gets mapped to , and everything not in it gets mapped to  (or 0)

We know by our process of construction for this that  and , so let's try to work with that. Well, for the  case. The  case is a bit more delicate since we added those two dummy functions. We have:

The first strict inequality was because of what  and  were. Then, just move the constants in. For the first non-strict inquality, it's because of monotonicity for our compact hull operator, , so it has a smaller compact hull. Then the next inequality is just grouping the two infs, and we're finished.

At this point, the usual argument of "fix a directed set of functions ascending up to , for each patch of  you can find a function from your directed set that beats the value  on that spot, this gets you an open cover of , it's compact, isolate a finite subcover ie finitely many functions, take an upper bound in your directed set, bam, it beats the step function on a compact superset of its open set so it beats the step function, and the directed set was arbitrary so  is approximated by the atomic step function" from Theorem 2 kicks in, to show that the atomic step function approximates . Since this works for arbitrary , and there are finitely many of these, the finite supremum  approximates , and dominates , and we're done.

Now for the  case. This case works perfectly fine if our  pair has  and  being above 0. But what if our  has  being above 0, but our j index is picking that  "dummy" approximator? Or vice-versa. Or maybe they're both the "dummy" approximator.

That last case can be disposed of, because  is just the constant-0 function, which trivially approximates everything. That leaves the case where just one of the step functions isn't the constant-0 function. Without loss of generality, assume  is paired with , but the other one is the  "dummy" approximator. Then our goal is to show that . This can be done because, since , and , we have

And the rest of the argument works with no problems from there.

 

Lemma 8: If , and , then , provided  lies in the function space of interest.  (or ), and  is compact, LHC, and second-countable.

By our constructions in Theorem 2, we can always write any function as the supremum of atomic step functions below it, , as long as . Since , we can find finitely many atomic step functions  which all approximate  s.t. the function  exceeds . In the  case, since the finite supremum exceeds , which is bounded below by Lemma 1, the  family covers .

Now, consider the finite collection of atomic step functions . If we can show that all of these approximate , and the supremum of them is larger than , then, since the supremum of finitely many approximators is an approximator, we'll have shown that , establishing approximation. So, let's show those. For arbitrary , we have 

So these atomic step functions all approximate . For exceeding , we have, for arbitrary ,

And so, our result follows. It's possible that, for the  case,  lies in no , but then the supremum of the empty set would be 0, and since the supremum of the  exceeds  as well, so the same inequality holds.

 

Lemma 9: If  and  with  with  being compact, LHC, and second-countable, then .

We can invoke Theorem 2, to write any function as the supremum of atomic step functions below it, , as long as . Since , we can find finitely many atomic step functions  which all approximate  s.t. the function  exceeds . Also,  is bounded below by Lemma 1, so the finite family  covers the entire space.

Now, consider the finite collection of atomic step functions . If we can show that all of these approximate , and the supremum of them is larger than , then, since the supremum of finitely many approximators is an approximator, we'll have shown that , establishing approximation. So, let's show those. For arbitrary , we have 

So these atomic step functions all approximate . For exceeding , we have, for arbitrary ,

And so, our result follows.

 

Lemma 10: If  and  with  with  being compact, LHC, and second-countable, then for all , as long as  is also bounded in .

By Theorem 2, we can always write any function as the supremum of atomic step functions below it, , where . Since , we can find finitely many atomic step functions  which all approximate  s.t. the function  exceeds .

Now, consider the following finite finite collection of atomic step functions. , along with 

If we can show that all of these approximate , and the supremum of them is larger than , then, since the supremum of finitely many approximators is an approximator, we'll have shown that , establishing approximation. So, let's show those. 

For arbitrary , if , then we have

So these atomic step functions all approximate . If , then the atomic step function turns into , which also approximates .

For the one extra step function we're adding in, we have two possible cases. One is where , the other one is where . In such a case, the function turns into c_{0}, which trivially approximates . However, if , then we have

For any , so this constant strictly undershoots the minimal value of  across the whole space, and thus approximates  by Lemma 2.

So, this finite collection of functions has its supremum being an approximator of . Now for showing that the supremum beats . If  lies in some , then

And we've shown that this supremum of step functions beats our new function. If  lies in none of the , then the original supremum of step functions must have mapped  to 0, and that beats , so . That's the only possible thing that could have happened. Then

So, this case is taken care of too, and our supremum of step functions beats . The lemma then finishes up, we have that  implies that for any  and  s.t.  and  and  all lie in , we have 

NOW we can begin proving our theorems!

 

Theorem 4: The subset of  (or ) consisting of inframeasures is an -BC domain when  is compact, second-countable, and LHC.

This proof will begin by invoking either Corollary 1 or Proposition 6. Since locally hull-compact implies locally compact, we can invoke these, to get that , or  is an -BC domain with a top element.

Then, if we can just show that the set of inframeasures is closed under directed suprema and arbitrary nonempty infinima, we can invoke Theorem 3 to get that the space of -inframeasures (or -inframeasures) is an -BC domain. This is the tricky part.

For our conventions on working with infinity, we'll adopt the following. 0 times any number in  is 0. Infinity times any number in  is infinity. Infinity plus any number in  is infinity. Given two functions  bounded below, then  is the function which maps  to , which is always continuous when  are, due to being monotone, and preserving directed suprema. The distance between points in , for defining the distance between functions as  is the usual distance when both numbers are finite, 0 when both numbers are  and  when one point is  and the other isn't.

An inframeasure is a function in  or  with the following three properties.

 should be 1-Lipschitz, it should map the constant-0 function  to 0 or higher, and it should be convex.

The definition of 1-Lipschitzness is that, using using our convention for the distance between points in  and the distance between functions , we have that for any two functions, .

The definition of concavity is that, for all ,,

Admittedly, this might produce situations where we're adding infinity and negative infinity, which we haven't defined yet, but this case is ruled out by Lemma 3 and Lemma 1. Any function has a finite lower bound by Lemma 1, and Lemma 3 steps in to ensure that they must have a finite expectation value according to . So, we'll never have to deal with cases where we're adding negative infinity to something, we're working entirely in the realm of real numbers plus infinity.

Now, let's get started on showing that the directed supremum of 1-Lipschitz, concave functions which map 0 upwards is 1-Lipschitz, concave, and maps 0 upwards.

Let's start with 1-Lipschitzness. In the case that our functions  have a distance of infinity from each other, 1-Lipschitness is trivially fulfilled. So we can assume that  have a finite distance from each other. Observe that it's impossible that (without loss of generality)  is infinity, while  is finite. This is because we have

So, if that first term is infinite, we can find  which map  arbitrarily high. And then  would only be a constant away, so the  values would climb arbitrarily high as well, making  be infinite as well. Then we'd have

And this would also show 1-Lipschitzness. So now we arrive at our last case where  is finite and the directed suprema are both finite. Then we'd have

and we're done. That was just unpacking definitions, and then the  was because we can upper-bound the distance between the suprema of the two sets of numbers by the maximum distance between points paired off with each other. Then just apply 1-Lipschitzness at the end.

As for concavity, it's trivial when p=0 or 1, because then (for  as an example)

So now, let's start working on the case where  isn't 0 or 1. We have

First equality is just unpacking definitions. Second equality is because, if the directed supremum is unbounded above, multiplying by a finite constant and taking the directed supremum still gets you to infinity, and it also works for the finite constants. Then, we observe that for any  chosen by the first directed supremum and  chosen by the second, we can take an upper bound of the two to exceed the value. Conversely, any particular  can be used for both directed suprema. So we can move the directed suprema to the outside. Then we just apply concavity, and pack back up.

Finally, there's mapping 0 to above 0. This is easy.

All these proofs work equally well with both type signatures, so in both type signatures, the set of inframeausures is closed under directed suprema.

Now we'll show they're closed under unbounded infinima. This is the super-hard part. First up, 1-Lipschitzness.

1-Lipschitzness is trivial if , so we can assume that this value is finite. It's also trivial if , because then the distance is 0. So we can assume that one of these values is finite. Without loss of generality, let's say that . Then, we can go:

Via Lemma 3. Now, at this point, we're going to need to invoke either Lemma 5 for the  case, or Lemma 6 for the  case. We'll treat the two cases identically by using the terminology . In the  case, this is just , because the functions  have a finite lower bound via compactness/Lemma 1, and we're in the assumed case where . In the  case, it's , which is a different sort of function. Anyways, since we have , this then means that  by Lemma 5 or 6 (as the type signature may be). So, swapping out the supremum over  with choosing a  and evaluating the , makes that second directed supremum go down in value, so the value of the equation as a whole go up. So, in both cases, we have

The starting inequality was already extensively discussed. Then, the shift to the absolute value is because we know the quantity as a whole is positive. The gap between the two suprema is upper-bounded by the maximum gap between the two terms with the same  chosen. Similarly, the gap between thetwo infinima is upper-bounded by the maximum gap between the two terms with the same  chosen. Then we just do a quick conversion to distance, and apply 1-Lipschitzness of all the  we're taking the infinimum of. Continuing onwards, we have

Now, we've got two possibilities. The first case is where  has range in . In such a case, the latter term would turn into , so the contents as a whole of the absolute value would be . The second case is where  has range in . In such a case, the latter term would be as close or closer to  than , so we can upper-bound the contents of the absolute-value chunk by . In both cases, we have

And we're done, 1-Lipschitzness is preserved under arbitrary infinima, for both type signatures.

Now for concavity. Concavity is trivial when  or , so let's assume , letting us invoke Lemma 7. Let's show concavity. We have

The first equality was just unpacking via Lemma 3. Then we can move the constant in, group into a single big directed supremum, combine the infs (making the inside bigger), then apply concavity for all our . Now it gets interesting. Since  and  and  we have that  by Lemma 7. Since all possible choices make an approximator for , we can go...

And concavity is shown. The proof works equally well for both type signatures.

All that remains is showing that the constant-0 function maps to 0 or higher, which is thankfully, quite easy, compared to concavity and 1-Lipschitzness. This is automatic for the  case, so we'll just be dealing with the other type signature.

Remember our result back in Lemma 2 that if you have a constant function  where , then . We'll be using that. Also we'll be using Lemma 4 that no 1-Lipschitz function mapping  to 0 or higher can map a function  any lower than , which is finite, by Lemma 1. So, we have

And we're done. First equality was just the usual unpacking of infinite inf via Lemma 3, second one was because, if , then , so the function value goes down, and the third inequality was because none of the  can map  below  since . That's it!

Now, since the space of inframeasures (concave, 1-Lipschitz, weakly-normalized) is closed under directed sup and arbitrary inf in  and , we can invoke Theorem 3 to conclude that it makes an -BC domain.

 

Theorem 5: The following properties are all preserved under arbitrary infinima and directed supremum for both  and -inframeasures, if  is compact, second-countable, and LHC.

(supernormalization)

 (homogenity)

 (cohomogenity)

 (C-additivity)

 (crispness)

So, the deal with this proof is that the directed suprema part works equally well for both cases, but the arbitrary infinima part will need to be done once for the  type signature (where it's marginally easier), and done a second way for the  case, where it's considerably more difficult to accomplish.

First, .

Second, .

Third, .

Fourth, , which is trivial from second and third.

Fifth, supernormalization.

Sixth, homogenity.

Seventh, cohomogenity.

Eighth, C-additivity.

Ninth, crispness, which follows from six and eight since crispnes is equivalent to the conjunction of homogenity and c-additivity.

Now for arbitrary infinima in the  case. We'll note when the same proof works for the  case, and when we have to loop back later with a more sophisticated argument. Lemma 3 is used throughout.

First, preservation of  under infinima. We already know that, by  being preserved under arbitrary infinima it can't be below 0, so that leaves showing that it can't be above 0.

This was by monotonicity, since , and then we just apply that . This proof works for the  type signature.

Second, preservation of  under infinima. Since  when  via Lemma 2, we can go

And we're done. In order, that was unpacking the arbitrary inf, the inequality was because we swapped out for a more restricted class of approximators (value decreases), then we reexpressed , applied concavity (value decreases), distributed the inf in (value decreases), used that  always, and our assumption that  (value decreases), and then we can finish up easily. Same proof works just as well for the  type signature.

Third, preservation of  under infinima. Since  when  by Lemma 2, we can go

(

Due to monotonicity. Same proof works for the  type signature.

Fourth, preservation of  under infinima. This is trivial since we proved preservation of  and  under infinima already, for both type signatures.

For 5, supernormalization is that  for all numbers in  or  respectively. We'll show this is preserved under infinima. We have to prove both directions of this separately. In one direction, we have

Which establishes an upper bound. For a lower bound, we have, since  implies  by Lemma 2,

Now, for the  type signature, the only fiddly bit is the lower-bound argument, because maybe . In that case, you can just apply the fact that  is preserved under infinima, which we proved already.

Number 6: Homogenity, that for any . We only need to check , because for , it's saying that , which we've already shown is preserved under arbitrary infinima. This will work equally well for both type signatures.

And now, if , then . And similarly, if , then , by Lemma 8. So, we can switch to taking approximants of  itself and scaling them, because every approximant of , scaled  by , is an approximant of . And every approximant of , scaled by , is an approximant of . Due to this, we have

And then we can go, by homogenity,

And so, homogenity is preserved under arbitrary infinima, for both type signatures.

Seventh, preservation of cohomogenity under infinima. The condition is , for functions  s.t.  is lower-semicontinuous, and . This holds for  as well, in both type signatures, because then it's just , which we've already shown is preserved under arbitrary infinima.

This is exceptionally difficult to show in the  type signature, so we'll just show it for the  type signature for now and circle back to it at the end.

Now things get tricky. First, observe that if , then 

By appealing to Lemma 8, then 9. And then, adding  to both sides which preserves the approximation by Lemma 9, we'd have

And we can also get a converse to this. If , then, by Lemma 8,

And then, adding  to both sides with Lemma 9, we'd get

So, given that we can shift approximants back and forth between  and  freely, we can get

And then, since  rewrites as , we can go

(by cohomogenity) and then rewrite as

And we're done, cohomogenity has been proved to be preserved under arbitrary inf for the  type signature. The  proof is substantially trickier.

Eighth, preservation of C-additivity under infinima. The condition is  for all constants . Again, this is one we'll have to just prove for the  type signature, and not the  type signature, as that one takes more work to show. We can start with showing

Now, observe that if , then 

By adding a constant and appealing to Lemma 9. And we can also get a converse to this. If , then, by Lemma 9,

So, given that we can shift approximants back and forth between  and  freely, we can get

And C-additivity is preserved under arbitrary infinima.

That just leaves condition 9, preservation of crispness under infinima. Crispness is, for all . This is equivalent to the conjunction of C-additivity and homogenity, both of which are preserved under arbitrary infinima, so the same applies to crispness as well. Accordingly, we don't need to prove this a second time for , because it will follow for free when we prove that C-additivity is preserved under infinima in the  case.

Time for the two last difficult cases, showing preservation of cohomogenity under arbitrary infinima for the  type signature, and doing the same for C-additivity.

For cohomogenity, we want the following to be preserved under infinima.

for functions  s.t.  is lower-semicontinuous, and . What we'll do is just prove it for the case where  and  are both bounded above 0.

Once we get this case, we can consider making an arbitrarily small perturbation of our function  if one of those two conditions is violated, in order to apply the exact cohomogenity result, and then 1-Lipschitzness (applied to the arbitrary closeness of the perturbed function and the actual function) can be used to show that the cohomogenity equality comes arbitrarily close to holding since the equality holds exactly for the perturbation, so the equality also works for cases where one of the two functions may be 0 in places.

To do this, since the result is trivial for , we'll prove  if . Then we'll use concavity (preserved under arbitrary infinima) to get the other inequality direction, and show the cohomogenity equality if . Then we'll use further arguments to show that if the equality holds for , it also holds for .

So, assume , and we'll show one inequality direction of cohomogenity.

Observe that if , then

by Lemma 8. And then, applying Lemma 10,

Now, the important thing here is that  must be bounded above , otherwise  wouldn't be bounded above 0, which we're assuming. Then, since a possible approximator to  would be  (for sufficiently small  that still undershoots the lower bound of ), the directed supremum of approximators to  does contain some  s.t.  is never below 0 and thus is a legit function. Such a suitable  would be , because  would equal , which is strictly above 0 because  by assumption.

Thus, if we're taking the directed supremum of , we're guaranteed to have some functions  where, instead of having

as Lemma 10 says, we can replace it with

Because there are suitably high  s.t. the  lower bound never becomes relevant.

Anyways, after all these details, we can go

Because those things in  of the second line are a subset of all the stuff that approximates . Now, we can apply 1-Lipschitzness to get

And then rewrite a bit and apply cohomogenity for the  to get

And then, since we have 

but  can be arbitrarily small, we get

Which is one inequality direction of cohomogenity. But it's proved only for . Assuming , let's derive the other direction from concavity, known to be preserved under arbitrary infinima.

This is just rewriting things. Since we're assuming  is a suitable number to use for mixing things together so we can apply concavity. We apply concavity, yielding

Now, cohomogenity for the various  implies that . We know that  is preserved under arbitary inf, we proved it already. So we can rewrite our previous concavity line as

and then simplify to yield

And so we've derived

the other direction of the inequality. So cohomogenity holds for , and when the various functions are bounded away from zero. Now, using that it holds for , we'll prove it for arbitrary . Let  now. Then we can go

Deriving cohomogenity for the  case, because we can apply cohomogenity to  since that's above 1, and cohomogenity works in that case.

So cohomogenity is preserved overall under arbitrary infinima, as long as the functions are bounded away from 0. Then you can just use a limiting argument with the 1-Lipschitz constant to extend to functions that touch 0.

Time for our last piece, preservation of C-additivity under infinima. The condition is  for all constants . The way this will work is we'll show it for  (the  case is trivial), and then use that to show it for . So, assume 

Now, observe that if , then 

By adding a constant and appealing to Lemma 10. There are always approximants of this form above zero, because  so we can just take  to be sufficiently small. So, we get

By going to a smaller collection of approximants, then applying 1-Lipschitzness. Anyways, since  is arbitrarily small, we have

And to show equality, observe that if we had a strict > sign for some , we'd get a violation of 1-Lipschitzness, since  and  are only  distance apart, but our inframeasure (which is 1-Lipschitz) would have the two functions being more than  apart from each other.

Now that it's proven for , let's prove it for . We have

Because we can apply C-additivity to . Now it's proven in full generality.

That's the last of it, pretty much every nice condition we could ask for is preserved under finite suprema and arbitrary infinima.

 

Proposition 7: The functor mapping  to  and  to  is indeed a functor .

So, first-up, we already know that a space of inframeasures over an -BC domain is an -BC domain by Corollary 1 and Theorem 4 so the objects work out, we don't need to worry about this part.

Second, we'll need to show that  is indeed a legit inframeasure if  is.

Third, we'll need to show that  is not just a function , it's also a continuous function, showing that said maybe-functor indeed maps morphisms  to morphisms .

And finally, we'll need to show that said maybe-functor preserves identity morphisms and morphism composition in order to show it's a functor.

Starting on that second part (first part is taken care of), the requirements for 

to be an inframeasure are Scott-continuity (monotone, and preserving suprema of directed subsets), 1-Lipschitzness, mapping the constant-0 function up, and concavity.

For monotonicity, if , then, by the definition of pushforward, and  being monotone (since it's an inframeasure), we have

And monotonicity of  is shown.

For preservation of directed suprema, letting  be a directed set of Scott-continous functions , we have

And we're done. The first equality was just reexpressing definitions, then we reexpress the function, use continuity of  to shift the directed suprema to the outside, and wrap the definition back up.

For 1-Lipschitzness of , we have

And this is shown. We just used definitions of pushforward, then 1-Lipschitzness of  and how distances between functions work, then one last inequality and everything works.

For mapping 0 above 0, we have

And finally, for concavity,

Where we used concavity of  for the inequality, and then definitions.

So, indeed,  is always a legit inframeasure.  and  was arbitrary, so this shows our functor always maps morphisms between domains to functions between inframeasures over domains. The various other properties like C-additivity and such can be shown if the reader wishes it, they're all pretty simple to show, if you want a more restricted version of this functor.

We do need to show that  is a continuous function to show that said maybe-functor maps morphisms to morphisms. So, we need monotonicity and preservation of directed suprema of inframeasures.

Assume . Then

And  was arbitrary, so

And thus,  is indeed a monotone function, regardless of . Time to show preservation of directed suprema. Let  be a directed set of inframeasures in . We have

First equality was using the definition of , second equality was using that  were continuous so their composition was continuous, and how directed suprema of continuous functions (the ) works. Then there's just a bit of reexpressing with the definition of , and writing it as a directed suprema of inframeasures. And  was an arbitrary continuous function  (or ), so we have

And thus,  is indeed continuous, since it preserves suprema of directed sets.

Now that we know it maps objects to objects and morphisms to morphisms, we need to check that said maybe-functor preserves identity morphisms and morphism composition.

For identity morphisms, we have

Now,  was arbitrary, so we have

And  was arbitrary, so we have . That's preservation of identity morphisms down. 

Now for preservation of composition. Let , and .

Since  was arbitrary, we have

And so, since  was arbitrary, we have

Therefore, the functor mapping spaces to their spaces of inframeasures, and functions to their pushforwards is indeed a functor.

 

Proposition 8: The "space of inframeasures" functor is locally continuous.

Inspired by Lemma 5.2.2 and Definition 5.2.3 from Abramsky, we must check local continuity of the functor. In particular, we must show that the function

is continuous. This is done by showing monotonicity and preservation of directed suprema. First up is monotonicity. If , then

That inequality in the middle was, because , then , and  is Scott-continuous, and all Scott-continuous functions are monotone. Since  was arbitrary, we have  and since  was arbitrary, we have , establishing monotonicity. 

Time for establishing preservation of directed suprema. Let  be a directed set of functions . Then

We use continuity of functions a few times here, like continuity of  to move the directed supremum out of the inside. Now, since  was arbitrary, we have

And, since  was arbitrary, we have

Which is precisely the continuity of the function which maps a function to its pushforward, and local continuity is established. This can be seen by using the notation  instead of , because then it's

Which is more clearly preservation of directed suprema of functions.

 

Proposition 9: The category of -BC domains is closed under lifting, ,,,, function space, strict function space, and bilimit.

We'll show that given three basic results, we can derive the entire theorem from results in Abramsky and stuff we've already proved. Our three basic results we'll need to show are that:

1: If  is an -BC domain, then  is bounded-complete and has a countable basis.

2: If  are -BC domains, then  is bounded-complete and has a countable basis.

3: If  are -BC domains, then   has a countable basis.

Assuming these three results work out, we can show the entire theorem, as follows.

For lifting, the table in Summary 3.2.6 indicates that lifting a continuous domain produces a continuous domain, so all that remains is showing bounded-completeness and the existence of a countable basis, to establish that lifting an -BC domain produces an -BC domain. (Our first thing we need to show)

For coalesced sum , the table in Summary 3.2.6 indicates that coalesced sum of continuous domains is a continuous domain, so all that remains is showing bounded-completeness and the existence of a countable basis to establish that coalesced sum of -BC domains is an -BC domain. (Our second thing we need to show)

For sum , because  and -BC domains are closed under lifting and coalesced sum, they're also closed under sum.

For product , Corollary 4.1.6 says that the category BC is cartesian-closed, so we at least know that  is a BC-domain. Then, Proposition 3.2.4.2 says that a basis for  is the product of the bases for  and . Both of these are countable, so  has a countable basis, and so it's an -BC domain.

For smash product  happens to be a retraction of . Just map all the  and  pairs in  to , and the  pairs to themselves. This is Scott-continuous, and the corresponding Scott-continuous section  is just the obvious injection.

-BC domains are closed under product. And, Proposition 4.1.3 says that BC-domains are closed under retracts, so we know that  is at least a BC-domain. All that remains to check is that  has a countable basis. This follows by Lemma 3.1.3, that the retraction of the countable basis for  is a basis for .

For function space, Proposition 4.1.5 says that the category of BC-domains is closed under function space, so we at least know that  is a BC-domain. Then, it has a countable basis (the third thing we need to show), so it's an -BC domain.

For strict function space,  happens to be a retraction of . Just map all the  to the function  which does the exact same thing but also maps  to . This is Scott-continuous, and the corresponding Scott-continuous section  is just the obvious injection. -BC domains are closed under function space, as we've shown. And, Proposition 4.1.3 says that BC-domains are closed under retracts, so we know that  is at least a BC-domain. All that remains to check is that  has a countable basis. This follows by Lemma 3.1.3, that the retraction of the countable basis for  is a basis for .

For bilimit, Proposition 4.1.6 says that bilimits of BC-domains are BC-domains, and the countability of the basis for the bilimit is taken care of by Theorem 3.3.11.1. And we're done! As long as we manage to prove the three missing pieces.

 

Missing piece 1: Try to prove that if  is an -BC domain, then  is bounded-complete and has a countable basis.

Given any two points , one of three cases occurs. First,  and  could both be . Second, without loss of generality, , and . Third, . Clearly, in the first case, the pairwise supremum exists, it's just . And in the second case, the pairwise supremum is just . In the third case, if , and there's an upper bound in , then the same upper bound exists in , and so we can get a supremum of  and  in , and then it remains a supremum in . This establishes bounded-completeness.

As for a countable basis,  is clearly countable. We'll show that it works as a basis. Given any 

Now,  approximates all , so this turns into

And then, we've got two possible cases. One is where . In this case,  isn't in the original , and can't be in the original basis, so the supremum just turns into  ie  and we're done with that case. In the other possible case, , so  is in the original . Obviously, this supremum is entirely of stuff below , so the supremum will be equal or less than . So our new proof target will be that

in order to show equality. So, let's begin. We have

Because  is continuous. Since, for any , we have , we've shown that  is a countable basis for . That's one part down.

Missing piece 2: Try to prove that if  are -BC domains, then  is bounded-complete and has a countable basis.

Given any two points , one of two cases occurs. First,  and  could both be in the same original domain, or they could be in different original domains. If there's an upper bound for  and , they must be in the same original domain, and then we can appeal to bounded-completeness of  or  (whichever one the two points are in) in order to find a suprema for the two. this establishes bounded-completeness.

As for a countable basis,  is clearly countable since the two sets we're unioning are countable. We'll show that it works as a basis. Given any , without loss of generality, we can assume that , because the same upcoming proof will work if . Then we have

Now, since  by assumption, the only thing in  which approximates  is , so we have

And then, we've got two possible cases. One is where . In this case, the only thing in  which approximates  is  itself, so we get

and we're done there. In the second case, . In this case, since  must be in  and approximate , we have

because  is continuous and we're done. The same proof works for points in , so since we have , we've shown that  is a countable basis for . That's the second part down.

Missing Piece 3: If  are -BC domains, then  has a countable basis.

This will rely on a proof very similar to a stage in our proof of Theorem 2. Our proposed basis for , given a countable basis for  and , is all the atomic step functions  where  and , and all finite suprema of such which exist. The atomic step functions are, if , then , and otherwise . So our task is now to show that . Clearly we have one direction of the inequality, that  matches or exceeds the supremum, since everything in there approximates  and thus is less than . So we'll focus on the other direction, showing that . This is doable by showing said result for all . So, let  be arbitrary in . We then have

This occurs because  is continuous, so . Then,  is a continuous function, so we can move the directed supremum out of the function. Then,  is continuous, so . For the final step, because , we have , so .

Now, we'll assume something for now, and loop back to prove it later. We'll assume that if , then . Assuming this works out, then for any choice of  and  from those two directed sets, since , we have , so . Accordingly, we can go

The first inequality happens because every  pair for the first two directed suprema corresponds to an atomic step function which approximates , but there may be other step functions which approximate . The second inequality happens because  is composed of atomic step functions which approximate , but also some other stuff. Then we just reexpress things a bit. Assuming this works out, then since  is arbitrary, it'd show the other inequality direction, that  and so, we'd have a countable basis for , showing it's an -BC domain.

We do, however, need to show our key intermediate result that 

First, assume . Then, in order to show that , we need to pick an arbitrary directed set of functions, , with a supremum above , and show that there's a function in that collection which lies above . This is pretty easy, actually. Pick a suitable directed set . We have , so, we have

because of our starting assumption that , and  being a directed collection of functions which matches or exceeds . Now, by the fact that  approximates , and the directedness of the , there's an element of that which exceeds , which corresponds to some particular function . We have 

Now, we just need to show  and we'll have shown that for any directed set of functions with supremum above , it has a function which exceeds , and we'll be done. Let  be arbitrary. We can split into two cases. One is , and one is . In the first case, we have

Because of how the atomic step function was defined, and we showed that  already, and also since , we have  and Scott-continuous functions (like ) are monotone. For the second case, we have

And we're done, we hit all our proof targets, the theorem follows now.

0 comments

Comments sorted by top scores.