Zulip Chat Archive

Stream: maths

Topic: conv and associativity


view this post on Zulip Scott Morrison (Nov 13 2018 at 09:22):

If any category theorists have recently been fighting with associativity, they might like the new conv tactic I just wrote:

/--
`slice` is a conv tactic; if the current focus is a composition of several morphisms,
`slice a b` reassociates as needed, and zooms in on the `a`-th through `b`-th morphisms.

Thus if the current focus is `(a ≫ b) ≫ ((c ≫ d) ≫ e)`, then `slice 2 3` zooms to `b ≫ c`.
 -/

view this post on Zulip Scott Morrison (Nov 13 2018 at 09:22):

@Reid Barton, @Michael Jendrusch, @Johan Commelin in particular may like this.

view this post on Zulip Scott Morrison (Nov 13 2018 at 09:23):

It needs a better name, and perhaps to be generalised to an arbitrary associative operation ...

view this post on Zulip Johan Commelin (Nov 13 2018 at 09:26):

Hurray! That looks really cool. And yes, I wouldn't mind having this for groups and rings as well!

view this post on Zulip Patrick Massot (Nov 13 2018 at 10:00):

Oh yes, I already asked for this tactic in groups and rings

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 13:09):

I was doing some basic binomial theorem stuff yesterday for the UGs and this would have been very convenient if it worked for + i.e. let me zoom into (a+b)+((c+d)+e)


Last updated: May 09 2021 at 10:11 UTC