Stream: new members

Topic: Curves

Nicolò Cavalleri (Aug 22 2020 at 09:10):

I'd like to define curves in topology. I wish I could treat at the same time the case where the domain is any interval (close open, half close half open) as people often do in maths. My idea is to define a curve from a connected subset of the reals to the target space, so that I can give as an input every interval I want. However I do not really understand the details of the coercions between sets and subtypes, so I am not really sure this idea is feasible. Will Icc and Ioo be recognized as subsets? Does anyone see any other drawback with this approach / has suggestions?

Nicolò Cavalleri (Aug 22 2020 at 09:56):

I guess a disadvantage of this is that one has to require connectedness as a field of the structure. Why not making a class : Prop for connected and compact similarly to what they did for path_connected_space?

class connected (α : Type*) [topological_space α] : Prop :=
(connected : is_connected (univ : set α))


Nicolò Cavalleri (Aug 22 2020 at 10:14):

(Is example : is_connected (Icc (0 : ℝ) 1) := by library_search! really not in mathlib? or am I doing something wrong?)

Kevin Buzzard (Aug 22 2020 at 10:19):

It's not so clear that one would want such a result in a library, is it? Perhaps something about Icc a b if a<=b but I'm not sure library_search would then find what you're asking

Scott Morrison (Aug 22 2020 at 10:23):

I think you would want both.

Nicolò Cavalleri (Aug 22 2020 at 10:24):

Kevin Buzzard said:

It's not so clear that one would want such a result in a library, is it? Perhaps something about Icc a b if a<=b but I'm not sure library_search would then find what you're asking

I tried also with a b but no luck! Well I thought it would be there because it is the first example that comes to my mind of something connected!

Reid Barton (Aug 22 2020 at 10:25):

src/topology/algebra/ordered.lean:lemma is_preconnected_Icc : is_preconnected (Icc a b) :=


Nicolò Cavalleri (Aug 22 2020 at 10:27):

Reid Barton said:

src/topology/algebra/ordered.lean:lemma is_preconnected_Icc : is_preconnected (Icc a b) :=


Ok thanks! I guess to prove it is connected one just needs to add the hypothesis a \leq b

Nicolò Cavalleri (Aug 22 2020 at 10:28):

Kevin Buzzard said:

It's not so clear that one would want such a result in a library, is it? Perhaps something about Icc a b if a<=b but I'm not sure library_search would then find what you're asking

I think it should definitely be in the library! Why do you think not?

Nicolò Cavalleri (Aug 22 2020 at 10:30):

Nicolò Cavalleri said:

I guess a disadvantage of this is that one has to require connectedness as a field of the structure. Why not making a class : Prop for connected and compact similarly to what they did for path_connected_space?

class connected (α : Type*) [topological_space α] : Prop :=
(connected : is_connected (univ : set α))


@Reid Barton @Scott Morrison what do you think of this class?

What's it for?

Nicolò Cavalleri (Aug 22 2020 at 10:30):

To not look for the hypothesis of connected things every time and for consistency with path_connected_space

Reid Barton (Aug 22 2020 at 10:31):

I don't have anything against classes like this (I added compact_space for example)

Nicolò Cavalleri (Aug 22 2020 at 10:31):

In the case of path_connected you have both is_path_connected and path_connected_space and it looks great to me

Reid Barton (Aug 22 2020 at 10:31):

If you have a purpose for it, then sure. Probably it should be called connected_space though

Nicolò Cavalleri (Aug 22 2020 at 10:32):

Reid Barton said:

If you have a purpose for it, then sure. Probably it should be called connected_space though

Sure

Reid Barton (Aug 22 2020 at 10:32):

since that seems to be the current convention for some reason

Reid Barton (Aug 22 2020 at 10:32):

Returning to the original question, I'm not sure exactly what definition you have in mind or what it's for

Reid Barton (Aug 22 2020 at 10:34):

I'd think that, rather than just having "a continuous(?) map from some sort of interval to X", you'd want to know specifically what interval you're working with

Reid Barton (Aug 22 2020 at 10:34):

and at that point, you're just talking about a bundled continuous map at most

Nicolò Cavalleri (Aug 22 2020 at 10:34):

Reid Barton said:

Returning to the original question, I'm not sure exactly what definition you have in mind or what it's for

Well the final purpose is defining complete vector fields. For this I need curves on manifolds and for this I need curves in topological spaces

Reid Barton (Aug 22 2020 at 10:35):

but don't you want curves indexed on some specific $(a, b)$ or $(0, \varepsilon)$ or something

Reid Barton (Aug 22 2020 at 10:35):

I think this is a case where we have a word in math that isn't really useful for formalization, but maybe you have a use I don't know about

Reid Barton (Aug 22 2020 at 10:36):

Why don't you just write explicitly here the kind of definition you have in mind?

Nicolò Cavalleri (Aug 22 2020 at 10:37):

Reid Barton said:

but don't you want curves indexed on some specific $(a, b)$ or $(0, \varepsilon)$ or something

