Zulip Chat Archive

Stream: general

Topic: morphisms up to associativity


Scott Morrison (May 29 2019 at 09:49):

I wrote a preliminary attempt to allow composing morphisms in a monoidal category that aren't quite composable, and need associators/unitors inserted. Similarly, I want to be able to say two morphisms are equal, up to composing with appropriate associators.

Scott Morrison (May 29 2019 at 09:50):

In an attempt to intrigue @Kevin Buzzard, I did this in terms of a "canonically_isomorphic" typeclass predicate, so you can write f ≫≅ g to compose two morphisms that aren't quite composable, but are if you have an appropriate canonically_isomorphic instance in between.

Similarly you can write f =≅ g to test equality.

Scott Morrison (May 29 2019 at 09:51):

The code is at https://github.com/leanprover-community/mathlib/commit/939662add11b3b205b90ee3b122c985e76b96491

Scott Morrison (May 29 2019 at 09:51):

It's definitely just a WIP. In particular, nothing here reflects that fact that a canonical isomorphism from an object to itself must be the identity.

Kevin Buzzard (May 29 2019 at 10:23):

If you admit that both the standard normalisations of class field theory are canonical, which I think they are, then you have to let go of at least one of the following ideas: a composition of canonical isomorphisms is canonical; the inverse of a canonical isomorphism is canonical; the only canonical isomorphism from X to X is the identity.

Scott Morrison (May 29 2019 at 13:11):

I'm curious if you've looked at David Roberts' article about Mochizuki's "proof" of abc. It looks very much like he's saying: "Mochizuki is treating canonical isomorphisms as equalities, but he's using too many and they're not actually coherent."

Johan Commelin (May 29 2019 at 14:08):

No, that was not my impression. I think it's the other way round. @David Michael Roberts please correct me if I'm wrong.
I think what David is saying is something like: "Mochizuki had a discussion with PS and JS. PS and JS see certain canonical isomorphisms, and treat them as equalities. But Mochizuki claims they shouldn't, because they aren't coherent."
Note: David is not claiming that Mochizuki (or PS and JS for that matter) is right, but he's trying to rephrase Mochizuki's counterclaims in a language that we might understand.

Scott Morrison (May 29 2019 at 14:37):

Sorry, you're absolutely right. I've misremembered it exactly backwards...

David Michael Roberts (May 29 2019 at 21:07):

Worse. From what I understand, Mochizuki is essentially trying to generate a monoid of endomorphisms of an object that appears in a diagram in some concrete category C, to in some sense close up some subset of that object under the action. Because he doesn't use diagrams properly, he uses 'polymorphisms', when you should really think of that as the image of the hom-set of the diagram shape D, under the diagram D --> C.

David Michael Roberts (May 29 2019 at 21:10):

And he talks about 'polyisomorphisms' which are a fancy way of considering subsets of groups of automorphisms, if one does the identifications PS and JS do. The replacement of some 'full polyisomorphism' (aka the full automorphism group) by the identity map means throwing away all the group except the identity.

Johan Commelin (May 29 2019 at 21:10):

Did you ever hear some sort of reaction/reply from Mochizuki's camp?

David Michael Roberts (May 29 2019 at 21:11):

One can phrase polymorphisms as the morphisms of a category, and the polyisomorphisms are not invertible in that category. But my claim is that the whole approach is baroque and probably unneeded, if one uses existing category theory properly.

David Michael Roberts (May 29 2019 at 21:14):

@Johan Commelin I've had productive conversations with Taylor Dupuy, who isn't really in M's camp, but who is trying to properly go through the details to understand what is going on. He knows anabelian geometry, and has made progress, but is by no means convinced by M. He's been to Kyoto at least twice, to talk in person with M, and various documents on M's website got updated, to which Taylor essentially said "was that trying to explain what we discussed???"

Johan Commelin (May 29 2019 at 21:15):

Hmmzzz... sounds familiar...

Johan Commelin (May 29 2019 at 21:15):

As in... another instance that shows the huge disconnect

Johan Commelin (May 29 2019 at 21:16):

I must say that I very much appreciate how you tried to illuminate the "baroque" approach.

David Michael Roberts (May 29 2019 at 21:17):

I think Taylor (joint with Anton Hilado, and using efforts of others, like Lepage) has unwound, in ordinary language, the proof of Cor 3.12 => abc, starting from a plain-language statement of the former

David Michael Roberts (May 29 2019 at 21:17):

Thanks :-)

David Michael Roberts (May 29 2019 at 21:18):

And there have been serious efforts of stripping away all the Frobenioid stuff that M confessed was completely unnecessary.

David Michael Roberts (May 29 2019 at 21:20):

Personally, I think Taylor's doing, whether he officially is or not, the job that the referee would or should be doing on those papers. PS+JS did a first 'sniff test' and felt is wasn't up to scratch, but due to the communication issues, I incline to the view that their simplifications were a bit too strong, allowing that M may still be barking up the wrong tree.

David Michael Roberts (May 29 2019 at 21:56):

And by 'may' I mean 'until proven otherwise'.


Last updated: Dec 20 2023 at 11:08 UTC