Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
As far as I can tell, the difference between a monadic functor and a strictly monadic functor boils down to this: a strictly monadic functor $U : \mathcal{D} \to \mathcal{C}$ has the property that, for any object $D$ in $\mathcal{D}$ and any isomorphism $f : C \to U D$ in $\mathcal{C}$, there is a unique object $\tilde{C}$ and an (automatically unique) isomorphism $\tilde{f} : \tilde{C} \to D$ such that $U \tilde{f} = f$. Conversely, any monadic functor with this property is strictly monadic. This is very reminiscent of the definition of isofibration, but a monadic isofibration need not be strictly monadic. What’s a good phrase to describe functors like these for which isomorphisms lift uniquely?
Your second bullet point confuses me. Are you looking for a name for a functor such that for any isomorphism $f:C\to U D$ there exists a unique $\tilde{C}$ such that there exists some (not necessarily unique) isomorphism $\tilde{f}:\tilde{C}\to D$ with $U\tilde{f} = f$? If so, why? As you mentioned, in your motivating example of a strictly monadic functor, also $\tilde{f}$ is unique.
Well, it seems to be the smallest modification to the definition of isofibration needed to make things work. A monadic functor is automatically faithful (can we prove this directly from the assumptions of the monadicity theorem?) so the isomorphism, once it exists, is unique up to the choice of endpoints – so we only need to add a uniqueness hypothesis on the object part of the lifting problem. But I’m also happy to consider names for functors where isomorphisms lift uniquely in the stronger sense.
Well, asking for the domain of a morphism to be unique but not the morphism itself is pretty bizarre, categorically speaking. I think “strict isofibration” would naturally mean the stronger sense. Also there is the notion of an “amnestic functor”, which reflects the property of an isomorphism being an identity; I think that isofibration + amnestic should be equivalent to what you want.
Ah, amnestic functors! How ironic that I forgot about them. Yes, exactly – an amnestic monadic isofibration is strictly monadic and vice versa. It corresponds nicely to the two parts of the proof too – a monadic isofibration is one where the comparison functor is strictly surjective on objects, and an amnestic monadic functor is one where the comparison functor is injective on objects. Put the two together and we get a strictly monadic functor. Thanks!
If you feel like doing the world a service, you could create amnestic functor and add a section about strict monadicity to monadic functor, with references to amnestic functor and isofibration. (-:
Done!
Nice, thanks!
1 to 8 of 8