The point is that the velocity of a curve makes sense no matter if the interval is open or closed etc so I don't want to call curves just curves on open intervals or close intervals

Reid Barton (Aug 22 2020 at 10:37):

the domain doesn't even have to be connected then?

Reid Barton (Aug 22 2020 at 10:37):

but it probably shouldn't be a point etc.

Nicolò Cavalleri (Aug 22 2020 at 10:39):

Reid Barton said:

Why don't you just write explicitly here the kind of definition you have in mind?

@[reducible] def curve (α : set ℝ) [connected α] (β : Type*) [topological_space β] :=
continuous_map α β


Reid Barton (Aug 22 2020 at 10:40):

Right, so this is what I'm saying we have already and there is no need to also call it a "curve".

Reid Barton (Aug 22 2020 at 10:41):

I thought you wanted something like

structure curve (b : Type*) [topological_space b] :=
(a : set R)
(h : connected a)
(f : continuous_map a b)


Reid Barton (Aug 22 2020 at 10:42):

and this is what I thought seemed not so useful

Reid Barton (Aug 22 2020 at 10:48):

About your curve, I'm not sure what concretely you expect to gain from making this definition. You'll still have to repeat the hypotheses (α : set ℝ) [connected α]  everywhere you use curve, and then you could just write continuous_map instead of curve.

Nicolò Cavalleri (Aug 22 2020 at 10:50):

Well in the topology case I actually do not have any particular reason, in the smooth case it's just to have a curve namespace to write things like curve.speed and use the . notation

I see

Reid Barton (Aug 22 2020 at 10:56):

If you want to make a new type curve for the purpose of . notation, and maybe you have other stuff to include in a structure anyways, maybe it makes sense to bundle the connected hypothesis on α in that structure too, but not the type α itself

Reid Barton (Aug 22 2020 at 10:56):

like

structure curve' (a : set R) (b : Type*) [topological_space b] :=
(h : connected a)
(f : continuous_map a b)
-- ... maybe more stuff ...


Reid Barton (Aug 22 2020 at 10:56):

then you don't have to rely on instance search to find the connected hypothesis in your lemmas

Reid Barton (Aug 22 2020 at 10:57):

but you could make a constructor that still uses typeclass search if you wanted to, or you could decide it's not really necessary after all

Reid Barton (Aug 22 2020 at 10:58):

By the way, it might also be nice to have an inductive type with "codes" for all intervals, so you didn't have to rely on this somewhat indirect connected

Nicolò Cavalleri (Aug 22 2020 at 10:58):

Reid Barton said:

then you don't have to rely on instance search to find the connected hypothesis in your lemmas

Why do you think this is better though? Since a curve (I mean this kind of curves, for complete vector fields) will always be defined on an interval, it's cooler if Lean automatically checks the interval is connected without me having to tell it where to find the proof!

Nicolò Cavalleri (Aug 22 2020 at 10:59):

Reid Barton said:

By the way, it might also be nice to have an inductive type with "codes" for all intervals, so you didn't have to rely on this somewhat indirect connected

Reid Barton (Aug 22 2020 at 10:59):

It's only cooler if it actually works

Reid Barton (Aug 22 2020 at 11:00):

For example, there cannot be an instance for is_connected (Icc a b) because it needs a hypothesis a <= b, but <=isn't a class and the proof of a <= b can't be recovered from just knowing Icc a b.

Reid Barton (Aug 22 2020 at 11:02):

Nicolò Cavalleri said:

What is codes?

I just mean creating an inductive type

inductive interval
| Icc (a b) : interval
| Ioc (a b) : interval
| Ioi (a) : interval
...


and then defining the interpretation as a set.

Reid Barton (Aug 22 2020 at 11:04):

then if you like you can even make that interpretation into a coercion to sort, and write (i : interval \R) (s t : i), etc.

Kenny Lau (Aug 22 2020 at 11:04):

class connected_space (α : Type u) [topological_space α] extends preconnected_space α : Prop :=
(to_nonempty : nonempty α)


Reid Barton (Aug 22 2020 at 11:06):

I expect with these codes that there would be some disagreement about exactly what or what does not qualify as an interval, though...

Reid Barton (Aug 22 2020 at 11:08):

I mean, I'm not even sure I would agree with myself on the topic :upside_down:

Reid Barton (Aug 22 2020 at 11:11):

For example: should we include a hypothesis a <= b in the Icc constructor to make sure the interval is nonempty; does a point count as an interval.

Nicolò Cavalleri (Aug 22 2020 at 16:21):

I'd still would like to register an instance of Icc as a connected_space but to do this I need to prove that a subset is connected iff it is connected as a space, and I have a problem converting elements of set set a into elements of set a.
How am I supposed to go on with a proof like this?

