# Zulip Chat Archive

## Stream: general

### Topic: category theory universe issue?

#### Kevin Buzzard (Apr 14 2019 at 18:15):

**question in progress -- ignore for now unless you're Scott**

I am using a slightly modified mathlib but I am hoping this isn't the issue [update: it is]. The following innocuous-looking code:

import topology.opens import category_theory.functor import category_theory.instances.Top open category_theory.instances universes v u variables {α : Type*} {β : Type*} [topological_space α] [topological_space β] {f : α → β} open topological_space theorem is_open_map_of_open {α : Type*} [topological_space α] {s : set α} (hs : _root_.is_open s) : is_open_map (subtype.val : {x // x ∈ s} → α) := begin rintros _ ⟨t, ht, rfl⟩, convert is_open_inter _ _ _ ht hs, rw set.image_preimage_eq_inter_range, convert rfl, exact (set.range_coe_subtype s).symm end def is_open_map.map (h : is_open_map f) : opens α → opens β := λ U, ⟨f '' U.1, h U.1 U.2⟩ def functor.is_open_map.map (h : is_open_map f) : opens α ⥤ opens β := { obj := is_open_map.map h, map := λ X Y hXY x ⟨a, ha, ha'⟩, begin rw ←ha', use a, exact ⟨hXY ha, rfl⟩ end, map_id' := λ _, rfl, map_comp' := λ _ _ _ _ _, rfl } def inclusion (X : Top.{v}) (U : opens.{v} X) : opens.{v} ({x // x ∈ U.val}) ⥤ opens.{v} X := functor.is_open_map.map.{v v} (is_open_map_of_open U.2)

doesn't work. First I show that the inclusion of an open set is an open map. Then I define a function `opens alpha -> opens beta`

from an open map alpha -> beta. Then I beef it up into a functor. Then I try and apply it in the situation of an open map. I get an error in the def of `inclusion`

, a type mismatch hundreds of lines long because `pp.all`

has been switched on by Lean.

The two terms look identical other than in one small place: diff output is

< (@topological_space.opens.opens_category X) --- > (@category_theory.preorder_category > (@topological_space.opens > (@coe_sort category_theory.instances.Top (@category_theory.bundled.has_coe_to_sort topological_space) X) > (category_theory.instances.topological_space_unbundled X)) > (@partial_order.to_preorder > (@topological_space.opens > (@coe_sort category_theory.instances.Top (@category_theory.bundled.has_coe_to_sort topological_space) X) > (category_theory.instances.topological_space_unbundled X)) > (@topological_space.opens.partial_order > (@coe_sort category_theory.instances.Top (@category_theory.bundled.has_coe_to_sort topological_space) X) > (category_theory.instances.topological_space_unbundled X))))

I then attempt to verify that these terms are the same:

def inclusion (X : Top.{v}) (U : opens X) : opens ({x // x ∈ U.val}) ⥤ opens X := --functor.is_open_map.map (is_open_map_of_open U.2) begin have H : (@topological_space.opens.opens_category X) = (@category_theory.preorder_category (@topological_space.opens (@coe_sort category_theory.instances.Top (@category_theory.bundled.has_coe_to_sort topological_space) X) (category_theory.instances.topological_space_unbundled X)) (@partial_order.to_preorder (@topological_space.opens (@coe_sort category_theory.instances.Top (@category_theory.bundled.has_coe_to_sort topological_space) X) (category_theory.instances.topological_space_unbundled X)) (@topological_space.opens.partial_order (@coe_sort category_theory.instances.Top (@category_theory.bundled.has_coe_to_sort topological_space) X) (category_theory.instances.topological_space_unbundled X)))), exact functor.is_open_map.map (is_open_map_of_open U.2), end

and this time the error (in the definition of `H`

) is:

type mismatch at application opens.opens_category = category_theory.preorder_category (opens ↥X) term category_theory.preorder_category (opens ↥X) has type category_theory.category.{0 v+1} (@topological_space.opens.{v} (@coe_sort.{v+2 v+2} category_theory.instances.Top.{v} (@category_theory.bundled.has_coe_to_sort.{v+1 v+1} topological_space.{v}) X) (category_theory.instances.topological_space_unbundled.{v} X)) : Type v but is expected to have type category_theory.category.{v+1 (max (v+1) 1)} (@topological_space.opens.{v} (@coe_sort.{v+2 v+2} category_theory.instances.Top.{v} (@category_theory.bundled.has_coe_to_sort.{v+1 v+1} topological_space.{v}) X) (category_theory.instances.topological_space_unbundled.{v} X)) : Type (v+1)

This time Lean seems to have switched universes on! The two terms are equal except for universes.

Is this the sort of thing I just have to deal with in category theory? @Reid Barton ?

#### Kevin Buzzard (Apr 14 2019 at 18:21):

Oh *boggle* I just checked with a vanilla mathlib and `category_theory.instances.Top`

isn't there. That'll teach me to listen to Scott.

#### Kevin Buzzard (Apr 14 2019 at 18:26):

@Scott Morrison is this something to do with your modification `category_theory.instances.Top`

of `category_theory.instances.topological_spaces`

in your branch? I switched back to `topological_spaces`

and now I see ulifts and plifts when I try to define the functor.

#### Kevin Buzzard (Apr 14 2019 at 18:31):

This is all something to do with turning hom sets from Type v into Prop.

#### Kevin Buzzard (Apr 14 2019 at 18:34):

Sorry, this is an issue with some of Scott's work in progress; I'll take it to github. I can get this to with in regular mathlib.

#### Scott Morrison (Apr 14 2019 at 22:46):

Sorry! :-) There is a big queue of PRs in category theory at the moment, making things a bit confusing.

Last updated: Dec 20 2023 at 11:08 UTC