## Stream: new members

### Topic: Continuous maps

#### Nicolò Cavalleri (Jul 04 2020 at 19:04):

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 (Jul 04 2020 at 22:28):

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 (Jul 04 2020 at 22:38):

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

#### Heather Macbeth (Jul 04 2020 at 22:54):

I would also be curious to know!

#### Nicolò Cavalleri (Jul 04 2020 at 22:57):

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 (Jul 04 2020 at 22:58):

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

#### Reid Barton (Jul 04 2020 at 22:59):

Or making a structure with two fields?

#### Nicolò Cavalleri (Jul 04 2020 at 23:00):

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 (Jul 04 2020 at 23:04):

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 (Jul 04 2020 at 23:04):

I mean having both things living in mathlib?

#### Reid Barton (Jul 04 2020 at 23:05):

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

#### Nicolò Cavalleri (Jul 04 2020 at 23:06):

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 (Jul 04 2020 at 23:06):

Or the structure exists?

#### Reid Barton (Jul 04 2020 at 23:06):

docs#continuous_map

#### Nicolò Cavalleri (Jul 04 2020 at 23:10):

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 (Jul 04 2020 at 23:11):

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

#### Reid Barton (Jul 04 2020 at 23:13):

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 (Jul 04 2020 at 23:13):

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

#### Nicolò Cavalleri (Jul 04 2020 at 23:14):

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 (Jul 04 2020 at 23:17):

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 (Jul 04 2020 at 23:20):

Historical reasons and/or experience

#### Nicolò Cavalleri (Jul 04 2020 at 23:22):

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 (Jul 04 2020 at 23:23):

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 (Jul 04 2020 at 23:23):

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

#### Yury G. Kudryashov (Jul 04 2020 at 23:23):

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

#### Reid Barton (Jul 04 2020 at 23:25):

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 (Jul 04 2020 at 23:25):

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

#### Nicolò Cavalleri (Jul 04 2020 at 23:26):

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 (Jul 04 2020 at 23:27):

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 (Jul 04 2020 at 23:27):

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

#### Reid Barton (Jul 04 2020 at 23:27):

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

#### Reid Barton (Jul 04 2020 at 23:28):

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 (Jul 04 2020 at 23:33):

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 (Jul 04 2020 at 23:34):

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 (Jul 04 2020 at 23:36):

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 (Jul 04 2020 at 23:48):

What other types are you talking about?

#### Yury G. Kudryashov (Jul 05 2020 at 00:33):

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 (Jul 05 2020 at 00:33):

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

#### Yury G. Kudryashov (Jul 05 2020 at 00:34):

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 (Jul 05 2020 at 00:36):

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

#### Yury G. Kudryashov (Jul 05 2020 at 01:46):

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 (Jul 05 2020 at 01:49):

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 (Jul 05 2020 at 10:26):

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 (Jul 05 2020 at 10:28):

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

#### Nicolò Cavalleri (Jul 05 2020 at 10:29):

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

#### Nicolò Cavalleri (Jul 05 2020 at 10:38):

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 (Jul 05 2020 at 10:40):

@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 (Jul 05 2020 at 10:44):

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 (Jul 05 2020 at 10:45):

That is true, but it might be a historical artefact

#### Scott Morrison (Jul 05 2020 at 10:45):

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

#### Kevin Buzzard (Jul 05 2020 at 10:46):

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 (Jul 05 2020 at 10:46):

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 (Jul 05 2020 at 10:47):

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

#### Nicolò Cavalleri (Jul 05 2020 at 10:47):

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 (Jul 05 2020 at 10:48):

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 (Jul 05 2020 at 10:49):

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

#### Kevin Buzzard (Jul 05 2020 at 10:50):

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

#### Kevin Buzzard (Jul 05 2020 at 10:50):

Try categories. They're better than ever before

#### Kevin Buzzard (Jul 05 2020 at 10:51):

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

#### Kevin Buzzard (Jul 05 2020 at 10:51):

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

#### Kevin Buzzard (Jul 05 2020 at 10:52):

It will be a great test of the concrete category API

#### Nicolò Cavalleri (Jul 05 2020 at 10:58):

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 (Jul 05 2020 at 11:00):

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 (Jul 05 2020 at 11:07):

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 (Jul 05 2020 at 11:10):

I always used to call it DAMPT too :-)

#### Nicolò Cavalleri (Jul 05 2020 at 11:12):

Kevin Buzzard said:

I always used to call it DAMPT too :-)

Ops DAMTP haha

#### Nicolò Cavalleri (Jul 05 2020 at 11:12):

It's just that DAMPT is more easily pronounced haha

#### Kevin Buzzard (Jul 05 2020 at 11:17):

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 (Jul 05 2020 at 11:18):

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

#### Nicolò Cavalleri (Jul 05 2020 at 14:35):

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 (Jul 05 2020 at 18:00):

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 (Jul 05 2020 at 18:01):

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

#### Yury G. Kudryashov (Jul 05 2020 at 18:03):

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 (Jul 05 2020 at 18:05):

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

#### Mario Carneiro (Jul 05 2020 at 18:27):

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

#### Mario Carneiro (Jul 05 2020 at 18:28):

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

#### Mario Carneiro (Jul 05 2020 at 18:28):

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

#### Yury G. Kudryashov (Jul 05 2020 at 19:01):

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

#### Yury G. Kudryashov (Jul 05 2020 at 19:03):

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

#### Yury G. Kudryashov (Jul 05 2020 at 19:06):

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 (Jul 05 2020 at 23:40):

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 (Jul 05 2020 at 23:41):

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 (Jul 05 2020 at 23:44):

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 (Jul 05 2020 at 23:44):

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

#### Mario Carneiro (Jul 05 2020 at 23:45):

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 (Jul 05 2020 at 23:45):

I think 3. is the real motivation.

#### Scott Morrison (Jul 05 2020 at 23:46):

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 (Jul 05 2020 at 23:47):

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

#### Johan Commelin (Jul 06 2020 at 04:50):

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 (Jul 06 2020 at 07:22):

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

Last updated: May 14 2021 at 03:27 UTC