Exterior powers of finitely presented modules #2879

HechtiDerLachs · 2023-10-02T20:47:17Z

This is a suggestions for how we could do exterior powers of modules. See the test file for how this can be used.

fingolfin · 2023-10-04T10:23:55Z

@jankoboehm it would be great if you could have a look at this and comment on it. We want to make sure that potential applications can actually use this interface; and if not, revise it. But for this of course we need to know what is needed / missing / ...

This reverts commit 48b9752.

HechtiDerLachs · 2023-10-05T15:32:01Z

test/Modules/ExteriorPowers.jl

+@testset "multiplication map" begin
+  R, (x, y, u, v, w) = QQ[:x, :y, :u, :v, :w]
+
+  F = FreeMod(R, 5)
+  F3, mm = Oscar.exterior_power(F, 3)
+  v = (F[1], F[3], F[4])
+  u = (F[1], F[4], F[3])
+  @test mm(v) == -mm(u)
+  w = mm(v)
+  @test preimage(mm, w) == v
+end


@fieker : Is this like you had intended?

HechtiDerLachs · 2023-10-05T15:35:11Z

test/Modules/GradedModules.jl

+@testset "all_monomials for graded free modules" begin
+  R, (x, y, u, v, w) = QQ[:x, :y, :u, :v, :w]
+  S, (x, y, u, v, w) = grade(R)
+
+  F = graded_free_module(S, [-1, 2])
+
+  for d in -4:4
+    amm = Oscar.all_monomials(F, d)
+    @test d < -1 || !isempty(amm)
+    @test all(x->degree(x) == grading_group(F)([d]), amm)
+  end
+end


@jankoboehm : Sorry, this was not intended to be here. It was a little play-around for me needed to take some steps towards implementing sheaf cohomology. But I guess this might be useful also for you and the graded modules in general. Would you like this to be put in a separate PR?

HechtiDerLachs · 2023-10-05T21:50:07Z

Since some people like performance comparisons:

julia> n = 12
12

julia> R, x = polynomial_ring(QQ, "x" => 1:n)
(Multivariate polynomial ring in 12 variables over QQ, QQMPolyRingElem[x[1], x[2], x[3], x[4], x[5], x[6], x[7], x[8], x[9], x[10], x[11], x[12]])

julia> F = FreeMod(R, n)
Free module of rank 12 over Multivariate polynomial ring in 12 variables over QQ

julia> v = sum(a*e for (a, e) in zip(x, gens(F)))
x[1]*e[1] + x[2]*e[2] + x[3]*e[3] + x[4]*e[4] + x[5]*e[5] + x[6]*e[6] + x[7]*e[7] + x[8]*e[8] + x[9]*e[9] + x[10]*e[10] + x[11]*e[11] + x[12]*e[12]

julia> K1 = koszul_complex(x)
K1_-1 <---- K1_0 <---- K1_1 <---- K1_2 <---- K1_3 <---- K1_4 <---- K1_5 <---- K1_6 <---- K1_7 <---- K1_8 <---- K1_9 <---- K1_10 <---- K1_11 <---- K1_12 <---- K1_13

julia> K2 = koszul_complex(v)
K2_-1 <---- K2_0 <---- K2_1 <---- K2_2 <---- K2_3 <---- K2_4 <---- K2_5 <---- K2_6 <---- K2_7 <---- K2_8 <---- K2_9 <---- K2_10 <---- K2_11 <---- K2_12 <---- K2_13

julia> @time koszul_complex(x) # the Singular implementation
  7.038626 seconds (23.58 M allocations: 1.750 GiB, 26.06% gc time)
C_-1 <---- C_0 <---- C_1 <---- C_2 <---- C_3 <---- C_4 <---- C_5 <---- C_6 <---- C_7 <---- C_8 <---- C_9 <---- C_10 <---- C_11 <---- C_12 <---- C_13

julia> @time koszul_complex(v) # the new OSCAR implementation
  1.954575 seconds (5.20 M allocations: 278.098 MiB, 31.56% gc time)
C_-1 <---- C_0 <---- C_1 <---- C_2 <---- C_3 <---- C_4 <---- C_5 <---- C_6 <---- C_7 <---- C_8 <---- C_9 <---- C_10 <---- C_11 <---- C_12 <---- C_13

jankoboehm · 2023-10-06T09:13:01Z

It looks good to me, shall we call the function mult_map rather pure and the inverse inv_pure as in the tensor product? See also in the tensor product code:

set_attribute!(F, :tensor_pure_function => pure, :tensor_generator_decompose_function => inv_pure)

Note that these functions are created, when creating the module, so they do not create a parent on the fly.

Perhaps add a show function similar to the one for the tensor product of modules, see:

set_attribute!(F, :show => Hecke.show_tensor_product, :tensor_product => G)

With regard to the show function of the elements, you can set the field F.S in a free module F, which should have the symbols for the generators.

We need not only the case of free modules but also subquos. That we can do in a seperate effort.

lgoettgens · 2023-10-06T09:53:51Z

I think it would make sense to put OrderedMultiIndex into src/Combinatorics/ as there surely are other places where this can be used. What do you think?

HechtiDerLachs · 2023-10-06T12:24:27Z

I think it would make sense to put OrderedMultiIndex into src/Combinatorics/ as there surely are other places where this can be used. What do you think?

Agreed and done.

@lgoettgens : There seems to be some problem with an existing function is_exterior_power from the Lie algebras. I don't know what's the problem and what should be done to resolve this. Could you maybe have a look?

lgoettgens · 2023-10-06T12:37:41Z

@lgoettgens : There seems to be some problem with an existing function is_exterior_power from the Lie algebras. I don't know what's the problem and what should be done to resolve this. Could you maybe have a look?

I think you create a function with that name in the global Oscar module, right? In this case, to make the two same-named functions the same, you would need to remove the two exports in experimental/LieAlgebras/src/LieAlgebras.jl and instead add is_exterior_power to the long import list at the top of the file.

lgoettgens · 2023-10-06T13:09:35Z

src/Modules/ExteriorPowers/FreeModules.jl

+  return first(koszul_duals([v], cached=cached))
+end
+
+function induced_map_on_exterior_power(phi::FreeModuleHom{<:FreeMod, <:FreeMod, Nothing}, p::Int;


A similar function already exists for LieAlgebraModule.jl under the name hom_exterior_power. It would be great to have a unified interface for both types of modules.
This is not a request for you to change your proposal, I just wanted to mention it.
@fieker suggested to name this method simply hom and supply both exterior powers as arguments, as well as the home on the base modules

HechtiDerLachs · 2023-10-11T15:02:16Z

If anyone found the time to approve and merge this, that would be great! I'm afraid the green lights of the tests might be corrupted by future merge conflicts.

fingolfin

I started to look at this but have to run to other appointments, so just some quick comments, I hope I can look at the rest later.

fingolfin · 2023-10-11T17:46:08Z