## 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?

to avoid looping

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: May 12 2021 at 07:17 UTC