Zulip Chat Archive

Stream: new members

Topic: Hello


view this post on Zulip Harry Gindi (Nov 10 2018 at 18:35):

Hiya, some of you probably know me from mathoverflow. I was curious how things are going in here.

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:35):

Hey, welcome! Good to see you.

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:35):

Things are going pretty good here (-;

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:36):

I'm a complete noob on the whole theorem proving thing, but I feel like it's something worth learning

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:36):

One of our biggest problems is lack of (wo)man-power

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:36):

I'd like to eventually work on the library for simplicial sets, but I'm completely worthless at programming

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:37):

Right. The first thing you need to learn is that you should ask lots of questions here :lol:

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:37):

You don't need that much programming experience. Coincidentally, I did some stuff on simplicial sets a couple of months ago.

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:38):

In the mean time, Scott wrote a very very nice category library.

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:38):

Does it have Grothendieck constructions

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:38):

I've been meaning to update my stuff, but haven't done so yet.

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:38):

It only has the basics so far. We are in the process of adding limits and colimits.

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:38):

If it does, maybe it's already time to introduce the Theta construction that I use in my research

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:38):

Ah, ok!

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:39):

For example: we don't have abelian categories yet.

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:39):

If there's a simplicial library and a category theory library, you might be able to use simplicial objects in Cat to get monoidal categories

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:39):

No fundamental obstructions. Just that there are only 3 people working on this in their spare time.

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:39):

via Segal's observation

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:39):

Also, are Abelian categories really that fundamental for theorem proving?

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:40):

Practice seems to show that theorem provers need a delicate balance between hands-on constructions and big theoretical hammers.

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:40):

Not for theorem proving, but they are for applying theorem provers to (some, eg my) mathematical research.

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:41):

mhm, do you know where I can get bootstrapped with experience to start contributing?

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:41):

First you need to install a Lean environment.

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:41):

What editor do you use to type LaTeX and the likes?

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:41):

vscode

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:41):

Great!

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:41):

There is a Lean extension for VScode

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:42):

Is the Windows lean environment crippled?

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:42):

Install it, and open an empty Lean file. It will then ask if you want it to install Lean for you.

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:42):

oh, that's neat!

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:42):

I think it was fixed. I am not sure. I haven't touched Windows in 10 years.

view this post on Zulip Andrew Ashworth (Nov 10 2018 at 18:42):

If you like textbooks I would recommend Theorem Proving in Lean

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:42):

Maybe it is about to be fixed.

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:43):

If it's not working, I have the Win10 Linux emulator installed

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:43):

that's why I'm asking

view this post on Zulip Andrew Ashworth (Nov 10 2018 at 18:43):

Lean on Windows works great

view this post on Zulip Kenny Lau (Nov 10 2018 at 18:44):

@Harry Gindi here is my (controversal) instructions on how to get Lean on windows

view this post on Zulip Andrew Ashworth (Nov 10 2018 at 18:44):

There are some issues with setting $PATH correctly. However, if you are the kind of person to have WSL installed, I'm sure you'll be able to fix it

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:45):

Thanks!

view this post on Zulip Kenny Lau (Nov 10 2018 at 18:45):

oh wait, you said you're working in Linux, never mind then

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:45):

Both work, Kenny. WSL is slow though

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:46):

Disk I/O is extremely bad

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:46):

then again, so is mingw64 =D

view this post on Zulip Kenny Lau (Nov 10 2018 at 18:46):

what do you mean?

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:47):

iirc disk i/o on cygwin and msys is benchmarked just as slow as WSL

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:47):

it's the main reason why things are so slow.

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:48):

I was really active on the WSL github for like two years, and performance is on-par with linux now except for disk i/o

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:49):

@Harry Gindi Once you have Lean installed, you will want to fork https://github.com/leanprover-community/mathlib/
Then you need to run leanpkg build in that directory. After that, get yourself some tea. Your computer will be warming your room for about an hour.

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:49):

but I also used msys2 before, and it was even slower

view this post on Zulip Kenny Lau (Nov 10 2018 at 18:49):

