섹션의 의미에 관한 노트

유형론에서 섹션_section이라는 용어는 두 가지 의미로 등장한다.

정의. 사상 $r: B \to A$과 $s: A \to B$가 $rs \sim \mathrm{id}_A$를 만족한다면 $s$를 $r$의 섹션이라고 하고, $r$을 $s$의 리트랙트라고 한다. 즉, 다음과 같이 정의한다.

\[\begin{gather} \mathrm{sec}(r) := \sum_{s': A \to B} rs' \sim \mathrm{id}_A\\ \mathrm{ret}(s) := \sum_{r': A \to B} r's \sim \mathrm{id}_B \end{gather}\]

정의. $B$가 $A$에 대한 유형족_{type family}이라고 하자. $x: A$가 주어졌을 때 $b(x): B(x)$라면, $b$를 $B$의 섹션이라고 부른다.

두 가지 의미의 섹션은 연관돼 있다. 첫 번째 정의를 기하학적으로 해석하면, 섹션 $s: A \to B$는 공간 $A$를 공간 $B$에 한 단면으로서 포함시키는 사상이며, 그에 대응되는 리트랙트 $r: B \to A$는 공간 $B$를 공간 $A$로 투영하는 사상이다. 이로부터 몇 가지 사실을 고찰할 수 있다.

• 일반적으로, “확대 후 축소”는 원 공간의 관계를 보존하지만 “축소 후 확대”는 보존하지 않는다. 이는 $r, s$가 리트랙트-섹션 관계일 때, $rs \sim \mathrm{id}_A$이지만 일반적으로 $sr \sim \mathrm{id}_B$이지는 않음을 시사한다.

• 섹션은 각 $a: A$에 대해 $r$의 $a$-섬유_fiber에서 한 점을 선택한다. 이는 도형의 $z$-등고면은 각각 특정한 $z$-좌푯값의 선택과 같은 것으로 이해할 수 있다.

• 그림에서 섬유는 한 가닥의 실처럼 보이며, 이것은 “섬유”라는 이름의 유래이다.

한편 $b$가 $A$에 대한 유형족 $B$의 섹션일 때, $b$는 각 $a: A$에 대해 $b(a): B(a)$를 선택한다. 여기서 $B(a)$는 $\mathrm{pr}_1: \sum_{x: A}B(x) \to A$의 $a$-섬유와 자연스럽게 동치이다. 따라서 $b$가 $B$의 (두 번째 의미에서의) 섹션일 때, $\lambda x. b(x)$는 $\mathrm{pr}_1$의 (첫 번째 의미에서의) 섹션이다.

물론, $\lambda x . b(x)$는 $b$와 판단적으로 같다. 따라서 섹션의 두 번째 의미는 첫 번째 의미의 특수한 사례이다.