Stream: math-comp users

Topic: Limitations of MathComp ambient structures

Karl Palmskog (Jan 11 2022 at 16:13):

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.

Karl Palmskog (Jan 11 2022 at 16:19):

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

Cyril Cohen (Jan 11 2022 at 16:33):

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

Enrico Tassi (Jan 11 2022 at 17:37):

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.

Kenji Maillard (Jan 11 2022 at 17:46):

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.

Assia Mahboubi (Jan 12 2022 at 13:12):

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.

Assia Mahboubi (Jan 12 2022 at 13:34):

I have contacted him by email to let him know.

Enrico Tassi (Jan 12 2022 at 13:34):

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?

Enrico Tassi (Jan 12 2022 at 13:39):

ok

Ali Caglayan (Jan 12 2022 at 17:34):

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?

Assia Mahboubi (Jan 13 2022 at 15:36):

@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