morphisms up to associativity

Stream: general

[Scott Morrison]

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]

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]

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

[Scott Morrison]

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]

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]

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]

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]

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

[David Michael Roberts]

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]

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]

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

[David Michael Roberts]

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]

@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]

Hmmzzz... sounds familiar...

[Johan Commelin]

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

[Johan Commelin]

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

[David Michael Roberts]

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]

Thanks :-)

[David Michael Roberts]

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

[David Michael Roberts]

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]

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