Zulip Chat Archive

Stream: maths

Topic: universe issue


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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)}

view this post on Zulip 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}

view this post on Zulip Scott Morrison (Feb 18 2021 at 22:47):

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

view this post on Zulip Adam Topaz (Feb 18 2021 at 22:50):

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

view this post on Zulip Scott Morrison (Feb 18 2021 at 22:50):

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

view this post on Zulip Scott Morrison (Feb 18 2021 at 22:50):

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

view this post on Zulip 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)}

view this post on Zulip Scott Morrison (Feb 18 2021 at 22:51):

oh!

view this post on Zulip Scott Morrison (Feb 18 2021 at 22:51):

lame :-)

view this post on Zulip Adam Topaz (Feb 18 2021 at 22:51):

Indeed

view this post on Zulip 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)}

view this post on Zulip Adam Topaz (Feb 18 2021 at 22:52):

(or something similaar)

view this post on Zulip Scott Morrison (Feb 18 2021 at 22:53):

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

view this post on Zulip Scott Morrison (Feb 18 2021 at 22:54):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Feb 18 2021 at 22:54):

I suspect this is the source of the original issue anyway

view this post on Zulip Scott Morrison (Feb 18 2021 at 22:56):

Ok, I'm fixing.

view this post on Zulip Scott Morrison (Feb 18 2021 at 22:56):

#6300

view this post on Zulip Adam Topaz (Feb 18 2021 at 22:58):

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

view this post on Zulip 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 :=
{ to_is_right_adjoint := CompHaus.to_Profinite.{u u}, Profinite.to_Profinite_adj_to_CompHaus }

view this post on Zulip 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 }

view this post on Zulip Scott Morrison (Feb 18 2021 at 23:15):

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

view this post on Zulip 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