understanding universe error

Stream: general

[Chase Fleming]

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]

could you provide a #mwe?

[Chase Fleming]

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]

and sorry, I forgot my imports

import topology.maps
import topology.constructions

universes u v

[Matt Diamond]

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]

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]

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

[Chase Fleming]

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]

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]

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]

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

[Chase Fleming]

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

[Junyan Xu]

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]

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]

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