Quantifier over all type / universe

Stream: new members

[Weiyi Wang]

Not sure if the title makes sense, but this is the first time I run into universe problem and can't just write Type* and call it a day...

I am translating some theory about maximally complete field. I translated the definition as follows

import Mathlib

variable {K : Type*} [Field K]
variable {Γ : Type*} [LinearOrderedCommGroupWithZero Γ] (V : Valuation K Γ)
variable {L : Type*} [Field L]
variable {Γ' : Type*} [LinearOrderedCommGroupWithZero Γ'] (V' : Valuation L Γ')
variable [Algebra K L] [Valuation.HasExtension V V']

-- This definition is not important. Just certain property about the extension of valuation
def IsImmediate : Prop := Set.range V' = V' '' (⊥ : Subalgebra K L)
  ∧ Function.Surjective (IsLocalRing.ResidueField.map (algebraMap V.integer V'.integer))

-- "If field K admits no proper immediate extensions, K is said to be maximal"
def IsMaximal := ∀ (L Γ' : Type*) (_ : Field L) (_ : LinearOrderedCommGroupWithZero Γ')
  (V' : Valuation L Γ') (_ : Algebra K L) (_ : Valuation.HasExtension V V')
  (_ : IsImmediate V V'), Function.Surjective (algebraMap K L)

-- I'd like to prove a theorem with a goal ¬IsMaximal V
theorem foo (h : False) : ¬IsMaximal V := by
  simp [IsMaximal]
  -- I'd like to give an example that's a proper immediate extension, using K[X] as an example
  use Polynomial K
  /-
Application type mismatch: The argument
  K
has type
  Type u_1
of sort `Type (u_1 + 1)` but is expected to have type
  Type u_5
of sort `Type (u_5 + 1)` in the application
  @Polynomial K
  -/
  sorry

In the definition IsMaximal, I'd like to express "for all field L that's an extension of K...", which leads to the quantifier over type. I wrote Type* there without thinking much. But later on, I realized that when I want to provide an example field, it is not necessarily in the universe defined by Type*.

Maybe I should enforce that in IsMaximal, K and L should be from the same universe? That would allow me to proceed with the proof, but would that mean it isn't a real quantification over all fields? I feel I am trying to write "for all universes", but that's not a thing in Lean, is it?

[Aaron Liu]

the problem is that "all fields" is a proper class so quantifying over it can lead to set-theoretic type-theoretic difficulties

[Aaron Liu]

usually when this happens there's a better definition that doesn't quantify over a proper class or sometimes it suffices to stop looking after a certain cardinality

[Aaron Liu]

for example, your IsImmediate seems to be wanting that a certain map is surjective, so perhaps if the big field is too big you can never be surjective and so you don't have to worry about too big fields

[Weiyi Wang]

I see. I haven't come up with an alternative definition yet. I think I'll restrict them to be in the same universe and see how far I can go

[Andrew Yang]

Another common theme is you can prove something like "if it is not maximal there exists a larger one in Type max u v", so you can make the definition quantify over Type max u v and provide a constructor that takes in arbitrary Type _.

[Stepan Nesterov]

Weiyi Wang said:

I see. I haven't come up with an alternative definition yet. I think I'll restrict them to be in the same universe and see how far I can go

Can you say something like "$K$ is v-maximal if for all fields in universe v ..." and then have a theorem with universe parameters v and w the properties of being v-maximal and w-maximal are equivalent?

[Aaron Liu]

You can do that but then you have to use that theorem whenever you want to change universes

[Weiyi Wang]

The literature I am reading introduces a lemma to bound the cardinality of the field (card(K) <= card(ResidueField) ^ card(Γ)). I wonder if it is going to effectively say that the field to look for is within a certain universe. Haven't finished reading yet

[Aaron Liu]

If it's below the next inaccessible cardinal then you're in the same universe as the largest of all the things in the formula

[Aaron Liu]

This bounds the universe to max(universe of residue field, universe of Gamma)

[Kevin Buzzard]

@Weiyi Wang I know the literature is full of Valuations but mathematicians are very good at moving between equivalent valuations in a transparent way, and this is harder in Lean. If I were setting up the theory of immediate extensions then I would be strongly tempted to use docs#ValuativeRel instead of Valuation and docs#ValuativeExtension instead of Valuation.HasExtension. The point is that you do not really care what $\Gamma$ is, and in particular even though your code is universe polymorphic (as is the custom here) you definitely don't care what universe $\Gamma$ is in, not least because it can be replaced with the image of $K$ giving an equivalent valuation in the same universe as $K$. A ValuativeRel on a field is exactly the same thing as an equivalence class of valuations so for any mathematics where you only care about valuations up to equivalence (which is the case here) you should make your life easier by removing $\Gamma$ completely from the definitions, and if you want $\Gamma$ then you should use ValuativeRel.valuation, which takes values in ValueGroupWithZero K, a totally ordered group with 0 in the same universe as K.

This solves one of your universe problems in IsMaximal, but not the other one, because you still want to quantify over all extensions L. The trick for this case is to only quantify over fields L in the same universe as K in the definition, and then if you actually care about universes then prove that being maximal is the same as "for all L in all universes, K=L". Definitions should not involve extra types being quantified over in random universes, because it is not possible to say "for all universes" in Lean (this is a foundational issue) and what you are actually making is infinitely many definitions, some of which are mathematically meaningless (you might be quantifying over all fields in a smaller universe than K, so K will turn out to be maximal for the stupid reason that no such K-fields exist because the universe is too small). You are also making a footgun for yourself because whenever you don't specify the universe of the field being quantified over you are asking Lean to figure it out itself, and universe unification in these situations can lead to very weird and hard-to-diagnose timeouts.

[Weiyi Wang]

If I were setting up the theory of immediate extensions then I would be strongly tempted to use docs#ValuativeRel instead of Valuation and docs#ValuativeExtension instead of Valuation.HasExtension

I am really glad you said this. I suspected this after already writing a bunch of it but didn't have the courage to rewrite it. Now I have more motivation to do it

[Kevin Buzzard]

Let us know pain points in the rewrite! There are still parts of mathlib which need converting but ValuativeRel seems to be working fine in e.g. the theory of nonarchimedean local fields (see e.g. https://github.com/kbuzzard/ClassFieldTheory/blob/main/ClassFieldTheory/IsNonarchimedeanLocalField/Basic.lean )

[Aaron Liu]

Kevin Buzzard said:

The trick for this case is to only quantify over fields L in the same universe as K in the definition, and then if you actually care about universes then prove that being maximal is the same as "for all L in all universes, K=L".

I really don't like this either because then if you don't know the library so you unfold the definition to try to prove things with it then you're not universe general. I just feel like it's best to avoid quantifying over Type _ lest you start getting stuff like docs#Module.injective_iff which isn't universe general.

[Kevin Buzzard]

In which case the answer is to find a characterisation of being maximal (in the sense of valuation theory) which doesn't involve quantifying over anything. For example we did this with being a localization -- the universal property for $f:R\to A$ being a localisation at $S$ is that for all $B$ and $R\to B$ sending $S$ to units, we get a unique $A\to B$ making the diagram commute. However mathlib's definition of the predicate is: "$f(s)$ is a unit for all $s$, every $a\in A$ is of the form $f(r)/f(s)$ and $ker(f)$ is the annihilator of $S$". Neil Strickland had the insight here. Maybe you need another insight to come with a more mathlib-appropriate definition of IsMaximal.

[Stepan Nesterov]

Is the ideal situation to have two theorems

theorem no_immediate_of_maximal (K : Type*) (L : Type*) : IsMaximal K → IsImmediate L → L = K
theorem maximal_of_no_immediate (K : Type u) : (∀ L : Type u, IsImmediate L → L = K) → IsMaximal K

where the first refers secretly to L in all universes, and the second forces K and L to be the same universe?

[Aaron Liu]

I would say make maximal_of_no_immediate also not quantify over Type u but rather something smaller like IntermediateField K (AlgClosure K) or whatever you need to be able to prove the theorem

[Weiyi Wang]

Well, at least I know AlgebraicClosure is not large enough, because the I already showed that there can be transcendental immediate extension. Immediate extension seems to form a really large closure. But I get your point, and I'll try this way for other theories

[Kevin Buzzard]

We know that the mathematical notion has nothing to do with universes so no_immediate_of_maximal must be true but I don't know a maths proof (but I didn't look for one -- no doubt any proof that any explicit field is maximal will turn into one).

Interestingly, I do think that the mathematical community plays a little fast and loose with size issues in this area. In Wedhorn's adic spaces article he defines the set of equivalence classes of valuations on a commutative ring but without knowing about ValuativeRel it wasn't obvious (at least ro me) why this was a set (certainly the collection of all valuations on a commutative ring is not a set).

[Kenny Lau]

@Weiyi Wang This is the first time I'm reading this thread, so I'm sure all of what I have to say has already been said. When you translate something to Lean, it isn't always very straightforward, and you shouldn't just stick to one definition without thinking. As you've discovered, this universe issue is particularly important.

Now I've talked to people who are fine with things like AlgebraicClosure K living in one universe higher than K, and I consider them to be lunatics, and they also consider me to be a lunatic. (all jokes btw)

So you should first construct something in the same universe of K with a very ugly definition that will be the completion of K (wait, don't we have that already?), and then prove that for any L in any other universe, L maps to the completion of K. This is how you solve the unvierse problem in type theory. You should view the cardinality bound in set theory as the analogue of the universe problem in type theory.

And then secondly I saw that someone pointed out ValuativeRel before. This is another piece of new Mathlib object that is the result of careful consideration of paper maths. This is the cornerstone of the valuation library in Mathlib and you should definitely use it instead of an arbitrary Valuation.

In other words, maybe next time you can phrase your question as "here's a definition i tried, should I try another definition?" instead of "here's the definition i have, i'm running into all these problems, lean is broken" (I know you didn't actually say this)

[Kevin Buzzard]

Kenny this is not about completions, it is more subtle mathematically.

[Kenny Lau]

I apologise, I've read more now. So now my approach would be:

• First define an arbitrary maximal completion of any given field with valuative rel (Cor 6 by Poonen). Note that this is not unique, and note that at this point I have deliberately not introduced the predicate IsMaximallyComplete!
• Then define the predicate to mean that the map K -> MaximalCompletion K is surjective. Note that I have not quantified over any universe in this definition!
• Now prove the theorem that if K is maximally complete, then it satisfies the textbook definition (which does quantifier over all universes, and is allowed in a statement but not a definition)

[Kevin Buzzard]

Aah (from that pdf), apparently Krull showed that there's a bound on the cardinality of a valued field with a given value group and residue field, which would resolve all universe issues. Note that this must have a little content, e.g. the p-adic numbers are an uncountable field with countable value group and finite residue field.

[Kevin Buzzard]

Screenshot from 2025-11-14 18-34-03.png

(the dagger is just the footnote "if S is a set then |S| is the cardinality of S")

[Kenny Lau]

the cardinality bounds might not be very helpful for now, unless we do an explicit approach like what another theorem prover did, with "now let's consider all the possible ring structures on this type"; such as this glorious proof in Stacks project that alg closure exists

[Kevin Buzzard]

Oh they are helpful, because the technique of the paper shows the following result: if K is a valued field, with value group Gamma and residue field R (in the same universe as K because they're subquotients of K), and if L is an immediate extension of K which might live in some much bigger universe, then there's an injection L -> (Gamma -> R), and hence L bijects with a subtype of something in K's universe giving us an isomorphism of L with a field in the same universe as K and thus proving that "no immediate extensions in K's universe" implies "no immediate extensions in any higher universe".