## Stream: general

### Topic: understanding universe error

#### Chase Fleming (Sep 07 2022 at 03:03):

Hello, I'm trying to define proper maps but am running into a universe error. I don't know much about universes, can anyone help me decipher it?

#### Matt Diamond (Sep 07 2022 at 03:35):

could you provide a #mwe?

#### Chase Fleming (Sep 07 2022 at 03:41):

variables {α : Type*} {β : Type*} {γ : Type*}
variables [topological_space α] [topological_space β] [topological_space γ]

structure proper_map (f: α → β) : Prop :=
(is_univ  : ∀ z, topological_space z → is_closed_map (prod.map (@id z) f))
(is_cont  : continuous f)


The following lemma highlights the issue

lemma comp_proper {f: α → β} {g: β → γ} (hf: proper_map f) (hg: proper_map g) : proper_map (g ∘ f) :=
begin
constructor,
{
rintro z hz,
change is_closed_map (prod.map (id ∘ id) (g ∘ f)),
rw ←prod.map_comp_map,
obtain h' := hf.1 z,
},
{
exact continuous.comp hg.is_cont hf.is_cont,
}
end


We see that the error comes with obtain h' line as we get

type mismatch at application
hf.is_univ z
term
z
has type
Type u_6 : Type (u_6+1)
but is expected to have type
Type u_4 : Type (u_4+1)


I do not know enough about universes to make sense of this.

#### Chase Fleming (Sep 07 2022 at 03:42):

and sorry, I forgot my imports

import topology.maps
import topology.constructions

universes u v


#### Matt Diamond (Sep 07 2022 at 03:55):

this probably won't do it, but I wonder if changing the Type*s to Type u might help, or at least lead to a clearer error message

#### Matt Diamond (Sep 07 2022 at 04:00):

actually, if you do that (changing the types to use the universe variable u) and then change the type of is_univ to ∀ (z : Type u), topological_space z → is_closed_map (prod.map (@id z) f), that seems to fix the universe error

#### Matt Diamond (Sep 07 2022 at 04:01):

it works because it explicitly specifies the universe level of the z argument

#### Chase Fleming (Sep 07 2022 at 04:03):

So, that's what I did, and I'm not getting anything bad yet except i'm getting a goal of topological_space (z × α) when I attempt the final exact even though we have both \a and z being topological_spaces.

#### Matt Diamond (Sep 07 2022 at 04:07):

I see... I don't think I can really help you with that part, but I'm sure someone more knowledgeable will come along

#### Junyan Xu (Sep 07 2022 at 04:07):

If you do

set_option pp.universes true
#check @proper_map


you'll see

proper_map.{u_4 u_5 u_6} :
Π {α : Type u_4} {β : Type u_5} [_inst_1 : topological_space.{u_4} α] [_inst_2 : topological_space.{u_5} β],
(α → β) → Prop


where u_6 is the universe variable of z in is_univ. Since this is a free variable, it becomes three independent free variables in hf, hg and the conclusion, as you can see from

hf: proper_map.{u_1 u_2 u_4} f
hg: proper_map.{u_2 u_3 u_5} g
z: Type u_6


The way to solve this is indeed to specify variables explicitly: setting the universes of α, β and z to be the same as suggested by @Matt Diamond is definitely reasonable. I'm not sure what you should set z to if {α : Type u} {β : Type v} what should be the type of z; I think z : Type (max u v) would probably allow you to derive is_closed_map in all universes, or maybe even z : Type 0 suffices?

In general it's not recommended to quantify over (all types in) a universe in a definition, and for proper maps there are two other definitions that doesn't use such quantification; however they're only equivalent to your definition under certain conditions, so your definition is still worth having.

#### Junyan Xu (Sep 07 2022 at 04:07):

I think you can solve the topological_space (z × α) goal using apply_instance

#### Chase Fleming (Sep 07 2022 at 04:09):

@Junyan Xu You are fantastic. Allow me to read over this and apply it.

#### Junyan Xu (Sep 07 2022 at 04:20):

This works for me, no need of apply_instance:

import topology.constructions

universe u
variables {α β γ : Type u}
variables [topological_space α] [topological_space β] [topological_space γ]

structure proper_map (f: α → β) : Prop :=
(is_univ : ∀ z : Type u, topological_space z → is_closed_map (prod.map (@id z) f))
/- (is_univ : ∀ (z : Type u) [topological_space z], is_closed_map (prod.map (@id z) f)) seems
better; would allow you to write (hg.is_univ z).comp ... below without the underscore. -/
(is_cont : continuous f)

lemma comp_proper {f : α → β} {g : β → γ} (hf : proper_map f) (hg : proper_map g) :
proper_map (g ∘ f) :=
begin
constructor,
{ introsI z hz,
/- introsI puts hz inside the instance cache, so the topological_space (z × α) can
be automatically inferred. -/
exact (hg.is_univ z _).comp (hf.is_univ z _) },
{ exact continuous.comp hg.is_cont hf.is_cont },
end


#### Chase Fleming (Sep 07 2022 at 04:27):

Aha, I was just coming back to ask something about the error. Thank you so much for that explanation of why you use introsI

#### Jireh Loreaux (Sep 07 2022 at 20:00):

Chase, when you get around to it, could you please provide results connecting proper maps to docs#cocompact_map under the appropriate conditions?

Last updated: Aug 03 2023 at 10:10 UTC