Bundle section

Consider a fibre bundle.

𝐹 \to 𝐸 𝜋 ↠ 𝐵 .

A section of the bundle is simply a section of $𝜋$ in the sense of category theory, #m/def/top i.e. a morphism $𝜎 : 𝐵 ↪ 𝐸$ such that $𝜋 𝜎 = 1 𝐵$ .

This makes a section a special case of a bundle map if we consider $𝐵$ as a bundle over itself, so the set of all sections is given by

Γ (𝐵, 𝐸) = Γ 𝐸 : = 𝖡 𝗎 𝗇 𝖽 𝐵 (𝐸, 𝐵)

A section can be thought of as a dependently typed function, sending each $𝑝 \in 𝐵$ to a $𝜎 (𝑝)$ in the fibre $𝐸 𝑝$ .

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