algebra.comap

Stream: maths

[Chris Hughes]

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

[Kenny Lau]

to avoid looping

[Chris Hughes]

Which loop?

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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]

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

[Kenny Lau]

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

[Chris Hughes]

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

[Chris Hughes]

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

[Kenny Lau]

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

[Kenny Lau]

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]

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.