accidentally-corrected namespace?

Stream: general

[Kevin Buzzard]

I might be about to make a fool of myself, but I discovered by accident that we seem to have a namespace called Module.category_theory in mathlib3:

import algebra.category.Module.basic

#check category_theory.forget -- it exists

namespace Module

-- doing stuff with modules and now I need category_theory.forget

open category_theory

#check forget -- fails!!

open _root_.category_theory

#check forget -- works

end Module

open Module.category_theory -- works!!

I don't think we have anything like CommRing.category_theory or anything like that, and I'm wondering if Module.category_theory was created by accident. I think it's in algebra.category.Module.basic, because if I replace that import with the files which it imports instead then the error goes away. Or are we supposed to have a namespace Module.category_theory?

[Adam Topaz]

It's probably caused by an automatically generated name from a category (or something else from the CT library) instance

[Kevin Buzzard]

It's

instance : has_zero_object (Module.{v} R) :=
⟨⟨of R punit, is_zero_of_subsingleton _⟩⟩

in the Module namespace, which creates a term named Module.category_theory.limits.has_zero_object. Is this anything worth worrying about?

[Kevin Buzzard]

This tripped me up when teaching just now, because I opened category_theory in the Module namespace and it didn't open, causing me a few minutes of confusion :-)

[Adam Topaz]

I don't think it's necessarily anything to worry about, but it should be very easy to just add a name for that instance.