Better handling of subspace construction in pushout

[pjbruin]

When taking a pushout of two modules in the case where the construction of exactly one of them involves a subspace construction, the result does not have a coercion map from the other object:

sage: A = ZZ^2
sage: V = span([[1, 2]], QQ)
sage: P = sage.categories.pushout.pushout(A, V)
sage: P
Vector space of degree 2 and dimension 1 over Rational Field
User basis matrix:
[1 2]
sage: P.has_coerce_map_from(A)
False

The explanation is that for the other currently existing constructions F, the result F(X) of applying the construction to X has a coercion map from X, but for the subspace construction, F(X) only has a coercion map to X.

This ticket addresses this by equipping the class ConstructionFunctor with an attribute coercion_reversed, which is False by default; if it is True for a construction F, then the pushout of two objects omits F in the case where (at a given step of constructing the pushout) including it would not yield a coercion to the final domain. Of course, we set coercion_reversed = True for the subspace construction.

No change is necessary in the case where both constructions involve F, since this situation should be taken care of by F.merge(). This is indeed true for the subspace construction, where F.merge() takes the sum of the two subspaces.

The situation described above can be viewed as the case where one of the two constructions involves a "trivial" application of F, i.e. with the subspace equal to the whole space. Hence we should interpret our situation as a case where the effect of merge() with one trivial argument is desired.

In the above example, this strategy will cause P to be equal to QQ^2, as might be expected.

CC: @simon-king-jena @nthiery @jpflori

Component: categories

Keywords: pushout subspace, sd59

Author: Peter Bruin, Robert Bradshaw

Branch/Commit: 1ef05f2

Reviewer: Jean-Pierre Flori

Issue created by migration from https://trac.sagemath.org/ticket/16507

[pjbruin]

Commit: 1e75320

[pjbruin]

Branch: u/pbruin/16507-pushout_coercion_reversed

[tscrim]

comment:2

I think this is good, but Simon/Nicolas, could I get a second opinion on this?

[tscrim]

Changed keywords from pushout subspace to pushout subspace, sd59

[jjermann]

comment:4

What about the discussion we had on sage-devel / the example 1.1 + x^2

I liked the suggestion of doing a coercion check for exceptional cases.
That would however involve applying/evaluating (part of) the functor prematurely
(which is not necessarily wrong/bad).

[pjbruin]

comment:5

Replying to @jjermann:

What about the discussion we had on sage-devel / the example 1.1 + x^2

I was planning to come back to this, but I'm currently slightly busy (moving house)...

I liked the suggestion of doing a coercion check for exceptional cases.
That would however involve applying/evaluating (part of) the functor prematurely
(which is not necessarily wrong/bad).

Yes, but as you say it is not a bad thing; in the end we have to apply the "merged" functor anyway, so the consequence of this coercion checking is just that the logic becomes a little bit more complicated.

If you feel like implementing this, feel free to go ahead; I'm not sure if I'll have enough time very soon.

[simon-king-jena]

Replying to @pjbruin:

This ticket addresses this by equipping the class ConstructionFunctor with an attribute coercion_reversed, which is False by default; if it is True for a construction F, then the pushout of two objects omits F in the case where (at a given step of constructing the pushout) exactly one of the two constructions is F. Of course, we set coercion_reversed = True for the subspace construction.

I hope this will not end up with a pullback construction.

What do you mean by "exactly one of the two constructions is F"? Isn't it the case that one can simply drop all "reversed" construction functors, before constructing the pushout? Say, if you have direct construction functors F1,...,F5 and reversed construction functors R1,R2, and consider (F5*R2*F4*F3*R1*F2*F1)(ZZ), then (R2*F4*F3*R1*F2*F1)(ZZ) coerces into (F4*F3*R1*F2*F1)(ZZ) and (F4*F3*R1*F2*F1)(ZZ) coerces into (F5*F4*F3*R1*F2*F1)(ZZ). Would this already imply that (F5*R2*F4*F3*R1*F2*F1)(ZZ) coerces into (F5*F4*F3*R1*F2*F1)(ZZ)? If yes, then one could inductively remove all the reversed construction functors, and will eventually construct the pushout of (F5*F4*F3*F2*F1)(ZZ) with the other given parent.

[robertwb]

Changed branch from u/pbruin/16507-pushout_coercion_reversed to u/robertwb/ticket/16507

[robertwb]

New commits:

5edca1c	Merge branch 'u/pbruin/16507-pushout_coercion_reversed' of git://trac.sagemath.org/sage into coerce-16507
60be6dc	Check coercions when applying coercion reversed construction functors.

[robertwb]

Changed author from Peter Bruin to Peter Bruin, Robert Bradshaw

[robertwb]

Changed commit from 1e75320 to 60be6dc

[sagetrac-git]

Branch pushed to git repo; I updated commit sha1. This was a forced push. New commits:

87f6298

Check coercions when applying coercion reversed construction functors.

[sagetrac-git]

Changed commit from 60be6dc to 87f6298

[sagetrac-git]

Changed commit from 87f6298 to e315748

[sagetrac-git]

Branch pushed to git repo; I updated commit sha1. New commits:

e315748

More reverse coercion tests.

[pjbruin]

comment:11

Replying to @simon-king-jena:

I hope this will not end up with a pullback construction.

It definitely won't; this algorithm is far from being symmetric.

Isn't it the case that one can simply drop all "reversed" construction functors, before constructing the pushout?

In that case you would end up with some object admitting coercion maps from both original objects, but the idea is to try to get something as close as possible to the "real" push-out. Hopefully Robert's list of examples makes it clear that one shouldn't just throw away all "coercion-reversed" constructions.

[pjbruin]

comment:13

Replying to jpflori (#10513):

Could you add a little documentation about the coercion_reverse thing?
Or rather, move it in the actual code, rather than in comments?
Not that the category/coercion stuff is already obscure, but...

It's a bit annoying to document member variables, one would have to do it in the class docstring. Anyway, I'll try if I can do this in a reasonable way.

[pjbruin]

Changed commit from e315748 to 1ef05f2

[pjbruin]

comment:14

I ended up moving this explanation to the docstring of pushout() instead, and also made a number of other documentation improvements.

[pjbruin]

Changed branch from u/robertwb/ticket/16507 to u/pbruin/16507-pushout_coercion_reversed

[jpflori]

comment:15

Looks better to me!

[jpflori]

Reviewer: Jean-Pierre Flori

[vbraun]

Changed branch from u/pbruin/16507-pushout_coercion_reversed to 1ef05f2