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