lemma is_connected_univ (α : Type*) [topological_space α] (s : set α) :
is_preconnected s ↔ is_preconnected (univ : set s) :=
begin
split,
{
unfold is_preconnected,
rintro h u v ⟨w, hw, rfl⟩ ⟨z, hz, rfl⟩ h1 ⟨⟨a, ha⟩, ⟨⟩, h2⟩ ⟨⟨b, hb⟩, ⟨⟩, h3⟩,
have h3 := h z w hz hw, -- need to transform h1 to put it here...
simp only [mem_preimage, subtype.coe_mk, univ_inter] at *,
},
{ }
end


Reid Barton (Aug 22 2020 at 16:21):

rather than do it this way, we should have some lemma like the image of a connected set is connected

Reid Barton (Aug 22 2020 at 16:22):

that would handle the <- direction (apply to subtype.val)

Reid Barton (Aug 22 2020 at 16:23):

hmm, maybe the -> direction is more awkward

Kenny Lau (Aug 22 2020 at 16:26):

we do have the theorem that a subset is connected iff it is connected

Nicolò Cavalleri (Aug 22 2020 at 16:32):

Haha I did not find it with library search

Where is it

Nicolò Cavalleri (Aug 22 2020 at 16:32):

Kenny Lau said:

we do have the theorem that a subset is connected iff it is connected

You are basically the ultimate version of library search haha

Reid Barton (Aug 22 2020 at 16:33):

Actually, the ultimate version of library search is reading the library

Kenny Lau (Aug 22 2020 at 16:36):

is_connected_iff_connected_space


Reid Barton (Aug 22 2020 at 16:37):

If you want to know what is in the library about connected sets, why not read the whole section where connected sets are defined? It's only 360 lines and it will answer all subsequent questions of this form.

Reid Barton (Aug 22 2020 at 16:37):

git grep is also a recommended way to find lemmas.

Kenny Lau (Aug 22 2020 at 16:43):

I just wrote #check connected (and then reset the cursor by pressing escape) and then press Ctrl+space

Kenny Lau (Aug 22 2020 at 16:43):

then it gives you a bunch of lemmas with the name connected

Nicolò Cavalleri (Aug 22 2020 at 17:27):

Ok sorry I actually did not even know a class which is proposition valued could be treated as a normal proposition in iff lemmas so I did not think such a lemma could exist.

Nicolò Cavalleri (Aug 22 2020 at 17:29):

Reid Barton said:

For example, there cannot be an instance for is_connected (Icc a b) because it needs a hypothesis a <= b, but <=isn't a class and the proof of a <= b can't be recovered from just knowing Icc a b.

All the same this should not be a problem with fact: I was thinking to something like this

lemma is_connected_Icc {a b : ℝ} (h : a ≤ b) : is_connected (Icc a b) :=
⟨⟨a, by {simp only [left_mem_Icc], exact h}⟩, is_preconnected_Icc⟩

@[reducible] def curve (α : set ℝ) [connected_space α] (β : Type*) [topological_space β] :=
continuous_map α β

instance some_other_name {a b : ℝ} [h : fact (a ≤ b)] : connected_space (Icc a b) := is_connected_iff_connected_space.1
(is_connected_Icc h)

noncomputable def a : curve (Icc 0 1) (ℝ × ℝ) :=
⟨λ x, (x, x), continuous_induced_dom.prod_mk continuous_induced_dom⟩


Nicolò Cavalleri (Aug 22 2020 at 17:29):

I mean this is in the topology case but I think of something like this for geometry

Nicolò Cavalleri (Aug 22 2020 at 17:30):

I take it that there is no point in defining curves in topology, it is just to illustrate my point

Nicolò Cavalleri (Aug 22 2020 at 17:32):

The geometry library already treats [a, b] as a manifold with corners by making use of fact so there should be no problem to use it further: the user already has to use it there

Reid Barton (Aug 22 2020 at 17:32):

I don't really know what the story with the fact class is but it sounds more complicated than what I suggested.

Reid Barton (Aug 22 2020 at 17:32):

If it works for you, then OK.

Patrick Massot (Aug 22 2020 at 17:39):

Nicolò Cavalleri said:

Ok sorry I actually did not even know a class which is proposition valued could be treated as a normal proposition in iff lemmas so I did not think such a lemma could exist.

Remember this whole class business is only about inferring arguments that you don't provide. It doesn't change the type of anything. If connected_space X : Prop then it's a Prop.

Nicolò Cavalleri (Aug 23 2020 at 11:01):

Another idea that works particularly well in Lean, modeled on the idea of local_equiv, would be to define a curve to be a continuous / smooth function from $\R$ to the target space / manifold and only care about its values on a source subset. This would be perfect to define an order relation on curves to define maximal curves. The problem with this however is that this breakes extensionality. I see that in the case of local equivalences extensionality requires that the two equivalences have same source, fun and inv_fun, which is not ideal. In the case of curves one would want two curves to be equal if they are the same only on their sources, and this is important for the order relation. One way to achieve this is to require that the target space be inhabited and require that the curves takes the default value on points not in the source, so to save extensinoality the way I want it. If someone else has better ideas to get the right extensionality however I am happy to hear them

Last updated: May 08 2021 at 09:11 UTC