then what's the best one?

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:49):

Kenny Lau, meh, nothing's great. The best thing you could do probably is run a VM

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:49):

if you're concerned about performance

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:49):

Thanks Johan!

view this post on Zulip Andrew Ashworth (Nov 10 2018 at 18:50):

I compile Lean with MSYS2, disk i/o is far from the limiting factor when it comes to performance

view this post on Zulip Kenny Lau (Nov 10 2018 at 18:50):

and you need to rewarm your room for an hour every time you update mathlib, isn't Lean wonderful!

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:51):

Andrew Ashworth, then maybe performance on WSL is better than msys2 on everything but disk I/O

view this post on Zulip Kenny Lau (Nov 10 2018 at 18:51):

@Harry Gindi ping

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:51):

hello!

view this post on Zulip Kenny Lau (Nov 10 2018 at 18:51):

Harry Gindi, not ping

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:51):

I'm aware, I'm just using the web UI

view this post on Zulip Andrew Ashworth (Nov 10 2018 at 18:51):

is it now? I can't imagine there being a huge difference

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:52):

Andrew, they did benchmarks on phoronix, and on cpu-only tasks, WSL performs at 95-100% of native

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:52):

once it hits disk i/o, it crashes to like 20%

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:53):

it has to do with the fact that NTFS doesn't use inodes and therefore can't cache them effectively

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:54):

also, windows defender, and a bunch of other things just kill it on disk i/o

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:54):

anyway, going to get this lean system installed

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:54):

does arch have a lean-git AUR package?

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:55):

Looks like it does

view this post on Zulip Andrew Ashworth (Nov 10 2018 at 18:55):

ah, I was aware of that. I think you can compile Lean with visual studio and get a totally native binary, if i recall correctly

view this post on Zulip Andrew Ashworth (Nov 10 2018 at 18:55):

i've never investigated it though, so ymmv

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:55):

blech, I have an arch installation on this pc

view this post on Zulip Andrew Ashworth (Nov 10 2018 at 18:56):

disk access is not an issue at 20% or 100% anyway

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:56):

but every time I decide to jump into linux, I get sidetracked

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:56):

I end up staying up all night messing around with it, it's unhealthy for me

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:56):

Don't use that arch thing.

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:56):

oh, it's bad?

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:57):

or are you saying don't use arch in general :D

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:57):

The VScode Lean extension is better. It sets up a useful wrapper called elan.

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:57):

No, I run arch as OS :lol: So that's fine.

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:57):

the arch thing is just a lean system, I thought

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:58):

anyway gonna work on this tomorrow morning

view this post on Zulip Harry Gindi (Nov 10 2018 at 18:58):

cheers all

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 20:00):

@Kenny Lau I think https://github.com/leanprover/mathlib/blob/master/docs/elan.md is a better place to direct computer-savvy Windows users to than your link

view this post on Zulip Kenny Lau (Nov 10 2018 at 20:08):

fair

view this post on Zulip Scott Morrison (Nov 10 2018 at 21:30):

Yes --- please, please, everyone should now be using elan, no messing around with $PATH, no installing complicated things like msys2 or WSL, just go with the bare minimum provided by "git bash" and its installer, then work entirely inside VS Code.

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:30):

@Harry Gindi ^^ that

view this post on Zulip Scott Morrison (Nov 10 2018 at 21:33):

Also, welcome @Harry Gindi. :-)

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:33):

Got it, thanks!

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:34):

Also hello, Kevin and Scott, it's been a while since I saw you on MO

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:34):

Here is a roadmap to getting started. First read through all of Theorem Proving In Lean and do all the exercises. Then choose a project to work on, and work on it.

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:34):

The projects I chose were: (1) do all the exercises in the undergraduate class I was teaching at the time and then (2) define schemes and prove that an affine scheme is a scheme.

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:35):

Do not underestimate how difficult all of this is at this point.

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:35):

It seems like it'll be really annoying, don't worry =)

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:36):

I think maybe a good project to work on would be weak factorization systems once I learn stuff

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:36):

