Uncountably long paths through a quiver

Stream: maths

[Robert Maxton]

I've been trying to implement http://www.tac.mta.ca/tac/volumes/1999/n11/n11.pdf in order to implement (strict) colimits in Cat, an effort I am increasingly considering may be better directed towards putting enough 2-limit structure into Mathlib to do weak colimits instead. I have just encountered an obstacle that seems mathematically nontrivial (rather than 'mathematically obvious but unclear how to implement in Lean'), so I'm turning to the Zulip for advice.

BBP claim that

Let $F : A → B$ be a functor.
Usually, the images of objects and morphisms of $A$ in $B$ via $F$ , denoted $F(A)$, do not
form a subcategory of $B$, cf. example 3.8. There is always, however, the least subcategory
of $B$ which contains $F(A)$. This subcategory, denoted $\operatorname{Im} F$ , is called the image of $A$ in $B$
via $F$. Clearly, $\operatorname{Ob} \operatorname{Im} F = F (\operatorname{Ob} A)$ while $\operatorname{Mor}\operatorname{Im} F$ consists of all compositions of morphisms
from $F (\operatorname{Mor}A)$ possible in $B$. A functor satisfying $F (A) = B$ is called surjection.

Fair enough. But in that case, when referring to a functor that is indeed surjective, s.t. $\operatorname{Im} F = B$, the "preimage" of an arbitrary morphism in $B$ may in fact only be a path in $A$ -- potentially an infinite path, and if there's any constraint on the length I don't see it.

[Robert Maxton]

I suppose this does ultimately turn into "how do I work with this in Lean". Quiver.Path is an inductive datatype, thus necessarily finite; maybe I can take some limiting object to work with a countably long path, but it can't possibly represent an uncountable one, AIUI.

[Robert Maxton]

I'm currently staring at docs#CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape, to see if it will provide the handle I need, but it's not clear that it will. What I fundamentally need is a large eliminator, some way to not just prove things but generate data on all paths of arbitrary length in this category... This is probably going to end up with me resorting to Zorn's lemma, isn't it?

[Aaron Liu]

Robert Maxton said:

I suppose this does ultimately turn into "how do I work with this in Lean". Quiver.Path is an inductive datatype, thus necessarily finite; maybe I can take some limiting object to work with a countably long path, but it can't possibly represent an uncountable one, AIUI.

I don't see how you would reasonably implement the source and target of an infinite path, can you explain why you think finite paths are not enough? Finite paths are closed under composition, so I would think they form a category.

[Robert Maxton]

They form a category. They don't form the specific arbitrary category in some Type u with Type v-indexed paths I'm trying to prove things about.

[Robert Maxton]

And actually the source and target's the easiest part, you can pin that down as part of the type signature. Or, you can fix the source and then have the target as the colimit of the indexing functor, which is the strategy TransfiniteCompositionOfShape uses.

[Aaron Liu]

What is the specific arbitrary category you are trying to prove things about? I got the impression that it was $\text{Im} F$.

[Robert Maxton]

Yes, but $F$ is an arbitrary functor.

... ah.

Right. The least subcategory of $B$ that contains $F(A)$ would be the one with finitely long paths at most, wouldn't it.

[Robert Maxton]

Okay, that might have saved me a lot of rewriting. Thanks!