sagemath / sage

Main repository of SageMath
https://www.sagemath.org
Other
1.33k stars 453 forks source link

TensorFreeModule should not have a coercion from its quotients, ExtPowerFreeModule/ExtPowerDualFreeModule #30278

Open mkoeppe opened 4 years ago

mkoeppe commented 4 years ago

This coercion is going in the wrong direction and seems quite dangerous.

Depends on #30229

CC: @tscrim @egourgoulhon @mjungmath

Component: linear algebra

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

egourgoulhon commented 4 years ago
comment:1

What do you mean by "this coercion is going in the wrong direction"? It seems to me that the direction is correct. For instance, we have

sage: M = FiniteRankFreeModule(ZZ, 2, name='M')
sage: T = M.tensor_module(2, 0)
sage: A = M.exterior_power(2)
sage: T.has_coerce_map_from(A)
True
sage: A.has_coerce_map_from(T)
False

This is correct because any element of A is a tensor of type (2,0) (and the identification is canonical), whereas the reverse is not true.

mkoeppe commented 4 years ago
comment:2

Compare with:

sage: ZZ.has_coerce_map_from(Z5)
False
sage: Z5.has_coerce_map_from(ZZ)
True

sage: QQ.has_coerce_map_from(QQ/ZZ)
False
sage: (QQ/ZZ).has_coerce_map_from(QQ)
True
egourgoulhon commented 4 years ago
comment:3

Replying to @mkoeppe:

Compare with:

sage: ZZ.has_coerce_map_from(Z5)
False
sage: Z5.has_coerce_map_from(ZZ)
True

sage: QQ.has_coerce_map_from(QQ/ZZ)
False
sage: (QQ/ZZ).has_coerce_map_from(QQ)
True

The coercion direction is clear from the quotient view point, but the opposite direction is also clear from the "tensor with symmetries" view point. IMHO, this is the latter that we need for tensor calculus: when we do a + t, with a in A and t in T (notations from comment:1), we want the result to be in T with a prior coercion of a to an element of T.

mjungmath commented 4 years ago
comment:4

Replying to @egourgoulhon:

Replying to @mkoeppe:

Compare with:

sage: ZZ.has_coerce_map_from(Z5)
False
sage: Z5.has_coerce_map_from(ZZ)
True

sage: QQ.has_coerce_map_from(QQ/ZZ)
False
sage: (QQ/ZZ).has_coerce_map_from(QQ)
True

The coercion direction is clear from the quotient view point, but the opposite direction is also clear from the "tensor with symmetries" view point. IMHO, this is the latter that we need for tensor calculus: when we do a + t, with a in A and t in T (notations from comment:1), we want the result to be in T with a prior coercion of a to an element of T.

Precisely. That is exactly what I was going to point out as well; but you were faster. :)

There is a canonical isomorphism between anti-symmetric tensors of rank (k,0) and the exterior algebra.

I also vote to keep the current behavior, with the same argument you gave above.

mkoeppe commented 4 years ago
comment:5

Being canonical is a necessary condition for a coerce map, but not a sufficient one.

In #30242 (unfinished), this canonical injection from the exterior module to the tensor module is made available as the "lift" map. But it should not be a coercion.

mjungmath commented 4 years ago
comment:6

Replying to @mkoeppe:

...But it should not be a coercion.

Why not?

I cannot see any practical use for such a coercion. The current coercion, on the other hand, is needed to perform tensor calculus. This is what the whole piece of software is about.

Furthermore, removing the current coercion could corrupt many notebooks which have already been written with SageManifolds.

mkoeppe commented 4 years ago
comment:7

Replying to @egourgoulhon:

[...] we need for tensor calculus: when we do a + t, with a in A and t in T (notations from comment:1), we want the result to be in T with a prior coercion of a to an element of T.

Could you point me to a good example where you need this coercion, and where it would not be practical to use the lift map from A to T explicitly? This would be very helpful.

There is nothing really in the doctests of sage manifolds that needs these coercions. Indeed, if I disable these coercions, almost all tests pass.

