Deterministic timeout for class definition

Stream: general

[Eric Wieser]

I'm assuming I've either done something silly here that I've missed, or my lean installation is broken. Should this be expected to timeout?

import ring_theory.algebra
import linear_algebra

universes u1 u2 u3 u4

variables (R : Type u1) [comm_semiring R]
variables (M : Type u2) [add_comm_monoid M] [semimodule R M]

class tensor_algebra_class
  (T : Type u3) [semiring T] extends algebra R T :=
(to_fun' : M →ₗ[R] T)
-- (lift : Π {A : Type u4} [semiring A] [algebra R A], (M →ₗ[R] A) → (T →ₐ[R] A))

#print tensor_algebra_class

[Reid Barton]

I don't know what's going on, but I can tell you it times out for me too.

[Reid Barton]

Also, I'm quite confident you should use the same universe level for R, M, T, A.

[Mario Carneiro]

I suspect it has to do with the on the fly reconstruction of bits of the constructor into typeclasses in order to make things like semimodule R T work when you've only been given a bunch of fields. Making algebra R T a parameter fixes the issue

[Mario Carneiro]

a workaround:

structure tensor_algebra_mixin
  (T : Type u3) [semiring T] [algebra R T] :=
(to_fun' : M →ₗ[R] T)
-- (lift : Π {A : Type u4} [semiring A] [algebra R A], (M →ₗ[R] A) → (T →ₐ[R] A))

class tensor_algebra_class
  (T : Type u3) [semiring T] extends algebra R T :=
(mixin : tensor_algebra_mixin R M T)

[Eric Wieser]

Reid Barton said:

Also, I'm quite confident you should use the same universe level for R, M, T, A.

I'd disagree with this simply because algebra and module use different universe levels today.

[Reid Barton]

That is also a dubious, but more defensible choice

[Reid Barton]

Once you try to characterize an object by a universal property that quantifies over all other objects, it will become extremely unpleasant.

[Eric Wieser]

As in, once I uncomment lift?

[Reid Barton]

In the is_def_eq_detail trace I see stuff like

[type_context.is_def_eq_detail] [4]: algebra.to_semimodule._proof_5 =?= algebra.to_semimodule._proof_5
[type_context.is_def_eq_detail] [5]: _to_algebra =?= _to_algebra_1
[type_context.is_def_eq_detail] on failure: _to_algebra =?= _to_algebra_1
[type_context.is_def_eq_detail] unfold left&right: algebra.to_semimodule._proof_5
[type_context.is_def_eq_detail] [5]: (id
   ((((forall_congr_eq [... many more lines omitted]

[Reid Barton]

I understand _to_algebra is probably an instance argument of algebra.to_semimodule._proof_5, but still why is it doing this work to check a defeq between proofs?

[Sebastien Gouezel]

Mario Carneiro said:

a workaround:

structure tensor_algebra_mixin
  (T : Type u3) [semiring T] [algebra R T] :=
(to_fun' : M →ₗ[R] T)
-- (lift : Π {A : Type u4} [semiring A] [algebra R A], (M →ₗ[R] A) → (T →ₐ[R] A))

class tensor_algebra_class
  (T : Type u3) [semiring T] extends algebra R T :=
(mixin : tensor_algebra_mixin R M T)

Note that this is bad, as tensor_algebra_class has a parameter M which is not in algebra R T, so you should not extend it (unless I misunderstand something).

[Reid Barton]

Eric Wieser said:

it will become extremely unpleasant.

As in, once I uncomment lift?

Yes. You cannot quantify over universes so what you have defined is a u3-algebra T that satisfies a universal property with respect to all u4-algebras.

[Mario Carneiro]

@Sebastien Gouezel Ah, that's true, I didn't look at the original example carefully enough

[Mario Carneiro]

so you probably want the mixin version anyway

[Eric Wieser]

Thanks @Sebastien Gouezel, that's good advice

[Kevin Buzzard]

@Eric Wieser in the perfectoid project we thought we wanted to make a structure which involved quantifying over types in a random universe, but the type theory experts pointed out that we could just quantify over types in the same universe as part of our definition, and then prove the more general universal property as a theorem. My understanding was that you don't really want to be introducing new universe variables in your structures that can't be inferred from the inputs, but that was way back in 2019 before the fork and maybe things are better now

[Eric Wieser]

class tensor_algebra_class
  (T : Type u3) [semiring T] [algebra R T]:=
(to_fun' : M →ₗ[R] T)

works just fine

[Kenny Lau]

:four_leaf_clover: ?

[Kenny Lau]

(as in, will the typeclass system in Lean 4 be better?)

[Mario Carneiro]

:rainbow:

[Reid Barton]

I predict it will be better in at least some respects.

[Eric Wieser]

The motivation for A and T having different universes came from #3531, for which I'm trying to work out if a typeclass-style "Assume such a construction exists" type formalization can be used instead of assembling what to me seems like a rather uninteresting definition. That PR used different universes, so I figured I'd try the same

[Eric Wieser]

(although admittedly there tensor_algebra R M has universe max u1 u2 instead of my T which is u3)

[Reid Barton]

A and T having different universes just doesn't work

[Reid Barton]

because you cannot characterize an object by its maps into objects in another universe in general

[Reid Barton]

A and T having the same universe, distinct from R and M could work

[Adam Topaz]

Maybe I should mention that my initial construction of the tensor algebra is here:
https://gist.github.com/adamtopaz/84315ae5b11319013707b2d0804fb37e

Here I quantified over all types of some random universe when defining the relation, and got exactly the universe issues that Kevin mentioned.

[Reid Barton]

but it will just lead to strictly more headaches than simply putting everything in the same universe

[Reid Barton]

I mean, they will be different headaches.

[Eric Wieser]

Does the PR suffer from the same issue, where A is u3 and T = tensor_algebra R M is max u1 u2? Or is it exempt because the lemma using both universes does not attempt to be part of a type class?

[Kevin Buzzard]

We are doing mathematics here. In actual mathematics all our objects will be what ZFC people call sets, so in particular they will all be in the same universe. Universe polymorphism is important sometimes, but for definitions like this I don't think it is

[Reid Barton]

The PR is different because it is performing a construction

[Adam Topaz]

The universe level of tensor_algebra R M is the maximum of the universe levels of R and M, as it should be.

[Adam Topaz]

But the universal property is proved for maps into algebras with arbitrary universe levels.

[Eric Wieser]

@Adam Topaz, just to emphasize I'm super excited by your PR, and this is me trying to understand alternatives not criticise your approach :)

[Reid Barton]

also, someone can always come along and set u1 = u2 = u to get the plain case where the universes agree

[Reid Barton]

however, this will probably cause Lean some difficulties

[Mario Carneiro]

Kevin Buzzard said:

We are doing mathematics here. In actual mathematics all our objects will be what ZFC people call sets, so in particular they will all be in the same universe. Universe polymorphism is important sometimes, but for definitions like this I don't think it is

If you have as a component of your structure a lift into every set, then the structure isn't a set (in ZFC)

[Reid Barton]

because unification with universe levels of the form max ?u_1 ?u_2 is hard

[Kevin Buzzard]

Right, so in the perfectoid project our universal property in the definition stuck with the same universe and we proved a theorem afterwards saying it worked with different universes too

[Reid Barton]

(or at least, too hard for Lean's elaborator)

[Mario Carneiro]

Lean will not unify max ?u_1 ?u_2 = u anyway, it knows that max is not injective

[Mario Carneiro]

it will not unify max ?u_1 ?u_2 = max u v

[Eric Wieser]

Kevin Buzzard said:

we proved a theorem afterwards saying it worked with different universes too

Would you mind linking to that theorem?

[Kenny Lau]

the workaround to "having a function quantify over a universe in a component in the structure" is "don't"

[Reid Barton]

This comes up sometimes in the category theory library because there are a lot of constructions whose results live in various complicated universes, and I think there are even instances which are declared for the sole purpose of enabling instance search to guess the right values of universe levels.

[Reid Barton]

It's really just not worth dealing with these issues if you don't have to.

[Mario Carneiro]

Actually, I stand corrected, lean will unify max u v = max ?u ?v even though it really shouldn't

universes u v
def foo : Type (max u v) := sorry

variable (x : Type (max u v))
set_option pp.universes true
#check foo = x -- foo.{u v} = x : Prop

[Reid Barton]

Kevin, in the perfectoid space project, I think you only used a single universe variable at a time, right?

[Kenny Lau]

this max problem causes issues with cardinal.lift etc

[Reid Barton]

Reid Barton said:

A and T having the same universe, distinct from R and M could work

Oh I remembered the other issue, which is that with three general universe levels for R, M, A = T, your definition might "work", but be wrong!

[Patrick Massot]

@Adam Topaz if you start playing with universes, don't forget to git pull first because I just pushed two commits to your branch.

[Reid Barton]

The problem is if R lives in u1, M lives in u2, T lives in u3, and u3 is not at least max u1 u2, then there might not be enough interesting u3-R-algebras with a map from M to map T into

[Mario Carneiro]

so then you want A to live in max u1 u2 u3

[Reid Barton]

Because the actual tensor algebra will usually really live in universe max u1 u2, and so whatever the object T described by this universal property happens to be, it certainly can't be the correct tensor algebra (most likely, it simply doesn't exist).

[Reid Barton]

Right, you can do that, but then Lean is likely to never understand how to guess u3

[Mario Carneiro]

it's in the type of T though?

[Reid Barton]

Oh, A not T

[Eric Wieser]

Ah, I think I see your complaint now -u4 is part of the tensor_algebra_class type as I wrote it, not just part of the quantifier. Is that a correct interpretation?

[Reid Barton]

that could work, but then you can't even prove that two different tensor algebras T are isomorphic without jumping through a bunch of ulift hoops

[Mario Carneiro]

yeah it won't be pleasant

[Reid Barton]

and all of these issues could have been dealt with up front by ulift anyways

[Reid Barton]

by just moving R and M into the same universe

[Mario Carneiro]

I agree with Kenny's recommendation: avoid universe quantification in definitions

[Mario Carneiro]

if you can get an "internal" definition use that instead, and prove the universal property as a lemma

[Reid Barton]

Eric Wieser said:

Ah, I think I see your complaint now -u4 is part of the tensor_algebra_class type as I wrote it, not just part of the quantifier. Is that a correct interpretation?

Yes, it is a parameter of the class, and it is impossible to quantify over universe variables in a forall like this.

[Eric Wieser]

by just moving R and M into the same universe

What's the motivation for semimodule putting R and M into different universes?

[Mario Carneiro]

they are both parameters to semimodule

[Mario Carneiro]

the preferred default is to have all input types be in unconstrained universes and for the output type to be derived from the inputs. That way universe inference is always easy

[Mario Carneiro]

generally if you have two "unrelated" types, they should probably be in different universes

[Mario Carneiro]

but if you make a concrete definition like real, it should live in the lowest permissible universe

[Reid Barton]

There's plenty of stuff you can do with semimodule before the universe headaches start, and once they do you can just specialize to the same universe and it doesn't cost too much.

[Reid Barton]

And the definition is really correct for all possible pairs of universe levels

[Reid Barton]

and because things like real being in a fixed universe Type 0, which penalizes the "just use a single universe and save yourself a lot of bother" approach, there's a range of applications where it's more convenient to allow distinct universes because it avoids ulift

[Reid Barton]

but as soon as you would have to use ulift anyways to prove things like "two objects with the same universal property are isomorphic" then it's no longer worth keeping it up

[Reid Barton]

For another example, I think the usual definition of a projective module as "lifts against surjections" is wrong when the module's universe is less than the ring's universe.

[Reid Barton]

And also, what Kevin said earlier. In real math, even if the objects are not just sets, we can always move them into the same universe and work there, and this is what people do. If supporting extra universe generality in the formalization doesn't cause any headaches, then great, but if it does, then it's just not worth it to create actual extra math problems for yourself.

[Reid Barton]

(Unless of course you're specifically interested in those problems, similarly to proving something constructively for its own sake.)

[Mario Carneiro]

Also it's worth noting that working with everything in the same universe is no loss of generality since you can always pick a universe large enough and then ulift everything. So moving to one-universe is just deferring the ulift to the application rather than the theory

[Kevin Buzzard]

A valuation on a ring R is a pair(Gamma,v) where Gamma is a (certain kind of) monoid and v : R -> Gamma is a map with some properties. We initially let Gamma be in a different universe to R. Let M(v) be the image of v; this is a submonoid. Two valuations v1 and v2 are _equivalent_ if there's an isomorphism M(v1)=M(v2) making the diagram commute. We only cared about valuations up to equivalence.

[Kenny Lau]

@Kevin Buzzard why not define it as an "ordered congruence" on R?

[Kevin Buzzard]

We wanted that the type of equivalence class of valuations on R lived in the same universe as R. This was problematic for two reasons. Firstly, we had let Gamma vary through all universes, and secondly, even if we restricted to one universe, the equivalence classes bumped the universe level up by one.

We solved both of these problems at the same time and it might be difficult to see the wood from the trees. In the perfectoid project the relevant files are valuation.basic and valuation_spectrum. The bump-universe-by-one issue is solved using a binary relation on R, and the universe issue was solved by only considering valuations taking values in monoids living in the same universe as R, and then proving that if we had a valuation R -> Gamma where Gamma was in some different universe to R, then there was an equivalent valuation taking values in some Gamma' in the same universe as R. We did this by using the first isomorphism theorem: R/equiv-coming-from-v is isomorphic to im(v), and R/equiv-coming-from-v lives in the same universe as R.

[Kevin Buzzard]

@Kenny Lau this is what we did in the end, but this was not because of the universe issue we're talking about, this was for a different universe issue.

[Utensil Song]

My takeaway:

1. We should avoid using different universes in our (concrete) theory development without loss of generality since the chosen universe could be a sufficiently large one as pointed out by @Mario Carneiro .
2. We could use different universes when PRing mathlib but we should follow rules pointed out by @Mario Carneiro , and if we encounter any headaches about universes we could use the specializing strategy suggested by @Reid Barton and it should be good enough for most interesting math.
3. Using the same universe for the definitions doesn’t stop us from proving that the theorems work for different universes later as long as the math allows the constructs to be dragged into the same universe as done in perfectoid project by @Kevin Buzzard et al.
4. The discussions above make a great library note worth PRing.

[Utensil Song]

1 is good enough for justifying using the same universe. I was just curious about how it could be relaxed later after fixing the same universe in 3 and it’s now perfectly explained.

[Utensil Song]

(deleted)

[Adam Topaz]

Concerning this specific construction--

When I originally made the construction in the "universal" way, i.e. using the following relation:

def rel : (pre R M) → (pre R M) → Prop := λ x y,
  ∀ (A : Type*) (h1 : ring A), by letI := h1; exact
  ∀ (h2 : algebra R A), by letI := h2; exact
  ∀ (f : M →ₗ[R] A),
  (lift_fun R M f) x = (lift_fun R M f) y

I obtained a construction tensor_algebra.{u1 u2 u3} with three universe levels. The u1 is the universe level of R, the u2 is the one of M and the u3 is the one of A appearing in the definition of rel.

But note that tensor_algebra.{u1 u2 u3} R M : Type (max u1 u2).

The issue with this is that the universal property (which is true "by construction" in this case) could only be easily proved for R-algebras whose underlying type has universe level u3. So as Reid, Kevin, and others mentioned, one would have had to prove the existence of some isomorphism between these objects for varying u3, and in particular for u3 = max u1 u2. It seemed much easier to just change the definition of rel to what it is now in #3531

[Eric Wieser]

Unrelated to your point, but... is the by letI := ...; exact a workaround for something I haven't run into yet?

[Adam Topaz]

It's a trick that @Johan Commelin told me about that lets you introduce instances in term mode.

[Adam Topaz]

But it's not really term mode.

[Bryan Gin-ge Chen]

There's some information about the fooI tactics here.

[Eric Wieser]

Does the following not work there to avoid needing letI?

def rel : (pre R M) → (pre R M) → Prop := λ x y,
  ∀ (A : Type*) [ring A] [algebra R A]
  (f : M →ₗ[R] A),
  (lift_fun R M f) x = (lift_fun R M f) y

[Adam Topaz]

This doesn't work.

[Adam Topaz]

The following emoji has been mentioned in relation to this: :four_leaf_clover:

[Mario Carneiro]

You want exactI, not letI here

[Mario Carneiro]

def rel : (pre R M) → (pre R M) → Prop := λ x y,
  ∀ (A : Type*) [ring A] [algebra R A], by exactI
  ∀ (f : M →ₗ[R] A),
  (lift_fun R M f) x = (lift_fun R M f) y

[Adam Topaz]

Oh nice!

[Adam Topaz]

So exactI just picks up all the instances in context?

[Mario Carneiro]

yep