Would be interesting to hear MathComp users/devs comment on the following claim about limitations of the MC approach to reasoning about structures:

It is worth noting however that such a trick [working with an ambient structure and its substructures] does not work more generally: for example in algebraic geometry one uses the category of commutative rings with 1, and morphisms by definition send 1 to 1. If R and S are general commutative rings with 1 then there is in general no morphism of rings from R to R × S sending 1 to 1, so one is forced to implement commutative ring theory in a more “traditional” manner.

I personally can't think of any CS applications where I would hit this case, at least...

Sure it does not always work, although it also works for another interesting class of: field extensions.

If I get correctly what he talks about, I would not call it trick.I don't know about fields, but in the local analysis part there are so many "notations" that just don't make sense if you are not in an ambient group (even if they don't state it explicitly every time). Of course I'm no mathematician... but it really seemed that the ambient structure is what they had in mind, just made very formal.

Maybe it's more of a terminological issue than a mathematical one: looking at subgroups of one fixed ambient group G correspond to working in a (subcategory of a) slice category of groups over G. Sure it is not the same as working with abstract groups (the forgetful functor is not full), but it is a sensible things to consider for specific goals/theorems.

I still do not understand why he wants to call this a trick, although some people have already suggested that it is not one. What he says about the way group morphisms are implemented in MC, suggesting that the definition requires the same ambient group for domain and co-domain is of course completely wrong.

I have contacted him by email to let him know.

Should I CC Kevin, he is on this zulip (but not following this stream)? I don't know if that paper is final yet, so he may be in time to fix it?

ok

Cyril Cohen said:

Sure it does not always work, although it also works for another interesting class of: field extensions.

Are you describing char 0 fields sitting in $\Bbb C$ or something else?

@Ali Caglayan Not necessarily $\mathbb{C}$, but typically $K < K[\alpha]< L$, for $K$ and $L$ fields. $L$ is usually the splitting field of a polynomial $\alpha$ is a root of.

Last updated: Dec 05 2023 at 04:01 UTC