Zulip Chat Archive

Stream: maths

Topic: algebra.comap


Chris Hughes (Oct 28 2019 at 00:28):

@Kenny Lau What was the motivation for defining the type alias algebra.comap. Could we have a docstring explaining the decision?

Kenny Lau (Oct 28 2019 at 00:28):

to avoid looping

Chris Hughes (Oct 28 2019 at 00:29):

Which loop?

Kenny Lau (Oct 28 2019 at 00:29):

maybe there's no loop. I'm not sure if it's necessary.

Kenny Lau (Oct 28 2019 at 00:30):

I'm just a bit worried about algebra R A and algebra S A both in the class instance

Kenny Lau (Oct 28 2019 at 00:30):

ah there's a loop: everytime you want algebra S A you would want to search for algebra S T and algebra T A

Kenny Lau (Oct 28 2019 at 00:30):

because algebra R S + algebra S A => algebra R (comap R S A)

Kenny Lau (Oct 28 2019 at 00:31):

if you remove the comap then you get algebra R S + algebra S A => algebra R A, very dangerous

Chris Hughes (Oct 28 2019 at 00:31):

I think it's not a loop, it's just a search with a metavariable in it.

Chris Hughes (Oct 28 2019 at 00:31):

Because it can't tell what the inbetween ring should be.

Kenny Lau (Oct 28 2019 at 00:32):

then to search for algebra R S you would want to look at algebra R ?m_1 + algebra ?m_1 S

Kenny Lau (Oct 28 2019 at 00:32):

and to search for algebra R ?m_1 you would want to look at algebra R ?m_2 + algebra ?m_2 ?m_1

Johan Commelin (Oct 28 2019 at 06:59):

Also, commutative diagrams, aka diamond. If you have R → A → C and R → B → C then everyone knows that there is a unique R-algebra structure on C. (If not, then what are you doing!!!!) But of course Lean cares to differ (-; By using comap we explicitly hard code which algebra structure we are talking about. Ugly, but I don't see how to avoid it.


Last updated: Dec 20 2023 at 11:08 UTC