Email Gateway (May 05 2022 at 17:39): Email Gateway (May 05 2022 at 17:39):From: Wenda Li <wl302@cam.ac.uk>
Dear lifting-and-transfer experts,
I am considering to set up the lifting-and-transfer package for the topology type in “HOL-Analysis.Abstract_Topology”. This requires defining a “relator” to relate two topologies under some relation:
definition rel_topology:: "('a ⇒ 'b ⇒ bool) ⇒
'a topology ⇒ 'b topology ⇒ bool" where
"rel_topology R T1 T2 = undefined”
And this relator should ideally satisfy the following properties:
lemma rel_topology_eq [relator_eq]: "rel_topology (=) = (=)"
sorry
lemma rel_topology_mono [relator_mono]: "rel_topology A ≤ rel_topology B"
if le: "A ≤ B"
sorry
lemma rel_topology_distr [relator_distr]:
"rel_topology A OO rel_topology B = rel_topology (A OO B)"
sorry
definition topo_map::"('a ⇒ 'b) ⇒ 'a topology ⇒ 'b topology" where
"topo_map f T1 = undefined"
lemma Quotient_topology[quot_map]:
assumes "Quotient R Abs Rep T"
shows "Quotient (rel_topology R) (topo_map Abs) (topo_map Rep) (rel_topology T)"
sorry
I have been attempting to imitate the lifting setup for filters:
definition map_filter_on :: "'a set ⇒ ('a ⇒ 'b) ⇒ 'a filter ⇒ 'b filter" where
"map_filter_on X f F = Abs_filter (λP. eventually (λx. P (f x) ∧ x ∈ X) F)”
inductive rel_filter :: "('a ⇒ 'b ⇒ bool) ⇒ 'a filter ⇒ 'b filter ⇒ bool" for R F G where
"rel_filter R F G”
if "eventually (case_prod R) Z" "map_filter_on {(x, y). R x y} fst Z = F" "map_filter_on {(x, y). R x y} snd Z = G”
because both ‘a topology and ‘a filter are constructed from ‘a set set but with different constraints. However, unlike filters it appears quite hard to define a map from one topology to another while satisfying the map compositionality as on filters:
lemma map_filter_on_comp: "map_filter_on X f (map_filter_on Y g F) = map_filter_on Y (f ∘ g) F"
if "g ` Y ⊆ X" and "eventually (λx. x ∈ Y) F"
I was wondering if it is at all possible to define a relator for the topology type.
Any hint or comment would be highly appreciated.
Best,
Wenda
Email Gateway (May 05 2022 at 17:50):From: Dominique Unruh <unruh@ut.ee>
Dear Wenda,
I had the same need recently, and I wrote the definition of
"rel_topology" (together with various transfer and parametricity
theorems) for it:
definition rel_topology :: ‹('a ⇒ 'b ⇒ bool) ⇒ ('a topology ⇒ 'b
topology ⇒ bool)› where
‹rel_topology R S T ⟷ (rel_fun (rel_set R) (=)) (openin S) (openin T)
∧ (∀U. openin S U ⟶ Domainp (rel_set R) U) ∧ (∀U. openin T U ⟶
Rangep (rel_set R) U)›
The first condition on the rhs says that the "openin" predictate relates
as one would expect.
However, that turned out to be insufficient (e.g., for proving
‹(rel_topology R ===> rel_set R) topspace topspace›). So I am
additionally requiring that the open sets are in the domain/range of the
underlying relation. (Your email is quite timely, I added this
correction yesterday evening! :) )
This definition seems to work (in the sense that I have managed to prove
various nontrivial transfer theorems, including for infinite sums w.r.t.
different topologies.
You can find the whole thing here:
(This is work in progress. But the part relating to rel_topology does
not have any sorry's as far as I can tell (since yesterday! :D). The
repo is a clone of the AFP but I think you can just extract the
Hilbert_Space_Tensor_Product directory on its own and it should work
with the normal release AFP.)
I have not tried to prove the lemmas you write below yet.
Best wishes,
Dominique.
Email Gateway (May 06 2022 at 11:05):From: Wenda Li <wl302@cam.ac.uk>
Dear Dominique,
Thanks a lot for your prompt reply! And I am so lucky to have you happen to think about the same problem :-)
Your definition of rel_topology is awesome, but I am afraid that with it we still cannot derive the monotonicity lemma: "A ≤ B ⟹ rel_topology A ≤ rel_topology B”.
My intention with the list of properties I described in the previous email is that we can then freely lift from the topology type similar to set/list:
typedef (overloaded) ('a, 'b) poly_inst ("(_ ⇒⇩p /_)" [1, 0] 0) =
"UNIV:: ('a ⇒ 'b) set"
by auto
setup_lifting type_definition_poly_inst
lift_definition PiE⇩p :: "'a set ⇒ ('a ⇒ 'b set) ⇒ ('a ⇒⇩p 'b) set" is
"λs f. PiE s f" .
text ‹This definition is only possible if we have @{thm Quotient_topology}›
lift_definition product_topology⇩p
:: "('a ⇒ 'b topology) ⇒ 'a set ⇒ ('a ⇒⇩p 'b) topology" is
"λf s. product_topology f s" .
Nevertheless, being able to prove this number of non-trivial transfer theorems is perhaps the best we can do for now...
Best,
Wenda
Email Gateway (May 06 2022 at 11:08):From: Lawrence Paulson <lp15@cam.ac.uk>
My own attempt at this was hopeless. If there is anyone out there who really has a good feel for how to define these things, it would be great if they could write a small tutorial…
Larry Paulson
Email Gateway (May 06 2022 at 13:07):From: Manuel Eberl <manuel@pruvisto.org>
I also failed miserably trying to define one for the "measure" type once.
I mean, I could define one that works for two types that are completely
isomorphic, but that's probably not as general as what we really want to
have.
Manuel
Email Gateway (May 08 2022 at 12:27):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Hi Wenda, Dominique and Manuel,
The first attempt at defining a relator for a type is usually to follow the structure of
the types it is built from. Joshua Schneider and I had an ITP paper on that topic a few
years ago: Relational parametricity and quotient preservation for modular (co)datatypes
http://dx.doi.org/10.1007/978-3-319-94821-8_24
For rel_topology, we'd get what was Dominique's first attempt:
rel_topology R S T = (rel_fun (rel_set R) (=)) (openin S) (openin T)
since openin is the representation morphism of type 'a set => bool. The above paper gives
sufficient conditions on when Wenda's desired properties are satisfied (especially section
5 on subtypes). However, rel_topology_mono will certainly not hold with this definition.
The reason is that the type variable 'a in 'a set => bool occurs in a negative position,
so this approach will yield a contravariant functor, for which the relator is anti-monotone:
R <= S ==> rel_topology S <= rel_topology R
Accordingly, you'd be looking for a contravariant map function for the quotient
preservation theorem.
Unfortunately, this approach sometimes does not give the right relator. For example, I
originally defined rel_filter following this approach:
https://isabelle.in.tum.de/repos/isabelle/annotate/5431e1392b14/src/HOL/Topological_Spaces.thy#l2285
However, this did not give the nice theorems for rel_filter that we have today in
Isabelle. As discussed at the end of Section 5 in the above paper, the current relator is
stronger and thereby eliminates some junk. In
https://isabelle.in.tum.de/repos/isabelle/rev/1d005f514417, I've switched out the old
definition for the new one.
In particular, the definition via a mapper gives the desired properties a lot more
directly than if we try to define the relator directly. So it may be worth to look for a
suitable map function (and decide whether it should be co- or contravariant).
On 06.05.22 15:07, Manuel Eberl wrote:
I also failed miserably trying to define one for the "measure" type once.
I can well imagine that.
'a measureconsists of the sigma algebrasetsand the measure
functionemeasure. Let's just look at the types:
sets :: "'a measure => 'a set set"
emeasure :: "'a measure => 'a set => ennreal"
Here, the type variable 'a occurs in sets in a positive position and in emeasure in a
negative position. This means that if we define the relator according to the types, we're
setup for failure. We get neither monotonicity nor anti-monotonicity and the mapper will
only work for isomorphism:
I mean, I could define one that works for two types that are completely isomorphic, but
that's probably not as general as what we really want to have.
One could try to get out of this problem via the isomorphism between sets and predicates.
If we understood the set to be measured as a predicate, i.e., the indicator function, then
all occurrences of 'a would be covariant again and there would be hope.
emeasure' :: "'a measure => ('a => bool) => ennreal"
This duality between sets and predicates w.r.t. co/contravariance was one of the main
reasons why we have re-introduces a separate type set for sets about 10 years ago. (In
2008, the set type constructor had been replaces as a type synonym: 'a set = 'a => bool)
Unfortunately, when a new definition is made involving sets or predicates, we typically do
not consider the co/contravariance aspect when we make a decision whether a parameter
should be a set or a predicate. We are mostly guided by the mathematical practice or
convenience of the notation. Of course, it's possible to define a relator on 'a set that
treats sets like predicates (see rel_pred in SPMF.thy), but that doesn't work well with
the transfer and lifting packages. They do not support several relators for a type, and
that's usually where my attempts in this direction have hit a wall. Proper support for
this duality would require a substantial rewrite of these packages.
I haven't yet thought about how a mapper or relator for topologies or measures could look
like. However, both topologies and measures typically consider only a well-behaved
functions (continuous or measurable) whereas the transfer and lifting packages always work
with the full function space, i.e., over the category SET. I don't know what complication
this brings along.
I hope that the above thoughts give you some inspiration where to look for solutions.
Andreas
Email Gateway (May 08 2022 at 17:32):From: Dominique Unruh <unruh@ut.ee>
Dear Wenda,
Your definition of rel_topology is awesome, but I am afraid that with it we
still cannot derive the monotonicity lemma: "A ≤ B ⟹ rel_topology A ≤
rel_topology B”.
I think that specific problem should be relatively easy to fix by replacing
"(rel_fun (rel_set R) (=)) (openin S) (openin T)" by "rel_set (rel_set R)
(Collect (openin S)) (Collect (openin T))". (I.e., we see the topology not
as a predicate over sets but a set of sets (which is anyway more in line
with usual language.) This would be monotonous.
However, that would not address the other lemmas you wanted.
I worked on it some more since your reply, and I think I have a much more
satisfactory approach.
Caveat: I have not formalized anything of what I write below in Isabelle. I
have handwritten proofs for the claims but they are not carefully checked
so the claims I am giving might not be correct. I am not including the
proofs in this email because is would take too long to write them in a
readable form. (But I can of course provide them if we need them.)
The first step was to define a map_topology function. I believe the
natural way to map topologies is the following (e.g. here
<https://en.wikipedia.org/wiki/Topological_space#Topological_constructions>):
For a surjective function [image: f:X\to Y], given a topology T on X, you
get a topology f(X) on Y by defining: [image: U\in f\left(X\right)] iff [image:
f^{-1}\in X].
However, the requirement that [image: f] is surjective is awkward in our
context because we do not want to add conditions in the various relator
theorems. So my solution is to [image: f\left(T\right)] be not a topology
on [image: Y] but a topology on [image: \text{im}f]. (I.e., with
topspace [image:
\text{im}f].) More precisely, for [image: f:X\to Y] we define [image:
\overline{f}] as follows:
[image: U\in\overline{f}\left(T\right)] iff [image:
f^{-1}\left(U\right)\cap\text{top}\left(T\right)\in T] and [image:
U\subseteq f\left(\text{top}\left(T\right)\right)].
(In Isabelle, we would write [image: \overline{f}] as *map_topology
f*.) ([image:
\text{top}\left(T\right)] denotes the topspace of [image: T].)
This construction has the following desired properties: [image:
\overline{\text{id}}=\text{id}]. [image: \overline{f\circ
g}=\overline{f}\circ\overline{g}]. [image:
\text{top}\left(\overline{f}\left(T\right)\right)=f\left(\text{top}\left(T\right)\right)].
If [image: f=g] on [image: \text{top}\left(T\right)], then [image:
\overline{f}\left(T\right)=\overline{g}\left(T\right)].
We can not define rel_topology. The idea how to do it is inspired by the
way relations on sets are lifted to relations on probability distributions
(e.g., in probabilistic relational Hoare logic). It is also similar to how
rel_filter is defined. The basic idea is to say that two topologies are
related (for some relation [image: R]) if there is a topology on pairs (I
call it the witness-topology) such that the witness-topology in a certain
sense satisfies [image: R] and the two topologies are the left/right
projection of the joint-topology. Specifically, we define:
For topologies [image: A,B], [image: \left(A,B\right)\in R] iff
[image:
\exists T^{\ast}.\ \ \ \text{top}\left(T^{\ast}\right)\subseteq R\ \
\wedge\ \ \ \overline{\text{fst}}\left(T^{\ast}\right)=A\ \ \ \wedge\ \
\overline{\text{snd}}\left(T^{\ast}\right)=B]
Concerning the properties you desired:
lemma rel_topology_eq [relator_eq]: "rel_topology (=) = (=)"
sorry
Holds. (Witness-topology for the [image: \Leftarrow]-direction is [image:
\overline{\text{double}}\left(A\right)] where [image:
\text{double}\left(x\right):=\left(x,x\right)].)
lemma rel_topology_mono [relator_mono]: "rel_topology A ≤ rel_topology B"
if le: "A ≤ B"
Holds trivially by definition.
lemma rel_topology_distr [relator_distr]:
"rel_topology A OO rel_topology B = rel_topology (A OO B)"
I do not know whether it holds. It looks like a difficult one to me. Is it
an important property?
lemma Quotient_topology[quot_map]:
assumes "Quotient R Abs Rep T"
shows "Quotient (rel_topology R) (topo_map Abs) (topo_map Rep)
(rel_topology T)"
Holds. The proof is more involved. (Quotient involves a number of
properties, and for most of them one has to choose the witness-topology
suitably.) But if I am not mistaken, it all works fine with a bit of work.
[For my own reference: Quicknotes 2022, p.95–100.]
I think this is better than the definition that I am currently using. (The
definition I use right now works for my purposes, but it may not be
sufficient for other purposes. And since one cannot use two relators for
the same typo (I think), it would be good to have only one (good)
definition of *rel_topology *throughout all Isabelle theories.
So if you feel that this is worth pursuing, maybe we can coordinate further
off-list? (I would also like to avoid duplicating work if we both develop
lifting of topologies.)
Best wishes,
Dominique.
Last updated: Jul 15 2022 at 23:21 UTC