What does the notation $ a \to a : A \to B$ means in the context of the word "inclusion"?

Question

I read the following sentence (from these notes on logic):

If $\mathcal A \subseteq \mathcal B$, then the inclusion $ a \to a : A \to B$ is an embedding $\mathcal A \to \mathcal B$

where $\mathcal{A} = (A, (R^{\mathcal A})_{R \in L^r}, (F^{\mathcal A})_{F \in L^f} )$, $\mathcal{B} = (B, (R^{\mathcal B})_{R \in L^r}, (F^{\mathcal B})_{F \in L^f} )$ are different L-structures.

I was trying to understand what that specific sentence meant. The things that confuse me the most are:

1. what inclusion means in this context.
2. what the notation $ a \to a : A \to B$ means.

usually $ x \to f(x) $ means x is mapped to f(x) e.g. $x \to e^x$. Then word inclusion from googling seems to just mean subset. Thus I'm confused, is what we are considering mapping the whole set A to B or elements from A to elements of B? What is an embedding in this context? I know embeddings in general are injective strong homomorphisms, but right now its unclear what the homomorphism we are talking about and what sets we are talking about and what relations/functions we are talking about. What are we mapping from what to what and where does this fit with the given sentence?

Answer 1

This is actually very trivial. Here 'inclusion' does indeed mean subset: The containment $\mathcal A \subseteq \mathcal B$ induces a subset relationship $A \subseteq B$ (you should verify this yourself). We are taking that subset relationship and reinterpreting it as the identity mapping from $A$ to $B$. The expression $a \to a : A \to B$ means we are expressing the definition of this identity mapping, by saying that we are mapping each object $a$ [left-side], viewed as an element of $A$, onto the self-same object $a$[right-side], viewed as an element of $B$. The opening sentence is then saying that this set-to-set mapping induces a corresponding structure-to-structure embedding.

Answer 2

A formula of the form $x \mapsto u(x) : X \to Y,$ where $u(x)$ is an expression, denotes a function that for a given value $x \in X$ returns the value $u(x) \in Y$. Note the difference between the two types of arrows. This notation is equivalent to writing $f:X \to Y,\ f(x)=u(x),$ but doesn't give a name to the function.

An example: $x \mapsto x^2 : \mathbb{R} \to \mathbb{R}$ denotes the same function as $f : \mathbb{R} \to \mathbb{R},\ f(x) = x^2$.

Modern programming languages have adopted this notion of anonymous functions with notations like (x) => x*x.