## Stream: maths

### Topic: universe issue

#### Calle Sönne (Feb 18 2021 at 20:59):

Is this expected behaviour?

import topology.category.Profinite

namespace category_theory

universes v u

set_option pp.universes true

example : reflective Profinite.to_CompHaus.{max u v} := by apply_instance -- works

example : reflective Profinite.to_CompHaus := by apply_instance -- fails

end category_theory


#### Adam Topaz (Feb 18 2021 at 22:18):

The error with this code hopfully will provide a better hint as to what's going wrong:

import topology.category.Profinite

namespace category_theory

set_option pp.universes true

universes u

def foo : reflective Profinite.to_CompHaus.{u} := Profinite.to_CompHaus.reflective

end category_theory


#### Adam Topaz (Feb 18 2021 at 22:18):

9:51: type mismatch, term
Profinite.to_CompHaus.reflective.{?l_1 ?l_2}
has type
reflective.{(max ?l_1 ?l_2) (max ?l_1 ?l_2) (max ?l_1 ?l_2)+1 (max ?l_1 ?l_2)+1}
Profinite.to_CompHaus.{(max ?l_1 ?l_2)} : Type ((max ?l_1 ?l_2)+1)
but is expected to have type
reflective.{u u u+1 u+1} Profinite.to_CompHaus.{u} : Type (u+1)


#### Adam Topaz (Feb 18 2021 at 22:21):

This works:

import topology.category.Profinite

namespace category_theory

set_option pp.universes true

universes u

def foo : reflective Profinite.to_CompHaus.{u} := Profinite.to_CompHaus.reflective.{u u}

end category_theory


#### Adam Topaz (Feb 18 2021 at 22:25):

Right, so it looks like Profinite.to_CompHaus.reflective has the following type with full universe annotation:

Profinite.to_CompHaus.reflective.{u_1 u_2} :
reflective.{(max u_1 u_2) (max u_1 u_2) (max u_1 u_2)+1 (max u_1 u_2)+1} Profinite.to_CompHaus.{(max u_1 u_2)}


#### Adam Topaz (Feb 18 2021 at 22:26):

Whereas:

Profinite.to_CompHaus.reflective.{u u} : reflective.{u u u+1 u+1} Profinite.to_CompHaus.{u}


#### Scott Morrison (Feb 18 2021 at 22:47):

Why does Profinite.to_CompHaus.reflective have two universe variables to begin with?

#### Adam Topaz (Feb 18 2021 at 22:50):

I think docs#Profinite.to_CompHaus is to blame for that

#### Scott Morrison (Feb 18 2021 at 22:50):

Oh, I see, it allows different universe levels for the source and target.

#### Scott Morrison (Feb 18 2021 at 22:50):

def CompHaus.to_Profinite : CompHaus ⥤ Profinite := ...

#### Adam Topaz (Feb 18 2021 at 22:51):

Yeah, but:

121:1: CompHaus.to_Profinite.{u_1 u_2} : CompHaus.{(max u_1 u_2)} ⥤ Profinite.{(max u_1 u_2)}


oh!

lame :-)

Indeed

#### Adam Topaz (Feb 18 2021 at 22:52):

I'm a bit surprised it's not

CompHaus.to_Profinite.{u_1 u_2} : CompHaus.{u_1} ⥤ Profinite.{(max u_1 u_2)}


#### Adam Topaz (Feb 18 2021 at 22:52):

(or something similaar)

#### Scott Morrison (Feb 18 2021 at 22:53):

Would that be more useful than just a constant universe level?

#### Scott Morrison (Feb 18 2021 at 22:54):

I'm generally wary of adding universe lifts in the midst of something else.

#### Adam Topaz (Feb 18 2021 at 22:54):

I don't know. Certainly the current version may as well restrict to the same universe level

#### Adam Topaz (Feb 18 2021 at 22:54):

I suspect this is the source of the original issue anyway

Ok, I'm fixing.

#6300

#### Adam Topaz (Feb 18 2021 at 22:58):

Hmmm.... it looks like the original issue remains even with this change

#### Adam Topaz (Feb 18 2021 at 22:59):

With this change it works:

/-- The category of profinite sets is reflective in the category of compact hausdroff spaces -/
instance Profinite.to_CompHaus.reflective : reflective Profinite.to_CompHaus :=


#### Adam Topaz (Feb 18 2021 at 23:02):

Or with this one:

def Profinite.to_CompHaus_equivalence (X : CompHaus.{u}) (Y : Profinite.{u}) :
(CompHaus.to_Profinite_obj X ⟶ Y) ≃ (X ⟶ Profinite.to_CompHaus.obj Y) :=
{ to_fun := λ f,
{ to_fun := f.1 ∘ quotient.mk,
continuous_to_fun := continuous.comp f.2 (continuous_quotient_mk) },
inv_fun := λ g,
{ to_fun := continuous.connected_components_lift g.2,
continuous_to_fun := continuous.connected_components_lift_continuous g.2},
left_inv := λ f, continuous_map.ext $λ x, quotient.induction_on x$ λ a, rfl,
right_inv := λ f, continuous_map.ext \$ λ x, rfl }


#### Scott Morrison (Feb 18 2021 at 23:15):

I like the second one. Shall I add it to the PR?

#### Adam Topaz (Feb 18 2021 at 23:16):

Sounds good to me ( I commented on github also )

Last updated: May 10 2021 at 08:14 UTC