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

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?

• On what page of the document did you see that? – md2perpe Sep 21 '18 at 18:51
• Does it possibly say $a \mapsto a : A \to B$ instead of $a \to a : A \to B$? – md2perpe Sep 21 '18 at 18:54
• The paper uses the notation $a\mapsto a$ not $a\to a$. This is commonly used for describing functions anonymously, i.e. its like saying you have an $i:\mathcal A\to\mathcal B$ where $i(a)=a$ without needing to name $i$. – Derek Elkins left SE Sep 21 '18 at 18:54
• @md2perpe page, 26 (Apologies forgot to say the page number!). – Pinocchio Sep 21 '18 at 22:11
• @md2perpe for your second comment, it looks like me like that you wrote the same thing twice. What is the difference between the first one and the second one? – Pinocchio Sep 21 '18 at 22:12

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.

• I think the arrow notation is clear to me now (thanks!). But what the question is actually saying confuses me. If we have an identity mapping then $A = B$ otherwise it wouldn't be an identity map. What the notes are trying to say still makes little sense to me. – Pinocchio Sep 23 '18 at 2:03
• @Pinocchio. An identity map has domain and codomain equal, but here we have an inclusion map which maps an element in a subset to itself in the superset. Example: $\iota : \mathbb{N} \to \mathbb{R}, \ \iota(x) = x.$ – md2perpe Sep 23 '18 at 7:08

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.

• When you mean i should verify it myself I am having trouble understanding what I am suppose to check. Am I suppose to check in subsets are a relation? They are under the power set poset $(P(A),\leq)$ where $\leq := \subseteq$. I know I'm missing something really silly, I know its just a parsing/language thing but I can't quite catch what it is. – Pinocchio Sep 21 '18 at 22:31
• is $x \mapsto \log(x) : \mathbb{R^{>0}} \to \mathbb{R}$ what that notation means? i.e. we have the anonymous function on the LEFT and the sets it maps to are on the RIGHT? I choose that specific example to hopefully make it clear since the log function maps positive things to the whole real line. Nearly like specifying the "types of objects" the anonymous functions maps between. – Pinocchio Sep 21 '18 at 22:32
• also I'm not sure what $\mathcal A \subseteq \mathcal B$ means since they aren't sets, they are L-structures. Only does $A \subseteq B$ make sense to me since those are the underlying sets (note the disappearance of the calligraphic notation). – Pinocchio Sep 21 '18 at 22:34