Formal definition of forgetful functor Given the definition of a category $\mathbb{C}$ (that I rewrite just to agree on the notation), that consists of


*

*a collection of objects $\mathsf{Obj} ( \mathbb{C} )$;

*a collection of $\mathsf{Arr} ( \mathbb{C} )$, with $f \in \mathsf{Arr} ( \mathbb{C} )$,


I have a problem with the formal definition of forgetful functor. What I mean is that I always find this concept only – so to speak – informally defined. This is a problem to me, because begin self-thaught, I prefer to have formal definitions, where my bad intuition can fail less frequently (...in principle!).  
Thus, here there is my definition.

A forgetful functor is a functor $U: \mathbb{X} \to \mathbb{Y}$ that assigns to each $A \in \mathbb{X}$ a corresponding $U(A) \in \mathsf{Obj}(\mathbb{Y})$, and assigns to each morphism $f : A \to A'$ in $\mathbb{X}$ the same function $f$, regarded as a function between elements of $\mathsf{Obj}(\mathbb{Y})$.

Is this definition correct?  
Thanks as always for your time.
Any feedback (or improvement, or comment on conceptual typos) is more than welcome.
PS: I am aware that this question could come as a duplicate (and see reference therein). However, I do think it is not the case. My question has not deep mathematical or conceptual implications: it is more a question in order to get some intuition behind this concept. In other words, I would find a reasonable answer, one where somebody writes "This is wrong, and you cannot do that, but in principle this is what roughly speaking we all have in mind (being aware it is not completely right!), when we find that expression".
 A: You should think of "forgetful functor" not as a class of functors that you can hope to isolate by some property but as a particularly common method of producing functors, which roughly goes like this: many categories are defined as having objects which are tuples of things $(a, b, c, ...)$ (e.g. the tuple $(M, e, m)$ consisting of a set $M$, an element $e \in M$, and a binary operation $m : M \times M \to M$) which satisfy some axioms (e.g. the identity axiom, associativity), and morphisms which are maps of tuples in some way. A forgetful functor is a functor you get by literally forgetting one or more of the things in the tuple (e.g. the identity $e$ and the multiplication $m$, which gets you the forgetful functor from monoids to sets). 
In particular, this notion of forgetful functor is not invariant under equivalence of categories: it depends on a choice of a presentation of a category in terms of objects made up of certain kinds of data, so that you can then forget some of the data. 
Even then, there are things that people call forgetful functors that aren't at least obviously described by this construction. For example, there is a functor from associative algebras to Lie algebras given by sending an algebra $A$ to the Lie algebra whose underlying vector space is $A$ and whose Lie bracket is the commutator bracket, and I often call this a forgetful functor even though I haven't, say, forgotten the entire multiplication on $A$. In order to describe this forgetful functor in terms of the above construction it's necessary to talk about every operation you get on algebras coming from composing scalar multiplication, addition, and multiplication (these form a Lawvere theory, or if you like an operad) and then forgetting some of them (the ones that you can get by composing scalar multiplication, addition, and the commutator bracket). 
Sometimes it's just not worth trying to come up with a general definition. An analogous term it's not worth (in my experience) coming up with a general definition for is "geometry." Any definition you come up with will probably either exclude some important example or be so general that you can't do anything useful with it.
A: There isn't a formal definition of forgetful functors. It is a general name for functors $\mathcal C \to \mathcal D$ that takes an object $c$ of $\mathcal C$ to its underlying objects in $\mathcal D$ and does nothing on morphisms. The words in italic are expected to have obvious definition in working examples. 
The only things that people tends to agree on is that a forgetful functor must be faithful (this is the best we can hope of do nothing in full generality). Beyond that, it is whatever you want it to be in the examples you are interesting it. For example, algebraists will probably require that the functor has also a left adjoint in order to have a free algebraic construction.