Working with isomorphisms is difficult. Working with categories is even more difficult, for several reasons -- some associated with dependent type theory (it is difficult to transport structure along isomorphisms at this point, although things will change one day), some associated with universe issues (mathematicians being sloppy about universes, basically) and other things too

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:37):

But there is no better recommendation than "start on something and whenever you get stuck, ask here"

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:37):

The first thing you will probably have to ask is a question of the form "here's a link to a pdf, I want to make definition 2.3 of that paper in Lean, where do I even start?". There will be an answer.

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:38):

WFS would be useful if anyone wants to go full bore and do model categories, and it can be done with monads for algebraic weak factorization systems

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:38):

I'm guessing that monads work well?

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:38):

Listen, honestly, categories are really like jumping in at the deep end

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:38):

ah

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:38):

groups work well

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:38):

but it is not impossible, and you have to jump in somewhere

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:39):

I mean, my research is in category theory

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:39):

but I'll see how hard it is

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:39):

well, when I arrived here a year ago people were already talking about formalising categories, and one year later they still haven't managed to do adjoint functors.

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:40):

This is basically for two reasons: (1) universes make this harder than you think and (2) lack of manpower or personpower or whatever it should be called nowadays

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:40):

I would have assumed that monads might be easier than adjunctions, but maybe this is a mistake

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:40):

I'm also exaggerating a little. But dependent type theory is perhaps not set up with category theory in mind

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:41):

On the other hand, "difficult" is certainly not the same as "impossible"

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:41):

Do presheaves of sets make sense?

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:41):

and there is no actual obstruction to doing adjoints and a whole bunch more. It's just that people really like (a) working in the maximal generality and (b) writing automation as they go

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:41):

they call them presheaves of types here

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:42):

but I defined these in a hands-on way when doing schemes, no problem

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:42):

Neat, I'll have to look at what you've done already before I try to jump in

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:42):

I did not use the category theory machinery though, I just wrote down the axioms for a functor in that specific case rather than relying on a general theory (which at that time was not there anyway)

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:42):

My code sucks though

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:43):

because it was the code I wrote to learn how to do mathematics in dependent type theory

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:43):

I am currently refactoring all of it with an MSc student

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:43):

so when you defined schemes, did you follow e.g. Toën?

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:44):

working with functors of points the whole way?

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:44):

or is that exactly the kind of non-kosher thing that implicitly uses universes

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:44):

I followed the stacks project

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:44):

https://github.com/kbuzzard/lean-stacks-project/blob/master/src/tag009I.lean

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:44):

there's presheaves of types on a basis of open sets of a top space

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:44):

But nowadays we would not write it like that

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:45):

we'd use the category theory machinery, which seems to be just about ready to do that sort of thing.

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:45):

As of about last week

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:45):

neat!

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:45):

I heard that some simplicial set machinery was developed up-thread

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:46):

was this done entirely without model structures using e.g. Ex^∞?

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:47):

In that code I linked to, I am literally saying that a presheaf of types is a function F which takes a basis element to a type, plus a restriction F(U)->F(V), plus the axioms that res from U to U is id and res of res is res. So I am avoiding explicit usage of any category theory formalism.

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:47):

You'll have to ask @Johan Commelin where he put his simplicial set stuff. That was also written before categories were available, I believe.

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:47):

mhm

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:47):

alright let's not but the cart before the horse, I've gotta do the exercises and stuff

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:48):

cheers, this seems exciting

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:48):

it's the future

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:48):

but I might have died before it becomes really important

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:48):

I have no idea of the time frame before it becomes (a) useful (b) powerful (c) better than us

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:48):

ascended to robothood

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:48):

but currently we are still a long way from (a)

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:49):

"proof assistants" currently do nothing but make mathematician's lives harder, for the most part.

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:49):

like any assistant they must be trained =p

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:49):

otherwise all they do is spill coffee on you

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:50):

right. And my view (and I do say this firmly with my tongue in my cheek and slightly provocatively, but there is a grain of truth in it) is that currently the main problem is that for the most part they are being trained to do mathematics by computer scientists, which is in my opinion not driving development in the right directions.

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:51):

