Morphism of field extensions

Let $𝐿 1 : 𝐾$ and $𝐿 2 : 𝐾$ be field extensions, with inclusions $𝜄 𝑖 : 𝐾 \to 𝐿 𝑖$ . A morphism $𝜑$ from $𝐿 1 : 𝐾$ to $𝐿 2 : 𝐾$ is a morphism $𝜑 : 𝐿 1 \to 𝐿 2$ which fixes (the image of) $𝐾$ pointwise, #m/def/field i.e.

𝜑 𝜄 1 = 𝜄 2

In this way one obtains the category $𝖥 𝗅 𝖽 𝐾$ .

#state/tidy | #lang/en | #SemBr