Zulip Chat Archive

Stream: general

Topic: complex

Johan Commelin (Jul 08 2020 at 12:47):

What do people think of renaming complex to complex_numbers?
There are several other notions of complex (see e.g. https://github.com/leanprover-community/mathlib/pull/3316/files#diff-002c2f374abb3b7357014befa3ba9ba2R40) that could have a nice name (maybe in a namespace, like category_theory.complex; note that category_theory is often open, if it is imported) and we would avoid conflicts this way.

The reason I dare to propose this change, is because we use notation anyway.

Gabriel Ebner (Jul 08 2020 at 12:50):

But I'd prefer the singular complex_number instead.

Johan Commelin (Jul 08 2020 at 12:50):

Ooh, sure... it's hidden by notation anyway (-;

Gabriel Ebner (Jul 08 2020 at 12:51):

What about definitions like complex.sin, and theorems like complex.add_im, etc.?

Johan Commelin (Jul 08 2020 at 12:51):

Aah, This would solve the dot notation problem, right?

Gabriel Ebner (Jul 08 2020 at 12:52):

Unfortunately we can't write 0.im yet.

Johan Commelin (Jul 08 2020 at 12:52):

No... if we keep the namespace complex, then z.sin will not make sense any more. Just like we wanted.

Gabriel Ebner (Jul 08 2020 at 12:53):

I'm absolutely against calling the type complex_number and the namespace complex.

Johan Commelin (Jul 08 2020 at 12:53):

How about cplx for both?

Johan Commelin (Jul 08 2020 at 12:54):

We already have nat and int and rat. Of course real and cplx are a bit more complicated, so they deserve 4-letter names.

Gabriel Ebner (Jul 08 2020 at 12:55):

I'm not against cplx.

Alex J. Best (Jul 08 2020 at 13:01):

I'm not a fan of cplx it just looks too random to my eye, nat and int and rat are at least just abbreviations of the full word. If we had way more stuff about homological complexes I could see a reason to change, but at this point adding a bunch of characters in a lot of files doesnt seem worth it to save only a few in one file. A lot more maths involves the complex numbers than homological complexes anyway!

Reid Barton (Jul 08 2020 at 13:09):

Why not just call it ℂ

Johan Commelin (Jul 08 2020 at 13:12):

Would work for me

Johan Commelin (Jul 08 2020 at 13:12):

I don't know if we want to start using unicode in names of types

Gabriel Ebner (Jul 08 2020 at 13:30):

Is the sine function then called ℂ.sin?

Reid Barton (Jul 08 2020 at 13:32):

That was what I was imagining, though I guess we could keep the namespace complex, perhaps

Mario Carneiro (Jul 08 2020 at 15:43):

that would mess up projection notation

Johan Commelin (Jul 08 2020 at 16:10):

Yes, but in the case of complex projection notation is usually "evil" anyways.

Gabriel Ebner (Jul 08 2020 at 16:24):

I don't see the point in changing the type name, but not the namespace name. Isn't the idea that we want to use complex for some other more important complexes? Wouldn't we still have the name clashes in the namespace then?

Johan Commelin (Jul 08 2020 at 16:38):

Well, those other complexes might be category_theory.complex, but after open category_theory I think Lean will get confused by

C : complex V b

and might say function expected at 'complex' if _root_.complex is the complex numbers...

Johan Commelin (Jul 08 2020 at 16:38):

Or does this just work? And will lean figure out that in this context category_theory.complex makes sense.

Mario Carneiro (Jul 08 2020 at 16:39):

that specific example will probably work

Johan Commelin (Jul 08 2020 at 16:42):

Ooh, well, maybe that means we don't need to do anything...

Mario Carneiro (Jul 08 2020 at 16:44):

another trick you can use, with a different set of upsides and downsides, is local notation `complex` := category_theory.complex

Scott Morrison (Jul 09 2020 at 00:37):

I'm not actually sure there's going to be a "one true (homological complex)", because my experiments so far with (short) exact sequences, thinking about bicomplexes, salamanders, and snakes, suggests we're going to need several inter-convertible types, at least:

  1. a complex modelled as a function from int to V (and dependently typed functions for the morphisms)
  2. a complex modelled as a inductive type (basically, a fancy version of list, called something like morphism_sequence), for dealing with "explicit" small complexes
    This makes me more relaxed about name conflicts, because we're likely to have several names anyway.

Scott Morrison (Jul 09 2020 at 00:38):

And in any case, in order to prevent anti-category-theory bias inhibiting people from proving the snake lemma, it should be called algebra.homology.complex, not category_theory.complex. :-)

Johan Commelin (Jul 09 2020 at 04:11):

@Scott Morrison Are those experiments already building on the machinery of @Markus Himmel ?

Last updated: Dec 20 2023 at 11:08 UTC