Zulip Chat Archive

Stream: maths

Topic: module


view this post on Zulip Johan Commelin (Nov 23 2018 at 12:49):

@Mario Carneiro Shouldn't this be flipped, for consistency with comp and llcomp?

def lcomp (f : M  N) : (N  P)  M  P := _ -- I would expect:   def lcomp (f : N →ₗ P) : (M →ₗ N) →ₗ M →ₗ P :=

view this post on Zulip Mario Carneiro (Nov 23 2018 at 12:50):

maybe, but the other direction is harder

view this post on Zulip Mario Carneiro (Nov 23 2018 at 12:50):

there is an order to the definitions

view this post on Zulip Johan Commelin (Nov 23 2018 at 12:50):

Also, are there compatibilities between comp and lcomp etc...? Is (lcomp f).to_fun defeq to f.comp?

view this post on Zulip Mario Carneiro (Nov 23 2018 at 12:50):

yeah, it's all defeq

view this post on Zulip Mario Carneiro (Nov 23 2018 at 12:50):

it's just composition so it's easy

view this post on Zulip Mario Carneiro (Nov 23 2018 at 12:52):

also there is a difference between lcomp that is there and the one you said

view this post on Zulip Mario Carneiro (Nov 23 2018 at 12:52):

one is precomposition and the other is postcomposition

view this post on Zulip Johan Commelin (Nov 23 2018 at 13:07):

Right, and I think the library isn't completely consistent about which one it uses for comp, lcomp and llcomp. Wouldn't it be easier if they were all post-composition?

view this post on Zulip Mario Carneiro (Nov 23 2018 at 13:09):

I mean there is a need for it, I didn't write that for no reason

view this post on Zulip Mario Carneiro (Nov 23 2018 at 13:09):

it's used before we have tensor products and swap and eval and such, so they aren't yet interchangeable

view this post on Zulip Johan Commelin (Nov 23 2018 at 13:10):

Ok, I see

view this post on Zulip Johan Commelin (Nov 23 2018 at 13:10):

So, may I then complain that the name is slightly confusing?

view this post on Zulip Mario Carneiro (Nov 23 2018 at 13:10):

rcomp :)

view this post on Zulip Johan Commelin (Nov 23 2018 at 17:23):

@Mario Carneiro I couldn't find where the zero linear map is defined, but apparently it is somewhere. However ⇑0 m doesn't simp to 0. Where should I add this simp rule?


Last updated: May 09 2021 at 09:11 UTC