Type class inference and category theory

Stream: new members

[Nicolò Cavalleri]

I just began looking at the category theory part of the library and I do not understand how type class inference works:

import category_theory.single_obj
import topology.sheaves.local_predicate

universe u

open Top category_theory

section

variables (X : Top.{u}) (s t : set X) (T : Type u)

#check sheaf_to_Type X T

example (hs : is_open s) (ht : is_open t) : is_open (s ∩ t) := hs.inter ht

end

section

variables (T : Type u) (X : Type u) [topological_space X]

#check sheaf_to_Type X T -- this does not typecheck

end

magically (I don't know how this is possible but it is super cool) X : Top.{u} gets recognized by type class inference as a topological space. But how do I go the other way around and get a standard topological space get recognized as an object in its category?

[Adam Topaz]

docs#Top.of

[Nicolò Cavalleri]

Ok thank you!

[Nicolò Cavalleri]

Why does sheaf_to_top only require one argument? I would guess that it should behave as presheaf_to_top:

variables (Y : Type u) [topological_space Y] (X : Type u) [topological_space X] (s t : set X)
  (hs : is_open s)


#check presheaf_to_Top (Top.of X) (Top.of Y)
#check sheaf_to_Top (Top.of X) (Top.of Y)

[Adam Topaz]

I think the idea is for you to write sheaf_to_Top T : sheaf _ X if you want to specify the X as well.

[Nicolò Cavalleri]

Adam Topaz said:

I think the idea is for you to write sheaf_to_Top T : sheaf _ X if you want to specify the X as well.

Why is that convenient? I mean why can X usually be inferred for sheaves?

[Adam Topaz]

I think the idea is that this definition is used primarily in the context where you have other objects of the category sheaf (Type*) X. For example, if Y : sheaf (Type*) X, then you would be able to write sheaf_to_Top T \hom Y to obtain the type of morphisms of sheaves from this thing to the given sheaf Y.

[Nicolò Cavalleri]

Ok thanks a lot! One more question:

variables (Y : Type u) [topological_space Y] (X : Type u) [topological_space X] (s t : set X)
  (hs : is_open s) (x : s)
  (f : (sheaf_to_Top (Top.of Y) : sheaf _ (Top.of X)).val.obj (op ⟨s, hs⟩))
  (g : (sheaf_to_Type (Top.of X) (Top.of Y)).val.obj (op ⟨s, hs⟩))

#check g x --typechecks
#check f x --does not

I understand that this does not work because despite f is really a continuous_map s Y, lean sees it as a (of Y).sheaf_to_Top.val.obj (op ⟨s, hs⟩) which is basically a type synonym for continuous_map s Y. Is there some trick to get lean recognize f as a continuous_map so that the above notation works?

[Yaël Dillies]

Use a type-ascription is the solution I suspect.

[Yaël Dillies]

@Anne Baanen, I hit the exact same thing in #11968. I assume there's no real solution here because Lean has too much to unfold?

[Adam Topaz]

You could also add the appropriate has_coe_to_fun instance to help lean along...

[Anne Baanen]

I suspect you could also get it to work by making certain definitions reducible, but I'd have to see the output of set_option trace.class_instances true to be sure. For now my advice is to either add new has_coe_to_fun instances or use type ascriptions.

[Nicolò Cavalleri]

Adam Topaz said:

You could also add the appropriate has_coe_to_fun instance to help lean along...

Yes I mean I though about that too but my above question was wrong sorry, I do not only want to use the notation, I also want to use the whole API for continuous_map

[Nicolò Cavalleri]

Yaël Dillies said:

Use a type-ascription is the solution I suspect.

What is type-ascription? haha

[Adam Topaz]

You can write (f : continuous_map _ _) x

[Adam Topaz]

You should still be able to use the continuous_map api just fine since f is indeed a continuous_map.

[Nicolò Cavalleri]

Oh I see thanks haha I did not think about that

[Nicolò Cavalleri]

Well it is not working for me

[Nicolò Cavalleri]

import category_theory.single_obj
import topology.sheaves.local_predicate

universe u

open Top category_theory topological_space opposite
variables (Y : Type u) [topological_space Y] (X : Type u) [topological_space X] (s t : set X)
  (hs : is_open s) (x : s)
  (f : (sheaf_to_Top (Top.of Y) : sheaf _ (Top.of X)).val.obj (op ⟨s, hs⟩))
  (g : (sheaf_to_Type (Top.of X) (Top.of Y)).val.obj (op ⟨s, hs⟩))

#check g x --typechecks
#check (f : continuous_map _ _) x --does not

[Nicolò Cavalleri]

This does should be a mwe

[Adam Topaz]

This looks like it's an issue with the type of x as opposed to f.

[Adam Topaz]

Hmmm... maybe not.

[Yaël Dillies]

You have to fill in those underscores for it to work, else Lean is not unfolding them enough :sad:

[Adam Topaz]

:expressionless:

import category_theory.single_obj
import topology.sheaves.local_predicate

universe u

open Top category_theory topological_space opposite
variables (Y : Type u) [topological_space Y] (X : Type u) [topological_space X] (s t : set X)
  (hs : is_open s) (x : s)
  (f : (sheaf_to_Top (Top.of Y) : sheaf _ (Top.of X)).val.obj (op ⟨s, hs⟩))
  (g : (sheaf_to_Type (Top.of X) (Top.of Y)).val.obj (op ⟨s, hs⟩))

#check let e : C(s,Y):= f in e x

[Adam Topaz]

I can't get it to work with type ascriptions.