universe issue

Stream: maths

[Calle Sönne]

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]

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]

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]

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]

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]

Whereas:

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

[Scott Morrison]

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

[Adam Topaz]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Adam Topaz]

Yeah, but:

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

[Scott Morrison]

oh!

[Scott Morrison]

lame :-)

[Adam Topaz]

Indeed

[Adam Topaz]

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]

(or something similaar)

[Scott Morrison]

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

[Scott Morrison]

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

[Adam Topaz]

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

[Adam Topaz]

I suspect this is the source of the original issue anyway

[Scott Morrison]

Ok, I'm fixing.

[Scott Morrison]

#6300

[Adam Topaz]

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

[Adam Topaz]

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 :=
{ to_is_right_adjoint := ⟨CompHaus.to_Profinite.{u u}, Profinite.to_Profinite_adj_to_CompHaus⟩ }

[Adam Topaz]

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]

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

[Adam Topaz]

Sounds good to me ( I commented on github also )