Category of field extensions

The category of extensions of $𝐾$ $𝖥 𝗅 𝖽 𝐾 : = 𝐾 ↓ 𝖥 𝗅 𝖽$ is a category where an object is a extension field of $𝐾$ and a morphism is a morphism of field extensions. #m/def/field

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