hivert · 2026-07-16T07:56:29Z

Motivation for this change

This PR generalize the compose or linear morphism w.r.t. to change of scalar:

By "linear with change of scalar" I mean the following: suppose that I've two rings $$R$$ and $$S$$ together with a morphism $$f : R \to S$$, and two modules $$M_R$$ and $$M_S$$ respectively on $$R$$ and $$S$$. I'm considering maps $$\phi : M_R \to M_S$$ which are $$Z$$-module morphisms and moreover for all $$c \in R$$ and $$x\in M_R$$ verify $$\phi (c\cdot x) = f(c)\cdot\phi(x)$$ where "$$\cdot$$" denote scalar multiplication. Such a map would be of type {linear RM -> SM | f \; *:%R} with MC notations. If someone knows a better name than "linear with change of scalar" I'd like to know by the way.

So here is my attempt:

Variables
  (R S T : nzRingType) (f : {rmorphism R -> S}) (g : {rmorphism S -> T})
    (RM : lmodType R) (SM : lmodType S) (TM : lmodType T)
    (F : {linear RM -> SM | f \; *:%R}) (G : {linear SM -> TM | g \; *:%R}).

Check G \o F : {additive RM -> TM}.

So far so good. My problem is that the compose map is not linear:

Fail Check G \o F : {linear RM -> TM | g \o f \; *:%R}.

MC should be able to infer this instance.

Minimal TODO list

added changelog entries with doc/changelog/make-entry.sh

added corresponding documentation in the headers
tried to abide by the contribution guide
this PR contains an optimum number of meaningful commits

See this Checklist for details.

Automatic note to reviewers

Read this Checklist.

proux01 · 2026-07-16T08:45:03Z

CI is not happy, unfortunately, it seems that making the new code an actual generalization of the previous one will require some more efforts (to infer things like id \; s when s is not already of that form for instance).

SnarkBoojum · 2026-07-16T08:51:45Z

Your $$f$$ is a choice, so it's not a canonical construction with respect to $$\Phi$$. It should be easy to compose two enriched maps (each being a pair $$(f, \Phi)$$), and with a coercion it's probably possible to go from a bland linear map to a pair with identity on first component; but that's ugly.

hivert · 2026-07-16T09:03:37Z

CI is not happy, unfortunately, it seems that making the new code an actual generalization of the previous one will require some more efforts (to infer things like id \; s when s is not already of that form for instance).

I'm trying something like that (inserting the id in the notation)...

hivert · 2026-07-16T12:03:10Z

My fix doesn't work. The compose of two simple linear function, that is with the scaling idfun \; :*R is now linear with scaling idfun \o idfun \; :*R that is not simple linear anymore. So compilation fails the first time one compose three function and need the result to be simple linear. This is confirmed by:

Check mxvec \o f : {linear _ -> _ | idfun \o idfun \; _}.
Fail Check mxvec \o f : {linear _ -> _ | idfun \; _}.

Any trick to solve convince here that idfun \o idfun is the same as idfun ???

Otherwise, I don't really know what's the best path here...

hivert · 2026-07-16T12:28:31Z

Your f is a choice, so it's not a canonical construction with respect to Φ .

From a general point of view, this is true. Now is $$f$$ is a natural embedding as in $$N \to Z \to Q \to R \to C$$ or a natural projection as in $$Z \to Z/pZ$$, I would say that it is canonical and happy to declare it so in MC...

The use case I had was something along the line of having Rocq/MC infer that the obvious map $$Z[X] \to Q[X] \to \overline{Q}[X]$$ is "linear".

hivert added the kind: enhancement Issue or PR about addition of features. label Jul 16, 2026

Generalized compose of linear maps

bbdc7e8

hivert force-pushed the change_ring_linear_composition branch from bdc289c to bbdc7e8 Compare July 16, 2026 08:59

Navigation Menu

Uh oh!

Generalized compose of linear maps w.r.t. to change of scalar - #1627