| [[범주론|'''범주론 {{{#!wiki style="font-family: Times New Roman, serif; display: inline"]] | ||
| {{{#!wiki style="min-height: calc(1.5em + 5px); margin: 0 -10px -5px" {{{#!folding [ 펼치기 · 접기 ] {{{#!wiki style="margin: -5px -1px -11px" | <colbgcolor=#2f4c52,#2f4c52><colcolor=#fff,#fff> 개념 | 범주(종류 · 여러 가지 범주) · 대상(부분 대상) · 사상(정의역과 공역 · Hom · 항등 사상 · 동형 사상) · 함자(항등 함자 · Hom-함자 · 범주의 동치) · 자연 변환(자연 동형) · 수반쌍 · 보편 성질 · 퀴버(quiver) · 자기 동형 사상군 |
| 범주의 종류 및 구성 | 곱범주 · 콤마 범주(조각 범주) · 자유 범주 · 준군(groupoid)(기본준군) · 반대 범주 · 함자 범주(화살 범주) | |
| 극한 | 다이어그램(가환 다이어그램) · 극한↔쌍대극한op · 끝↔시작op(영대상 · 영사상) · 곱↔쌍대곱op · 이퀄라이저(핵)↔코이퀄라이저op(공핵) · 당김↔밂op · 완비 범주 | |
| 하위 분야 | 범주론적 대수학 · 고차 범주론 · 풍성 범주론(enriched category theory) · 토포스 이론 · 대수적 집합론 | |
| 기타 | 교재(Categories for the Working Mathematician) · abstract nonsense · 쌍대성 | |
| 틀:수학기초론 · 틀:대수학 · 수학 관련 정보 | }}}}}}}}} | |
| '''[[집합론|집합론 {{{#!wiki style="font-family: Times New Roman, serif; display: inline;"]]''' | ||
| {{{#!wiki style="margin: 0 -10px -5px; min-height: calc(1.5em + 5px)" {{{#!folding [ 펼치기 · 접기 ] {{{#!wiki style="margin: -5px -1px -11px" | <bgcolor=#6600ff,#6600ff> ▲ 수학기초론 | |
| <colbgcolor=#6c6c2e,#5e5e28><colcolor=#fff,#fff> 기본 대상 | 집합(표기 · ∈) · 공집합 · 부분집합 · 모임(수학) · 공리 · 순서쌍 · 첨수 집합족 | |
| 공리계 | ZFC 공리계 · NBG 공리계 | |
| 연산 | 멱집합 · 곱집합 · 드모르간 법칙 · 분리 합집합 | |
| 관계 | 이항 관계 · 반사성 · 대칭성 · 추이성 · 동치관계 · 부분함수 · 함수(정의역과 공역 · 단사와 전사 · 합성함수 · 역함수 · 항등함수 · 공함수) · 순서 관계(부분 순서 · 하세 다이어그램) | |
| 자연수 | 페아노 공리계 · 재귀 정리 · 정렬 원리 · 수학적 귀납법 | |
| 기수 · 서수 | 선택공리(초른의 보조정리 · 하우스도르프 극대 원리) · 초한기수(힐베르트의 호텔) · 슈뢰더-베른슈타인 정리 · 대각선 논법 · 연속체 가설 · 추이적 집합 · 큰 가산서수 · 우주(집합론) | |
| 기타 | 러셀의 역설 · 집합론 교재 | }}}}}}}}} |
1. 개요
Thus we seem to have partially demonstrated that even in foundations, not Substance but invariant Form is the carrier of the relevant mathematical information.
윌리엄 로비어(William Lawvere), An elementary theory of the category of sets, 1964.[Lawvere1964]
윌리엄 로비어(William Lawvere), An elementary theory of the category of sets, 1964.[Lawvere1964]
모든 집합과 함수들의 범주 Set을 공리화한 일차 이론(first order theory).
토포스 이론 등으로 유명한 윌리엄 로비어(William Lawvere)가 리드 칼리지에서 해석학을 가르치면서 ZFC 공리계을 대체할 더 직관적인 집합론의 기초(foundation)를 고민한 것에서 출발했다.[2]
이후 1964년 손더스 맥레인의 도움을 받아(communicated) 미국국립과학원회보(PNAS)에 An elementary theory of the category of sets[Lawvere1964]라는 이름으로 발표했다. 덕분에 해당 paper 제목에서 따와 흔히 ETCS라고 불린다.
2. 정의
좀더 흔히 아는 범주스러운 직관을 위해선 MSL을 써도 되고 실제로 Sets for mathematics[Lawvere.Rosebrugh2003]에서 로비어 본인이나 Leinster[Leinster2014] 등도 two sorted로 설명하긴 하나, 로비어가 처음 쓴 내용은 singled sorted이고 아무래도 untyped predicate가 공리 나열할때만큼은 좀더 다루기 편하니 본 문서는 이를 기준으로 서술한다. 참고로 object를 identity morphism으로 보는 발상은 범주 문서의 일차 이론으로 정의 문단이나 사상만을 사용하는 정의 문단이랑 비슷하다.2.1. 이론
해당 이론(theory)의 (유일한) object of discourse를 morphism이라 부르고, 아래와 같은 signature [math(\Sigma)]로부터 생성되는 first order language를 생각하자.- 두 function symbols: [math(\mathrm{dom})] (rank 1), [math(\mathrm{cod})] (rank 1)
- relation symbol 하나: [math(\theta)] (rank 3)
즉, [math(\mathrm{dom})]과 [math(\mathrm{cod})]는 각 morphism마다 정의역과 공역을 할당하는 unary function symbol, [math(\theta)]는 사상의 합성을 표현하는 ternary predicate symbol이다.
여기에 정의역과 공역이 identity라는 내용과 사상의 합성의 존재성과 정의역/공역 상속 및 결합성 등 기본적인 범주가 가지는 공리를 나열하자.
- CT1: [math(\forall x_1 ( \mathrm{cod} ( \mathrm{dom} (x_1) ) = \mathrm{dom} (x_1) \land \mathrm{dom} ( \mathrm{cod} (x_1) ) = \mathrm{cod} (x_1) ))]
- CT2: [math(\forall x_1 \forall x_2 \forall x_3 \forall x_4 ( \theta ( x_1, x_2, x_3 ) \land \theta ( x_1, x_2, x_4 ) \to x_3 = x_4 ))]
- CT3: [math(\forall x_1 \forall x_2 ( \mathrm{dom} (x_2) = \mathrm{cod} (x_1) \leftrightarrow \exists x_3 ( \theta ( x_1, x_2, x_3 ) ) ))]
- CT4: [math(\forall x_1 \forall x_2 \forall x_3 ( \theta ( x_1, x_2, x_3 ) \to \mathrm{dom} (x_3) = \mathrm{dom} (x_1) \land \mathrm{cod} (x_3) = \mathrm{cod} (x_2) ) )]
- CT5: [math(\forall x_1 ( \theta ( \mathrm{dom} (x_1), x_1, x_1 ) \land \theta ( x_1, \mathrm{cod} (x_1), x_1 ) ))]
- CT6: [math(\forall x_1 \forall x_2 \forall x_3 \forall x_4 \forall x_5 \forall x_6 \forall x_7 ( \theta ( x_1, x_2, x_4 ) \land \theta ( x_2, x_3, x_5 ) \land \theta ( x_4, x_3, x_6 ) \land \theta ( x_1, x_5, x_7 ) \to x_6 = x_7 ))]
2.2. 공리
ZFC 공리계 등 문서와의 통일을 위해2.2.1. Axiom 1
유한 극한 및 쌍대극한의 존재성을 보장하는 공리인데, 원 논문에서는 당시 로비어가 쓰던 용어대로 finite roots/coroots로 쓰였다. 구체적으로 다음 여섯 가지로 나눌 수 있다.- ETCS1A: 끝(terminal)이 존재한다.
[math(\exists x_1 \forall x_2 ( \mathrm{dom} (x_2) = x_2 \to \exists x_3 ( \mathrm{dom} (x_3) = x_2 \land \mathrm{cod} (x_3) = x_1 \land \forall x_4 ( \mathrm{dom} (x_4) = x_2 \land \mathrm{cod} (x_4) = x_1 \to x_3 = x_4 ) ) ) )] - ETCS1B: 시작(initial)이 존재한다.
[math(\exists x_1 \forall x_2 ( \mathrm{dom} (x_2) = x_2 \to \exists x_3 ( \mathrm{dom} (x_3) = x_1 \land \mathrm{cod} (x_3) = x_2 \land \forall x_4 ( \mathrm{dom} (x_4) = x_1 \land \mathrm{cod} (x_4) = x_2 \to x_3 = x_4 ) ) ) )] - ETCS1C: 이항 곱(binary product)이 존재한다.
[math(\forall x_1 \forall x_2 ( \mathrm{dom} (x_1) = x_1 \land \mathrm{dom} (x_2) = x_2 \to \exists x_3 \exists x_4 ( \mathrm{cod} (x_3) = x_1 \land \mathrm{cod} (x_4) = x_2 \land \mathrm{dom} (x_3) = \mathrm{dom} (x_4) \land \forall x_5 \forall x_6 ( \mathrm{cod} (x_5) = x_1 \land \mathrm{cod} (x_6) = x_2 \land \mathrm{dom} (x_5) = \mathrm{dom} (x_6) \to \exists x_7 ( \mathrm{dom} (x_7) = \mathrm{dom} (x_5) \land \mathrm{cod} (x_7) = \mathrm{dom} (x_3) \land \theta ( x_7, x_3, x_5 ) \land \theta ( x_7, x_4, x_6 ) \land \forall x_8 ( \mathrm{dom} (x_8) = \mathrm{dom} (x_7) \land \mathrm{cod} (x_8) = \mathrm{cod} (x_7) \land \theta ( x_8, x_3, x_5 ) \land \theta ( x_8, x_4, x_6 ) \to x_7 = x_8 ) ) ) ) ))] - ETCS1D: 이항 쌍대곱(binary coproduct)이 존재한다.
[math(\forall x_1 \forall x_2 ( \mathrm{dom} (x_1) = x_1 \land \mathrm{dom} (x_2) = x_2 \to \exists x_3 \exists x_4 ( \mathrm{dom} (x_3) = x_1 \land \mathrm{dom} (x_4) = x_2 \land \mathrm{cod} (x_3) = \mathrm{cod} (x_4) \land \forall x_5 \forall x_6 ( \mathrm{dom} (x_5) = x_1 \land \mathrm{dom} (x_6) = x_2 \land \mathrm{cod} (x_5) = \mathrm{cod} (x_6) \to \exists x_7 ( \mathrm{cod} (x_7) = \mathrm{cod} (x_5) \land \mathrm{dom} (x_7) = \mathrm{cod} (x_3) \land \theta ( x_3, x_7, x_5 ) \land \theta ( x_4, x_7, x_6 ) \land \forall x_8 ( \mathrm{dom} (x_8) = \mathrm{dom} (x_7) \land \mathrm{cod} (x_8) = \mathrm{cod} (x_7) \land \theta ( x_3, x_8, x_5 ) \land \theta ( x_4, x_8, x_6 ) \to x_7 = x_8 ) ) ) ) ))] - ETCS1E: 이퀄라이저(equalizer)가 존재한다.
[math(\forall x_1 \forall x_2 ( \mathrm{dom} (x_1) = \mathrm{dom} (x_2) \land \mathrm{cod} (x_1) = \mathrm{cod} (x_2) \to \exists x_3 ( \mathrm{cod} (x_3) = \mathrm{dom} (x_1) \land \exists x_4 ( \theta ( x_3, x_1, x_4 ) \land \theta ( x_3, x_2, x_4 ) ) \land \forall x_4 ( \mathrm{cod} (x_4) = \mathrm{cod} (x_3) \land \exists x_5 ( \theta ( x_4, x_1, x_5 ) \land \theta ( x_4, x_2, x_5 ) ) \to \exists x_5 ( \mathrm{dom} (x_5) = \mathrm{dom} (x_4) \land \mathrm{cod} (x_5) = \mathrm{dom} (x_3) \land \theta ( x_5, x_3, x_4 ) \land \forall x_6 ( \mathrm{dom} (x_6) = \mathrm{dom} (x_5) \land \mathrm{cod} (x_6) = \mathrm{cod} (x_5) \land \theta ( x_6, x_3, x_4 ) \to x_5 = x_6 ) ) ) ) ))] - ETCS1F: 코이퀄라이저(coequalizer)가 존재한다.
[math(\forall x_1 \forall x_2 ( \mathrm{dom} (x_1) = \mathrm{dom} (x_2) \land \mathrm{cod} (x_1) = \mathrm{cod} (x_2) \to \exists x_3 ( \mathrm{dom} (x_3) = \mathrm{cod} (x_1) \land \exists x_4 ( \theta ( x_1, x_3, x_4 ) \land \theta ( x_2, x_3, x_4 ) ) \land \forall x_4 ( \mathrm{dom} (x_4) = \mathrm{dom} (x_3) \land \exists x_5 ( \theta ( x_1, x_4, x_5 ) \land \theta ( x_2, x_4, x_5 ) ) \to \exists x_5 ( \mathrm{cod} (x_5) = \mathrm{cod} (x_4) \land \mathrm{dom} (x_5) = \mathrm{cod} (x_3) \land \theta ( x_3, x_5, x_4 ) \land \forall x_6 ( \mathrm{dom} (x_6) = \mathrm{dom} (x_5) \land \mathrm{cod} (x_6) = \mathrm{cod} (x_5) \land \theta ( x_3, x_6, x_4 ) \to x_5 = x_6 ) ) ) ) ))]
범주론적 직관(?)을 생각하면 terminal(중 하나)을 [math(\mathbf 1)]이라 했을 때 흔히 생각하는 각 집합 [math(S)]의 원소(element) [math(x)]는 [math(x : \mathbf 1 \to S)] 꼴의 morphism으로 볼 수 있다. 즉, ETCS에서 ∈는 더 이상 primitive predicate가 아니고, [math(\in ( x_1, x_2 ) : \mathrm{IsTerminal} ( \mathrm{dom} (x_1) ) \land \mathrm{cod} (x_1) = x_2)] 등으로 ETCS 내에서 정의할 수 있다. 순수 편의상 앞으로는 terminal이 유일하다 가정하고 [math(\mathbf 1)]로 표기하자.
위와 같은 정의를 생각했을 때 ETCS의 morphism이 사실상 함수의 성질을 가짐을 보일 수 있는데, morphism [math(f)]에 대해 다음이 성립한다.
| [math(x)]가 [math(\mathrm{dom} (f))]의 원소라면, [math(f \circ x)]와 같은 [math(\mathrm{cod} (f))]의 원소 [math(y)]가 유일하게 존재한다. [math(\forall f \forall x ( \mathrm{dom} (x) = \mathbf 1 \land \mathrm{cod} (x) = \mathrm{dom} (f) \to \exists y ( \mathrm{dom} (y) = \mathbf 1 \land \mathrm{cod} (y) = \mathrm{cod} (f) \land \theta ( x, f, y ) ) ))] |
가정에 의하면 [math(x : \mathbf 1 \to \mathrm{dom} (f))]이니 [math(f)]를 apply해도 [math(f \circ x : \mathbf 1 \to \mathrm{cod} (f))] 꼴이니 [math(\mathrm{cod} (f))]의 원소가 되고, 존재성과 유일성은 합성의 존재성과 유일성(CT3, CT2)에 의해서 유도된다. 즉, 직관적으로 정의역 원소 [math(x \in \mathrm{dom} (f))]의 image [math(f (x))]는 [math(f \circ x)]처럼 표현하면 된다.
물론 집합과 원소의 구분이 사실상 없고, 모든 집합이 어떤 집합의 원소가 될 수 있는 ZFC 공리계와는 달리 어떤 morphism은 아예 원소가 될 수 없다. 가령 [math(y \neq \mathbf 1)]라면 [math(x \in y \in z)] 같은 식조차 성립하지 않는다.
또한 흔히 아는 Set을 생각하면 initial [math(\mathbf 0)]의 존재성 공리 ETCS1B는 ZFC 등의 공집합의 존재성 공리와 비슷하다.
3. 참고 문헌
- Lawvere, F. W., & McLarty, C. (2005). An elementary theory of the category of sets (long version) with commentary. Reprints in Theory and Applications of Categories, 11, 1-35.
4. 관련 문서
[Lawvere1964] Lawvere, F. W. (1964). An elementary theory of the category of sets. Proceedings of the national academy of sciences, 52(6), 1506-1511.[2] Clementino, M. M., & Picado, A. (2007). An interview with F. William Lawvere. University of Coimbra.[Lawvere1964] [Lawvere.Rosebrugh2003] Lawvere, F. W., & Rosebrugh, R. (2003). Sets for mathematics. Cambridge University Press.[Leinster2014] Leinster, T. (2014). Rethinking set theory. The American Mathematical Monthly, 121(5), 403-415.