Continuous maps

Stream: new members

[Nicolò Cavalleri]

Is there any particular reason why continuous maps are defined with def instead of being a structure such as linear maps? I am asking because when working with smooth maps I realize that if they were defined as a structure and smooth maps could be defined as a structure extending continuous maps, everything would be way more natural and smooth (no PUN intended!)

[Heather Macbeth]

I asked a related question about bounded continuous functions a couple of months ago. To summarize @Sebastien Gouezel and @Yury G. Kudryashov's answers there, indeed maybe it should be a structure, but this refactor is low priority.

[Nicolò Cavalleri]

Ok thanks! I guess it is too late to change it?

[Heather Macbeth]

I would also be curious to know!

[Nicolò Cavalleri]

I mean Sebastien plans to define smooth functions between manifolds as

def times_cont_mdiff (n : with_top ℕ) (f : M → M') :=
continuous f ∧ other_stuff

At this point I am not really sure If I should define a diffeomorphism as a structure extending a homeomorphism which would therefore require twice a proof that the map is continuous (I mean it'd be fine but dirty) or more basically as

structure diffeomorph extends M ≃ M' :=
(smooth_to_fun  : smooth I I' to_fun)
(smooth_inv_fun : smooth I' I inv_fun)

and then manually define all the coercions to homeomorphisms (more clean but more work)

PS.: smooth is an abbreviation for times_cont_mdiff \top

[Reid Barton]

Do you mean changing continuous to a structure, but leaving it still a Prop?

[Reid Barton]

Or making a structure with two fields?

[Nicolò Cavalleri]

Reid Barton said:

Do you mean changing continuous to a structure, but leaving it still a Prop?

No I'd make it a structure with two fields but I understand it requires a lot of work to change the library this way

[Nicolò Cavalleri]

Would it be to bad to leave it as it is and define a structure

structure continuous_map {α : Type*} {β : Type*} [topological_space α] [topological_space β] :=
(to_fun : α → β)
(continuous : continuous to_fun)

So that all these definitions can be given more cleanly?

[Nicolò Cavalleri]

I mean having both things living in mathlib?

[Reid Barton]

That actually already exists though it is a def and in a funny place.

[Nicolò Cavalleri]

Reid Barton said:

That actually already exists though it is a def and in a funny place.

You mean the name continous_map is already taken?

[Nicolò Cavalleri]

Or the structure exists?

[Reid Barton]

docs#continuous_map

[Nicolò Cavalleri]

Does that work for what I was saying? I mean writing the definition of smooth map as a structure extending a continuous map?

[Nicolò Cavalleri]

If it is just about the name I guess another name can be found for the structure

[Reid Barton]

You can't literally extend it because it is a def but there is no reason that it could not change to a structure.

[Reid Barton]

However, it would still be unused outside of this one file (which states theorems which cannot be formulated without it).

[Nicolò Cavalleri]

Reid Barton said:

However, it would still be unused outside of this one file (which states theorems which cannot be formulated without it).

What about making it a structure and moving it to topology.basic and then use it in geometry as well?

[Nicolò Cavalleri]

I mean I guess my question can be made more general as, why when implementing a concrete category in mathlib, sometimes morphisms are formalized as structure with a to_fun field and sometimes as properties with a true/false value? Is there a specific reason why a uniform choice was not taken?

[Reid Barton]

Historical reasons and/or experience

[Nicolò Cavalleri]

Nicolò Cavalleri said:

Reid Barton said:

However, it would still be unused outside of this one file (which states theorems which cannot be formulated without it).

What about making it a structure and moving it to topology.basic and then use it in geometry as well?

Ok what do you think of this?

[Reid Barton]

I mean, I'm not thinking about it very hard, but it doesn't seem worth it if the goal is to save 4 lines of copying the information that a function is continuous somewhere

[Reid Barton]

It sounds like you already have at least one perfectly satisfactory option

[Yury G. Kudryashov]

Continuous functions should not be bundled because usually continuity is not the main property of a function

[Reid Barton]

I think it's pretty likely that continuous has to exist as a Prop (even in a clean-slate redesign) whether or not you also use a name for a bundled continuous function.

[Reid Barton]

By the way, we also have a second form of bundled continuous functions, in category theory

[Nicolò Cavalleri]

Yury G. Kudryashov said:

Continuous functions should not be bundled because usually continuity is not the main property of a function

Can you say a bit more on this? I am not sure I understand what you mean?

[Nicolò Cavalleri]

Reid Barton said:

It sounds like you already have at least one perfectly satisfactory option

Which of the above two would you suggest then?

[Reid Barton]

I'm not in a position to suggest anything right now.

[Reid Barton]

Bundled fuctions are always more convenient if you don't know what the function is.

[Reid Barton]

But someone somewhere had to provide that bundled function and to do it they had to prove that some function is continuous, and it's probably too hard if they can't talk about continuous f : Prop.

[Nicolò Cavalleri]

Yeah I understand this! Indeed to me now the best option would be to have both and have continous and continous_map both in topology.basic, but if you say it's not worth it I just wonder if someone with more experience can suggest me what of the above two options is better at this point to define diffeomorphism

[Nicolò Cavalleri]

In any case it's not just to change those 4 lines but so to have also smooth maps as a structure and define those thousands of kinds of maps in geometry as structures extending smooth maps

[Nicolò Cavalleri]

I mean I had this issue with 4 maps already that are smooth maps also with other properties and I never know if it's better to repeat the proof that they are continous many times or if to do everything manually

[Yury G. Kudryashov]

What other types are you talking about?

[Yury G. Kudryashov]

I mean that continuous_map should not be the main interface for continuous maps because this way you'll need continuous_map.sin := ⟨sin, continuous_sin⟩ etc.

[Yury G. Kudryashov]

And you often create discontinuous functions from continuous functions (e.g., f / g).

[Yury G. Kudryashov]

However it's OK to deal with continuous_map (it should be redefined as a structure) when you study, e.g., the space of all continuous functions.

[Yury G. Kudryashov]

I think that diffeomorphism should be a bundled structure, cf. homeomorph.

[Yury G. Kudryashov]

Nicolò Cavalleri said:

Ok thanks! I guess it is too late to change it?

The only part of lean+mathlib that is "too late to change" is the core logic foundation. I'll be glad to review a PR that will move continuous_map to topology/basic or a dedicated file topology/continuous_map and redefine it using structure.

[Yury G. Kudryashov]

I mean, continuous_map is a much more rarely used definition than is_ring_hom was a year ago, and we almost migrated to bundled ring_homs.

[Nicolò Cavalleri]

Yury G. Kudryashov said:

I think that diffeomorphism should be a bundled structure, cf. homeomorph.

Yep sure I did define it like that (you can see above my definition), but I could have also defined it as

/-- α and β are homeomorph, also called topological isomoph -/
structure diffeomorph extends (homeomorph M M') :=
(smooth_to_fun  : smooth I I' to_fun)
(smooth_inv_fun : smooth I' I inv_fun)

[Nicolò Cavalleri]

And this way the proof that it is continuous has to be given twice

[Nicolò Cavalleri]

And it's totally fine but things can be done more cleanly if everything is also defined in terms of bundled maps

[Nicolò Cavalleri]

Yury G. Kudryashov said:

What other types are you talking about?

My point is that in geometry you can add a lot of structures to a manifold and then deal with morphisms that preserve those structures. I believe that for continuous maps and smooth functions it makes sense to have things defined both in terms of properties and bundled maps for the reason you said but at some points you start dealing with morphisms such as maps preserving a connection or any kind of structure and you care less about proving that a specific map has that property and treat things more as morphism just as for algebraic structure. And I believe it'd be very clean, if it is not too much of an effort, to have versions of bundled continuous maps and smooth maps and theorems proving things about them in such a way that whenever you add the nth structure on top of your manifold with (n-1) structures you just need to extend the morphisms you had and have automatic coercions

[Scott Morrison]

@Nicolò Cavalleri, have you looked at the category Top? That uses bundled continuous maps, and indeed allows you to simply write things like variables {X Y : Top} (f : X ⟶ Y) and that slightly-different-from-normal arrow means that f is automatically a continuous map.

[Nicolò Cavalleri]

I actually did look into Top but would you suggest using this version of the bundled map for geometry? It seemed to me that in Mathlib the style is to formalize things without category theory at first and then add category theory when things are already established (at least for maths that, possibly, can be done without too much category theory such as differential geometry)

[Kevin Buzzard]

That is true, but it might be a historical artefact

[Scott Morrison]

Yeah, I'm unsure. I am perfectly sympathetic to "no unnecessary category theory!" but the notation works out so nicely. :-)

[Kevin Buzzard]

We made topological rings in about 2017 and needed a gazillion facts about them in 2018 for the perfectoid project. Concrete categories didn't appear until 2019.

[Scott Morrison]

Until quite recently using the category theory library resulted in having to fight Lean, reminding it about universes all the time. This problem has gone away, so it's _much_ smoother to use.

[Kevin Buzzard]

And as Scott said, they are exactly the way to bundle morphisms.

[Nicolò Cavalleri]

I really like to use category theory from the beginning but the problem I see with that is that differential geometry is really necessary for physics and mathematical physics and developing it with category theory in the first place might make it less friendly for people that might not be very familiar with it

[Kevin Buzzard]

They bundle objects too. But I'm not sure this is really an issue. I would recommend you try categories. Progress is made through experimentation. The sad fact is that nobody knows the right way to do manifolds in a theorem prover

[Kevin Buzzard]

We had unbundled group homs in 2018 and bundled them in 2019

[Kevin Buzzard]

This question could have been asked 30 years ago but there was nobody to ask it

[Kevin Buzzard]

Try categories. They're better than ever before

[Kevin Buzzard]

And I speak as someone who has been very frustrated by previous iterations on more than one occasion

[Kevin Buzzard]

Bhavik Mehta and the other Cambridge people have had a very positive experience with them in their topos project

[Kevin Buzzard]

It will be a great test of the concrete category API

[Nicolò Cavalleri]

I can but the problem I have with categories now is that it seems to require way more work than just restating some theorems for continuous bundled maps and since I am doing all of this for a summer project at Cambridge to formalize some mathematical physics and we are already quite behind, I might just do things the way they were started and then come back to this after my project I guess

[Nicolò Cavalleri]

Also I'm from DPMMS but my colleagues are from DAMPT, so they might not enjoy too much if they need to study some category theory to work with the maths I formalize

[Nicolò Cavalleri]

Maybe I could define continuous bundled map in a file on my computer and prove just the things that I need so to do things cleanly on my computer closer to the style of category theory and then try later to convert it to category theory

[Kevin Buzzard]

I always used to call it DAMPT too :-)

[Nicolò Cavalleri]

Kevin Buzzard said:

I always used to call it DAMPT too :-)

Ops DAMTP haha

[Nicolò Cavalleri]

It's just that DAMPT is more easily pronounced haha

[Kevin Buzzard]

When you're just using category theory as a language, like you are (as a way to bundle morphisms) you won't need to learn any of the category theory language other than the way to compose morphisms. You will for example never need a functor. You will just need to learn the new way of saying "let X be a manifold" (which is easier than the old way, it's just X: Manifold) and how to move between the old way to the new way, which is easy with concrete categories. It is not a big ask for those DAMPTers.

[Kevin Buzzard]

You are literally just using it as a wrapper to bundle morphisms

[Nicolò Cavalleri]

Kevin Buzzard said:

When you're just using category theory as a language, like you are (as a way to bundle morphisms) you won't need to learn any of the category theory language other than the way to compose morphisms. You will for example never need a functor. You will just need to learn the new way of saying "let X be a manifold" (which is easier than the old way, it's just X: Manifold) and how to move between the old way to the new way, which is easy with concrete categories. It is not a big ask for those DAMPTers.

Yes sure I take it that it's not a lot to learn even though the problem of taking much more time to implement it subsists. The cool thing about not doing it with category theory is that I can use topology as a model to implement many things. Say that for example I need to implement diffeomorphisms or local_diffeomorphisms. I can just copy the files homeomorphism and local_homeomorphism, read them and keep all the lemmas (especially the simp ones) that make sense for diffeomorphisms, do a couple of replace, like homeo with diffeo and continuous with smooth, and voilà in 2 hours of work I have a pretty decent implementation of diffeomorphisms I can work with

[Yury G. Kudryashov]

AFAIK, one of the main reasons not to move to "categories everywhere" is that X ⟶ Y needs X and Y to be in the same universe, and @Mario Carneiro explains once a month that we should allow them to be in different universes because (some arguments I don't fully understand).

[Mario Carneiro]

You can use ulift in order to get around this, although it makes application a bit harder

[Yury G. Kudryashov]

The question is what is harder: use ulift where you need different universes or repeat lemmas like comp_assoc for every concrete category.

[Yury G. Kudryashov]

As a person who doesn't need different universes most of the time, I'd prefer to use ⟶.

[Mario Carneiro]

umm... comp_assoc is an axiom of categories. Category theory isn't giong to help you prove that

[Mario Carneiro]

I'm still waiting for an example of a theorem that category theory actually helps to make shorter

[Mario Carneiro]

That said, I don't think that there is a conflict here. We can have both

[Yury G. Kudryashov]

For me "using the same symbol and name for composition everywhere" is already a good reason.

[Yury G. Kudryashov]

What category/concrete_category gives for free: (a) End, Aut; (b) category from coe_fn + 2 or 3 rfls.

[Yury G. Kudryashov]

For me a good reason not to switch to categories is that now we have, e.g., mul_equiv that works for anything from semigroup to comm_group, and similarly for ring_equiv.

[Scott Morrison]

Mario Carneiro said:

I'm still waiting for an example of a theorem that category theory actually helps to make shorter

I'm pretty certain that if you include the "setting up the abstract nonsense" in your line count, this is never ever going to happen.

The purposes of using the category theory library should instead be

1. convenient notation when working with bundled objects/morphisms
2. stating universal properties and constructions clearly, and with a uniform API.
3. doing all of the modern mathematics outside of "category theory" which is all written in the languages of abelian categories, semisimple categories, triangulated categories, etc.
4. doing abstract category theory for its own sake, for those who like that kind of thing. :-)

[Scott Morrison]

For 2., what I have in mind is, e.g., there are many interesting adjunctions in mathematics worth having in mathlib. It's important that they all get stated as an adjunction, rather than using a different formulation of what it means to be an adjunction each time (which is prone to leaving bits out). We already have quite a few "universal properties" stated in mathlib which ideally we would clean up and state "properly" as an initialness condition, or an adjunction, etc. Similarly we have a bunch of "informal" functoriality statements.

[Scott Morrison]

If you don't need to count the "setting up the abstract nonsense", a small but nice PR from Markus #3280 significantly shortened the construction of direct sums in Ab, by saying "well, it's a preadditive category, and has products, so those products are automatically biproducts".

[Mario Carneiro]

I have to say that this is a disappointing answer, although it is more or less what I expected

[Mario Carneiro]

In theory, as long as you have enough example categories you might be able to beat the "abstract nonsense overhead" by sheer number of uses

[Scott Morrison]

I think 3. is the real motivation.

[Scott Morrison]

There is an awful lot of modern mathematics (particularly in rep theory, alg goem, quantum alg, low dim. topology) which simply can't be spoken about without a lot of category theory set up.

[Scott Morrison]

We're gradually getting to the point we're ready for these things. :-)

[Johan Commelin]

I think proving the snake lemma (and all other lemmas in homological algebra) via category theory might help. Otherwise we would have to prove them for add_comm_groups, for module, and later for abelian sheaves. And these proofs aren't exactly 1-liners.
Maybe (maybe) we still want to restate the snake lemma for (say) modules, without using the categorical language, because that way it might integrate better with other parts of the library. But I'm convinced that Markus's diagram chasing library will be a gateway drug to proving these kinds of lemmas using the category theory library.

[Kevin Buzzard]

It's probably not a coincidence that abstract category theory didn't appear until the 50s or whatever. You can get a long way without it. But after a while it becomes essential. The moment we start doing cohomology we're either going to be repeating work or using categories