Bug in equivalence_decomposition ?

[swewers]

sage: R.<x> = QQ[]
sage: v_7 = QQ.valuation(7)
sage: v0 = GaussValuation(R, v_7)
sage: v1 = v0.augmentation(x, 3/2)
sage: v2 = v1.augmentation(x^2-686, 7/2)
sage: f = x^4 - 8001504*x^2 - 592815428352
sage: v2.equivalence_decomposition(f)

leads to an assertion error:

AssertionError                            Traceback (most recent call last)
ivalence_decomposition(self, f, assume_not_equivalence_unit, coefficients, valuations, compute_unit, degree_
bound)
   1328
   1329         if compute_unit:
-> 1330             assert self.is_equivalent(ret.prod(), f) # this might fail because of leading zeros in i
nexact rings
   1331             assert self.is_equivalence_unit(ret.unit())
   1332
AssertionError:

[saraedum]

Somehow the unit part is wrong in this example. It's determined as 2 but it should have been 1.

I didn't have time to look into this further. Should anybody have a chance to debug this further, I can probably fix it but at the moment I don't see where this wrong unit comes from.

[swewers]

I think the problem is that lift_to_key does not guarantee a particular form for the equivalence unit, which makes it incompatibel with _equivalence_reduction.

sage: R.<x> = QQ[]
sage: v_7 = QQ.valuation(7)
sage: v0 = GaussValuation(R, v_7)
sage: v1 = v0.augmentation(x, 3/2)
sage: v2 = v1.augmentation(x^2-686, 7/2)
sage: f = x^4 - 8001504*x^2 - 592815428352
sage: val, phi_divides, F = v2._equivalence_reduction(f)
sage: F = F.factor()
sage: F
(2) * (x^2 + 1)
sage: g = v2.lift_to_key(F[0][0])
sage: g
x^4 - 343/2*x^2 + 1294139
sage: v2.is_equivalent(f, g)
True

I haven't really tried to understand the code for lift_to_key to be able to see what the equivalence unit R implicit in lift_to_key is.

[swewers]

Maybe the problem is that equivalence_unit doesn't have the multiplicativity property that is silently assumed?

sage: v2.equivalence_unit(7/2)^2*v2.equivalence_unit(-7)
1/343*x^2
sage: v2.reduce(_)
2

[saraedum]

Hm…equivalence_unit does not claim to reduce to 1 so maybe that's rather the problem that the implementation assumes that it does? Now I see what you mean.

[saraedum]

(I'm on Zulip, if you want to discuss this.)

[saraedum]

I think I have a fix for this. Is there an upstream ticket already?

[swewers]

No, I think there is none yet.

We want to compute u, phi_i and e_i such that f \sim u*\prod_i phi_i^e_i. One could compute u in the last step, by comparing the reduction of Rf and of R\prod_i phi_i^e_i (for an equivalence unit R with the right valuation) and then lifting the missing constant factor to a unit u.