Universe issue (infinite loop)

Stream: mathlib4

[Antoine Chambert-Loir]

When I want to rw a function that I can't reduce to a MWE, Lean is stuck at solving the universe constraint.
The error message seems to indicate that it rewrites things indefinitely. Has anyone seen/solved such a problem before?

[Adam Topaz]

Can you copy/paste the universe error?

[Antoine Chambert-Loir]

Not really because I need to stop VSCode by closing the window…
I'll try to copy something

[Adam Topaz]

Oh I see... maybe a screenshot?

[Antoine Chambert-Loir]

Finally, I could ! (its much longer…)

stuck at solving universe constraint
  max (max (max (u_1+1) (u_2+1)) u_3) u_4 =?= max (max (max (u_1+1) u_3) u_4) (?u.894720+1)
while trying to unify
  ↑(generize A N m) f
with
  (↑(generize A N m) f)
    ((↑(generize A N m) f) A A ((↑(generize A N m) f) A inst✝¹⁰) ((↑(generize A N m) f) A inst✝¹⁰)
      ((↑(generize A N m) f) A ((↑(generize A N m) f) A ((↑(generize A N m) f) A inst✝¹⁰)))
      ((↑(generize A N m) f) A inst✝¹⁰ M inst✝⁹ inst✝⁷ N inst✝⁸ inst✝⁶)
      ((↑(generize A N m) f) A inst✝¹⁰ ((↑(generize A N m) f) κ A inst✝¹⁰) N
        ((↑(generize A N m) f) ((↑(generize A N m) f) κ A inst✝¹⁰)
          ((↑(generize A N m) f) ((↑(generize A N m) f) κ A inst✝¹⁰)
            ((↑(generize A N m) f) ((↑(generize A N m) f) κ A inst✝¹⁰)
              ((↑(generize A N m) f) ((↑(generize A N m) f) κ A inst✝¹⁰) ((↑(generize A N m) f) A κ inst✝¹⁰)))))
        inst✝⁸
        ((↑(generize A N m) f) A A κ ((↑(generize A N m) f) A inst✝¹⁰) inst✝¹⁰
          ((↑(generize A N m) f) A ((↑(generize A N m) f) A inst✝¹⁰)))
        inst✝⁶)
      ((↑(generize A N m) f) A M N inst✝¹⁰ inst✝⁹ inst✝⁷ inst✝⁸ inst✝⁶)
      ((↑(generize A N m) f) A inst✝¹⁰ ((↑(generize A N m) f) κ A inst✝¹⁰) N
        ((↑(generize A N m) f) ((↑(generize A N m) f) κ A inst✝¹⁰)
          ((↑(generize A N m) f) ((↑(generize A N m) f) κ A inst✝¹⁰)
            ((↑(generize A N m) f) ((↑(generize A N m) f) κ A inst✝¹⁰)
              ((↑(generize A N m) f) ((↑(generize A N m) f) κ A inst✝¹⁰) ((↑(generize A N m) f) A κ inst✝¹⁰)))))
        inst✝⁸
        ((↑(generize A N m) f) A A κ ((↑(generize A N m) f) A inst✝¹⁰) inst✝¹⁰
          ((↑(generize A N m) f) A ((↑(generize A N m) f) A inst✝¹⁰)))
        inst✝⁶)
      ((↑(generize A N m) f) A M N inst✝¹⁰ inst✝⁹ inst✝⁷ inst✝⁸ inst✝⁶)
      ((↑(generize A N m) f) A inst✝¹⁰ ((↑(generize A N m) f) κ A inst✝¹⁰) N
        ((↑(generize A N m) f) ((↑(generize A N m) f) κ A inst✝¹⁰)
          ((↑(generize A N m) f) ((↑(generize A N m) f) κ A inst✝¹⁰)
            ((↑(generize A N m) f) ((↑(generize A N m) f) κ A inst✝¹⁰)
              ((↑(generize A N m) f) ((↑(generize A N m) f) κ A inst✝¹⁰) ((↑(generize A N m) f) A κ inst✝¹⁰)))))

[Adam Topaz]

We have indeed run into various universe issues around max. Does adding explicit universe parameters for generize help at all?

[Antoine Chambert-Loir]

By the way, if it can help, I am doing rw [generize_comp_equiv f e m with

theorem generize_comp_equiv (f : PolynomialMap A M N)
  {ι : Type} {κ : Type _} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (e : ι ≃ κ) (m : κ → M) :
  generize A N m f = (rTensor N
    (MvPolynomial.aeval (fun i ↦ MvPolynomial.X (e i))).toLinearMap)
      (generize A N (fun x ↦ m (e x)) f) := … ```

[Antoine Chambert-Loir]

In that definition, I had needed to restrict ι to a type at the first level.
(And the ultimate goal of this, whatever it means, is that I have an obvious equality except that I have to pass from Fin n to ULift (Fin n)… — maybe it is there that I should fix the universe problem.)

[Adam Topaz]

Do you have this code in a branch of mathlib4?

[Antoine Chambert-Loir]

For the moment, it is in an independent project with @María Inés de Frutos Fernández , but let me create a branch.

[Antoine Chambert-Loir]

This is branch#PolynomialMap

[Antoine Chambert-Loir]

Part of the complexity may come from the equivalence zooEquiv which implements the module isomorphism between $A[\sigma] \otimes_A M$ and a module $M [\sigma]$ which mathlib does not know (yet).

[Adam Topaz]

Another source of universe complexity comes from your definition of PolynomialMap, since it quantifies over rings. So that means PolynomialMap itself will have some universe parameters which dont appear in the universe levels of A, M and N. The following would simplify things a bit:

@[ext]
structure PolynomialMap (A : Type u) [CommSemiring A]
    (M : Type v₁) [AddCommMonoid M] [Module A M]
    (N : Type v₂) [AddCommMonoid N] [Module A N] where
  toFun (R : Type (max u v₁ v₂)) [CommSemiring R] [Algebra A R] : R ⊗[A] M → R ⊗[A] N
  isCompat {R : Type (max u v₁ v₂)} [CommSemiring R] [Algebra A R]
    {R' : Type (max u v₁ v₂)} [CommSemiring R'] [Algebra A R'] (φ : R →ₐ[A] R') :
    φ.toLinearMap.rTensor N ∘ toFun R =
      toFun R' ∘ φ.toLinearMap.rTensor M

[Adam Topaz]

Unfortunately, this would make the definition of comp somewhat more complicated if you want the most general universes possible.

[Antoine Chambert-Loir]

This quantification over all rings is necessary, but the restriction to the universes that you suggest may be enough.
(In practice, one just needs to take for R a ring of polynomials in finitely many coefficients over A).

[Adam Topaz]

Yes, I suspected that was the case (i.e. only needing polys in finitely many vars), but trying out slightly more restrictive universes caused other issues with the def of generize because \iota there was allowed to be in an arbitrary universe. I suppose a def with reasonable universe params would rather be

@[ext]
structure PolynomialMap (A : Type u) [CommSemiring A]
    (M : Type _) [AddCommMonoid M] [Module A M]
    (N : Type _) [AddCommMonoid N] [Module A N] where
  toFun (R : Type u) [CommSemiring R] [Algebra A R] : R ⊗[A] M → R ⊗[A] N
  isCompat {R : Type u} [CommSemiring R] [Algebra A R]
    {R' : Type u} [CommSemiring R'] [Algebra A R'] (φ : R →ₐ[A] R') :
    φ.toLinearMap.rTensor N ∘ toFun R =
      toFun R' ∘ φ.toLinearMap.rTensor M

[Adam Topaz]

This makes comp work out fine, but generize would have to be changed a bit.

[Adam Topaz]

In any case, I'm not actually seeing the universe issue pointed out above. Is it supposed to be at the comment labeled -- Universe issue !? The error i get by uncommenting that rw line is the following:

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ↑(generize A N m) f

[Antoine Chambert-Loir]

Indeed, the error appeared when I wanted to understand what was wrong and had changed rw [generize_comp_equiv f e m] to let H := generize_comp_equiv f e m.

[Adam Topaz]

Aha. I changed it to let... as you suggested, and got the following error:

stuck at solving universe constraint
  max u_1 ?u.693712 =?= max u_1 u_2
while trying to unify
  (PolynomialMap A M N) A inst✝¹⁰ M inst✝⁹ inst✝⁷ N inst✝⁸ inst✝⁶
with
  PolynomialMap A M N

This looks very similar to the universe unification issues we had in some parts of the category theory library!

[Adam Topaz]

And some more details:

stuck at solving universe constraint
  max u_1 ?u.694060 =?= max u_1 u_2
while trying to unify
  (PolynomialMap.{max ?u.694060 u_1, u_3, u_4, max ?u.694060 u_1} A M N) A inst✝¹⁰ M inst✝⁹ inst✝⁷ N inst✝⁸ inst✝⁶
with
  PolynomialMap.{max u_2 u_1, u_3, u_4, max u_2 u_1} A M N

[Adam Topaz]

The max is introduced in the declaration generize_comp_equiv

[Adam Topaz]

What I would recommend is to restrict the universe parameters of the rings involved to all be the same, which would mean changing the definition of PolynomialMap to be

@[ext]
structure PolynomialMap (A : Type u) [CommSemiring A]
    (M : Type _) [AddCommMonoid M] [Module A M]
    (N : Type _) [AddCommMonoid N] [Module A N] where
  toFun (R : Type u) [CommSemiring R] [Algebra A R] : R ⊗[A] M → R ⊗[A] N
  isCompat {R : Type u} [CommSemiring R] [Algebra A R]
    {R' : Type u} [CommSemiring R'] [Algebra A R'] (φ : R →ₐ[A] R') :
    φ.toLinearMap.rTensor N ∘ toFun R =
      toFun R' ∘ φ.toLinearMap.rTensor M

I think this should suffice for your applications?

Also, if possible I would restrict the universe parameter of the finite types you're using. Preferably they should all be in Type 0, if possible, and otherwise using Type u where the base ring is also in Type u should be fine.

What's the ultimate goal of this work?

[Antoine Chambert-Loir]

Polynomial maps are the algebraic gadgets that formalize polynomial maps from a module to another.
When the source module is a free module, what we should get is quite easy: essentially polynomials valued in the target module, but the definition is more intricate when the source is not free. Then, the definition proceeds by saying that polynomial maps $f \colon M \to N$ are just functorial families of maps $f_S \colon S \otimes_R M \to S \otimes_R N$ for all $R$-algebras $S$.
One first result (that follows from taking $S$ to be a ring of polynomials) shows that indeed, $f$ behaves as a polynomial on every finitely generated submodule, in the sense that for any finite family $(m_i)$, the image $f_S (\sum s_i \otimes m_i)$ is a polynomial $p_m$ in the $s_i$.

We are at the point where we need to express what it means for $f$ to be homogeneous: this means both that universally, the maps $f_S$ are homogeneous, and also that the polynomials $p_m$ are homogeneous.
Now, why doing all that ? Because our ultimate goal (at least, for what regards Mathlib) with @María Inés de Frutos Fernández is to fulfill @Kevin Buzzard 's wish that we formalize the theory of divided power structures.

One particularly delicate point of the theory is the construction of the divided power algebra of a module, and the divided power structure on its augmentation ideal. To that aim, it is necessary (at least, the only published proof works this way) to relate the graded pieces of the divided power algebra of a module to polynomial maps.

This also has a relation with the recent discussion about quadratic form, because in some sense, the piece of degree 2 of the divided power algebra of a module is the target of the “universal” quadratic form on that module.

[Kevin Buzzard]

I should say that this project has turned into a far bigger can of worms than I could have ever imagined, but conversely I'm certainly looking forward to the paper!

[Adam Topaz]

Yes, that's more-or-less what I gathered from your code, at least with regards to the polynomial maps. Anyway, since you only ever need to talk about $A$-algebras of the form $A[X_1,\ldots,X_n]$, I think you can impose the universe restrictions I mentioned above, including assuming that the finite types (which I assume will only be used to index the variables in your polynomial rings) live in Type 0. Adding such universe restrictions should eliminate the universe issues you were facing.

concerning divided powers, have you considered following an inductive approach similar to how the tensor algebra is defined here? https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean

You won't get an explicit description, but presumably the universal property is the main thing you need?

[Antoine Chambert-Loir]

Indeed. The definition of the divided powers is exactly defined as for the tensor algebra, with additional relations. We needed to add a lot of material to get the graded structure on the quotient.

[Antoine Chambert-Loir]

Thank you Adam for your help, with a more precise condition on the universes, I could finally rewrite the whole stuff,
and prove half of the theorem I had been struggling for many hours.
Just for fun, and to make Kevin slightly angry, this is proposition I.1 (page 226) in Roby's 1963 paper, and his proof is as follows:

La condition est trivialement suffisante. On voit qu'elle est nécessaire en prenant pour R une algèbre de polynômes.

(I just proved the “trivially sufficient” condition…)
image.png

[Antoine Chambert-Loir]

One remark before I go to bed: I had to fight a little bit with universes, because I needed to write a tensor $t \in S \otimes_R M$ as a finite linear combination of tensors, but the type of indices had to live in a given universe. Fortunately, starting with a linear combination indexed by Fin n, I could use ULift (Fin n) up to rewriting the sum along the equivalence given by docs#Equiv.ulift!

[Ruben Van de Velde]

Antoine Chambert-Loir said:

Thank you Adam for your help, with a more precise condition on the universes, I could finally rewrite the whole stuff,
and prove half of the theorem I had been struggling for many hours.
Just for fun, and to make Kevin slightly angry, this is proposition I.1 (page 226) in Roby's 1963 paper, and his proof is as follows:

La condition est trivialement suffisante. On voit qu'elle est nécessaire en prenant pour R une algèbre de polynômes.

(I just proved the “trivially sufficient” condition…)
image.png

And he didn't even have to fit his proof into a margin!

[Antoine Chambert-Loir]

;-)

[Eric Wieser]

Antoine Chambert-Loir said:

This also has a relation with the recent discussion about quadratic form, because in some sense, the piece of degree 2 of the divided power algebra of a module is the target of the “universal” quadratic form on that module.

Is there a canonical map out of this piece of degree 2 back to the original ring that doesn't multiply by the divided power (which is zero)? If not, then isn't the fact this is universal a proof that we're in trouble with a base change in char 2?