Nothing uses directed_system.map_self

Stream: maths

[Eric Wieser]

While doing some unrelated cleanup, I noticed that nothing seems to use docs#directed_system.map_self. Is this "axiom" justified in being there anyway?

[David Wärn]

Interesting find. I think it's still the 'correct' definition even if nothing currently uses it. The description of a directed system as a functor would be inaccurate without this condition. And you wouldn't be able to show that if ι has a greatest element then the direct limit is the corresponding 'last' object. (Effectively, if you remove the map_self condition, then each object comes equipped with an idempotent endomorphism, and the limit will quotient each object by the kernel of this endomorphism)

[Eric Wieser]

Actually I was wrong, it's used in docs#Module.direct_limit_diagram