Curves

Stream: new members

[Nicolò Cavalleri]

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]

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]

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

[Kevin Buzzard]

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]

I think you would want both.

[Nicolò Cavalleri]

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]

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

[Nicolò Cavalleri]

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]

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]

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?

[Reid Barton]

What's it for?

[Nicolò Cavalleri]

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

[Reid Barton]

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

[Nicolò Cavalleri]

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

[Reid Barton]

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

[Nicolò Cavalleri]

Reid Barton said:

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

Sure

[Reid Barton]

since that seems to be the current convention for some reason

[Reid Barton]

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

[Reid Barton]

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]

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

[Nicolò Cavalleri]

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]

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

[Reid Barton]

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]

It's a question about bundling

[Reid Barton]

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

[Nicolò Cavalleri]

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]

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

[Reid Barton]

but it probably shouldn't be a point etc.

[Nicolò Cavalleri]

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]

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

[Reid Barton]

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]

and this is what I thought seemed not so useful

[Reid Barton]

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]

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

[Reid Barton]

I see

[Reid Barton]

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]

like

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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]

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

I don't know about this! What is codes?

[Reid Barton]

It's only cooler if it actually works

[Reid Barton]

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]

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]

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]

src/topology/subset_properties.lean L1056:

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

[Reid Barton]

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]

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

[Reid Barton]

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]

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]

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

[Reid Barton]

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

[Reid Barton]

hmm, maybe the -> direction is more awkward

[Kenny Lau]

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

[Nicolò Cavalleri]

Haha I did not find it with library search

[Nicolò Cavalleri]

Where is it

[Nicolò Cavalleri]

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]

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

[Kenny Lau]

is_connected_iff_connected_space

[Reid Barton]

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]

git grep is also a recommended way to find lemmas.

[Kenny Lau]

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

[Kenny Lau]

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

[Nicolò Cavalleri]

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]

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]

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

[Nicolò Cavalleri]

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

[Nicolò Cavalleri]

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]

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

[Reid Barton]

If it works for you, then OK.

[Patrick Massot]

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]

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