diff --git a/src/sage/manifolds/differentiable/tensorfield_module.py b/src/sage/manifolds/differentiable/tensorfield_module.py
index fff3fac10b..4cf940a28b 100644
--- a/src/sage/manifolds/differentiable/tensorfield_module.py
+++ b/src/sage/manifolds/differentiable/tensorfield_module.py
@@ -448,14 +448,6 @@ class TensorFieldModule(UniqueRepresentation, Parent):
             return (self._tensor_type == other._tensor_type
                     and self._domain.is_subset(other._domain)
                     and self._ambient_domain.is_subset(other._ambient_domain))
-        if isinstance(other, DiffFormModule):
-            # coercion of p-forms to type-(0,p) tensor fields
-            return (self._vmodule is other.base_module()
-                    and self._tensor_type == (0, other.degree()))
-        if isinstance(other, MultivectorModule):
-            # coercion of p-vector fields to type-(p,0) tensor fields
-            return (self._vmodule is other.base_module()
-                    and self._tensor_type == (other.degree(),0))
         if isinstance(other, AutomorphismFieldGroup):
             # coercion of automorphism fields to type-(1,1) tensor fields
             return (self._vmodule is other.base_module()
diff --git a/src/sage/tensor/modules/tensor_free_module.py b/src/sage/tensor/modules/tensor_free_module.py
index 9285cbc0de..9886c90062 100644
--- a/src/sage/tensor/modules/tensor_free_module.py
+++ b/src/sage/tensor/modules/tensor_free_module.py
@@ -617,15 +617,6 @@ class TensorFreeModule(FiniteRankFreeModule):
                                          self._fmodule is other.domain()
             else:
                 return False
-        if isinstance(other, ExtPowerFreeModule):
-            # Coercion of an alternating contravariant tensor to a
-            # type-(p,0) tensor:
-            return self._tensor_type == (other.degree(), 0) and \
-                                    self._fmodule is other.base_module()
-        if isinstance(other, ExtPowerDualFreeModule):
-            # Coercion of an alternating form to a type-(0,p) tensor:
-            return self._tensor_type == (0, other.degree()) and \
-                                    self._fmodule is other.base_module()
         if isinstance(other, FreeModuleLinearGroup):
             # Coercion of an automorphism to a type-(1,1) tensor:
             return self._tensor_type == (1,1) and \
mkoeppe commented 4 years ago
comment:8

Replying to @mjungmath:

Replying to @mkoeppe:

...But it should not be a coercion.

Why not?

Basically, because not everything that we call "canonical" is actually canonical in a technical sense. The map from T to the quotient A is actually canonical. "The" lift map from A to T is not -- we are merely picking a preferred choice.

mjungmath commented 4 years ago
comment:9

What would happen if one implements both directions, i.e. both coercions? Would that be possible?

mkoeppe commented 4 years ago
comment:10

I would think that this is dangerous because the composition antisymmetrizes.

mkoeppe commented 4 years ago
comment:11

I just found a good discussion of the two viewpoints of ExtPower as a quotient space vs. as a subspace (which I was not familiar with) in https://kconrad.math.uconn.edu/blurbs/linmultialg/extmod.pdf, page 12/13.

mjungmath commented 4 years ago
comment:12

Replying to @mkoeppe:

I would think that this is dangerous because the composition antisymmetrizes.

Where's the problem in that?

However, due to my comment:7 in #30095, the aforementioned map is not necessarily an isomorphism if the field characteristic is not zero. Usually it is given, but we also allow other fields/rings as base. Hence, I tend to agree with you, Matthias.

Anyway, it would be good to keep the from Eric mentioned behavior a+T in case of characteristic zero. Is there a compromise, we can go?

By the way: not having a doctest doesn't mean that it is not used in practice, I'd say. Imho, the documention is in general very sparse, even though the manifolds extension has a comparatively comprehensive documentation.

mjungmath commented 4 years ago
comment:13

Replying to @mkoeppe:

I just found a good discussion of the two viewpoints of ExtPower as a quotient space vs. as a subspace (which I was not familiar with) in https://kconrad.math.uconn.edu/blurbs/linmultialg/extmod.pdf, page 12/13.

Thank you. This is more trustworthy than my reference to Wikipedia. On top, it is very good explained.

mjungmath commented 4 years ago
comment:14

Suggestion: What about just renaming ExtPowerFreeModule into something like AltContrTensorFreeModule, and keep the coercion as it is.

In a next step, we create the class ExtPowerFreeModule which behaves similar to quotients of polynomial rings. Namely, applying a tensor to ExtPowerFreeModule (i.e. reducing w.r.t. the ideal <x*x>) yields an element of AltContrTensorFreeModule. In that class, we can include all the things we need for a quotient such as a method lift and the coercion from tensor fields to the exterior algebra given by this quotient.

Just as a rough idea. This would make everyone happy and is mathematical rigorous.

Edit: Sorry. Wasn't such a good idea. I don't think that is what we want.

I think there should be no problem in implementing a coercion from FreeModuleTensor to ExtPowerFreeModule (given by the quotient) and a coercion from ExtPowerFreeModule to FreeModuleTensor (given by 1/k! α_(k,V) in case of zero field characteristic).

egourgoulhon commented 4 years ago
comment:15

Replying to @mkoeppe:

I just found a good discussion of the two viewpoints of ExtPower as a quotient space vs. as a subspace (which I was not familiar with) in https://kconrad.math.uconn.edu/blurbs/linmultialg/extmod.pdf, page 12/13.

Indeed, in page 12 of this reference, we can read: It means we can think of Λk (V ) as a subspace of the tensor power V⊗k instead of as a quotient space. This viewpoint is widely used in differential geometry. This is of course the differential geometry viewpoint that I took when introducing ExtPowerFreeModule. It is also written: ''That is fine for real and complex vector spaces (as in differential geometry), but it is not a universal method.''

egourgoulhon commented 4 years ago
comment:16

Replying to @mjungmath:

Suggestion: What about just renaming ExtPowerFreeModule into something like AltContrTensorFreeModule, and keep the coercion as it is.

In a next step, we create the class ExtPowerFreeModule which behaves similar to quotients of polynomial rings. Namely, applying a tensor to ExtPowerFreeModule (i.e. reducing w.r.t. the ideal <x*x>) yields an element of AltContrTensorFreeModule. In that class, we can include all the things we need for a quotient such as a method lift and the coercion from tensor fields to the exterior algebra given by this quotient.

Just as a rough idea. This would make everyone happy and is mathematical rigorous.

Edit: Sorry. Wasn't such a good idea. I don't think that is what we want.

Why do you think this is not a good idea? At least, this would be mathematically correct for any base ring...

mkoeppe commented 4 years ago
comment:17

Replying to @mjungmath:

By the way: not having a doctest doesn't mean that it is not used in practice, I'd say.

Yes, I didn't mean to imply that.

Imho, the documention is in general very sparse, even though the manifolds extension has a comparatively comprehensive documentation.

Rather, as we discussed briefly on another ticket, I think it is crucial to extend the doctests so that typical use in practice is covered, perhaps by importing the sage-manifolds worksheets.

mkoeppe commented 4 years ago
comment:18

Replying to @mjungmath:

Suggestion: What about just renaming ExtPowerFreeModule into something like AltContrTensorFreeModule, and keep the coercion as it is.

Note that #30229 (unfinished) creates submodules of the tensor modules with arbitrary prescribed symmetries. Prescribed antisymmetries are a special case. These submodules, of course, do have coercions into the ambient tensor module.

mkoeppe commented 4 years ago

Dependencies: #30229

egourgoulhon commented 4 years ago
comment:20

Replying to @mkoeppe:

Replying to @mjungmath:

Suggestion: What about just renaming ExtPowerFreeModule into something like AltContrTensorFreeModule, and keep the coercion as it is.

Note that #30229 (unfinished) creates submodules of the tensor modules with arbitrary prescribed symmetries. Prescribed antisymmetries are a special case. These submodules, of course, do have coercions into the ambient tensor module.

Indeed, this seems the way to go.

mkoeppe commented 3 years ago
comment:22

Setting new milestone based on a cursory review of ticket status, priority, and last modification date.