I'm going to try to get my friend in the US involved on this

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:51):

There are a few mathematicians here who are trying to change all this, mostly by saying things such as "mathematicians will not be able to use your software unless you make stuff like (x+y)^3=x^3+3x^2y+3xy^2+y^3 easy to do"

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:51):

he did a math undergrad and he's doing a CS Ph.D., but he hates CS

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:52):

this might be a nice change of pace for him

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:52):

https://xenaproject.wordpress.com/2018/06/13/ab3/

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:52):

is anyone doing analysis-related stuff?

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:52):

Yes, but it's happening very slowly

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:52):

because he always liked analysis

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:52):

alright, I'll try to cajole him into helping =)

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:53):

and in my opinion there is a problem with the development plan we have

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:53):

In fact Harry to be honest basic freshman one variable analysis would be a perfect project to learn Lean with

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:53):

because the maths is basically very well known and well understood, and putting it into a theorem prover would be a formidable challenge for a beginner, however there would be plenty of people around to help

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:54):

The problem is that the general position here is "do everything in the correct generality" which means "the maximal generality"

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:54):

break out a copy of Bourbaki's 'analysis in one real variable' haha

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:55):

so instead of developing a basic theory of analysis of functions of one real variable, everyone wants to do stuff on normed spaces and Banach spaces etc etc and then prove all the single-variable theorems in one fell swoop by specialising to this case

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:55):

Is that even possible?

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:55):

In my mind a good analogy here is what happened with polynomials

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:55):

A computer scientist developed a fabulous library of polynomials in an arbitrary number of variables (in fact for an arbitrary set of variables)

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:56):

but when mathematicians wanted to actually use it to prove basic stuff like quadratic reciprocity or finite fields or whatever

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:56):

For example, defining C^\infty functions requires you do have partial derivatives, which come from the 1-dimensional case, if I remember correctly (I haven't done analysis in around 8 years =\)

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:56):

they found they really just wanted a much deeper theory of polynomials in one variable

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:57):

so at the end of the day an undergraduate here at Imperial, Chris Hughes, just wrote the theory of polynomials in one variable anyway.

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:57):

And I kind of suspect that the same might happen for differentiable functions.

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:57):

Eventually we'll have them on Banach manifolds or something

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:57):

oh, you're saying that you agree that the 1-variable case is separate and important

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:57):

but then when someone wants to prove that the derivative of sin is cos (which we do not have at this point)

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:58):

they will not want to work on a Banach manifold

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:58):

it's not even meaningful on a banach manifold

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:58):

the derivative of a map of manifolds is a map on tangent bundles

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:58):

I know, I'm just saying that if you write general functions which work in some big generality then you will just end up constantly having to tell these functions to specialise to the case of the real numbers

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:59):

sure, yes

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:59):

the derivative of a map of manifolds is a map on tangent bundles

right, and you'll then have to identify the tangent space of the reals with the reals etc

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:59):

What I am saying is that in my opinion there is a need for a theory of functions in one real variable

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:59):

and that identification is not obvious without additional structure

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:59):

I believe that there is a little about functions in one complex variable, somewhere in the modular forms work

view this post on Zulip Harry Gindi (Nov 10 2018 at 21:59):

I get ya!

view this post on Zulip Harry Gindi (Nov 10 2018 at 22:00):

I fully agree with this

view this post on Zulip Harry Gindi (Nov 10 2018 at 22:01):

there's almost always a distinguished most important 1-dimensional case of whatever

view this post on Zulip Harry Gindi (Nov 10 2018 at 22:01):

imagine if people tried to write the categories library starting with 2-categories

view this post on Zulip Harry Gindi (Nov 10 2018 at 22:01):

It's also why e.g. Lawvere's ETCC was dead on arrival

view this post on Zulip Harry Gindi (Nov 10 2018 at 22:02):

anyway, I'm going to give some of this a shot tomorrow morning

view this post on Zulip Harry Gindi (Nov 10 2018 at 22:02):

cheers!


Last updated: May 11 2021 at 00:31 UTC