A formal definition of forgetful functor

Question

I have read in many category theory textbooks the term "forgetful functor". But no has ever given me a precise definition of this term. I want a rigorous definition, not merely an answer that basically says, "I know it when I see it.". Has someone developed a perfectly rigorous definition of forgetful functors? This question is different from the duplicate because even there the answer was basically, "I know it when I see it".

Answer 1

Forgetful functors are not a class of functors. No, really! They are a particular style of defining functors, given by "forgetting" something.

You might, as Max says in the comments, want to define forgetful functors as simply being the faithful functors. But I would argue that this definition is both too broad and too narrow.

Too narrow: Consider, for example, the functor $\text{Set} \times \text{Set} \to \text{Set}$ given by the projection to the first coordinate. I would argue that this functor deserves to be called "forgetful," since what you are forgetting is the second set (in the nLab's terminology, this functor "forgets stuff"). But it clearly isn't faithful!

Too broad: Probably a simpler example is possible, but consider the following. There is a functor $L \mapsto U(L)$ from Lie algebras to Hopf algebras given by taking the universal enveloping algebra. At least over a field of characteristic $0$, this functor is not only faithful, it is fully faithful. But I would argue that it does not deserve to be called a forgetful functor, because it was not defined by "forgetting" anything about Lie algebras. If you ever write somewhere the phrase "the forgetful functor from Lie algebras to Hopf algebras," you'll confuse people.

(There is an equivalent functor which maybe does deserve to be called forgetful, given by replacing the category of Lie algebras with the equivalent category of Hopf algebras generated by their primitive elements, and then forgetting this last condition. But actually every functor is equivalent to a functor which is "forgetful" in the broad sense I'm describing, or rather which can be "defined forgetfully.")