#!if 넘어옴1 != null
'''ETCS'''{{{#!if 넘어옴2 == null
{{{#!if 넘어옴1[넘어옴1.length - 1] >= 0xAC00 && 넘어옴1[넘어옴1.length - 1] <= 0xD7A3
{{{#!if ((넘어옴1[넘어옴1.length - 1] - 0xAC00) % 28) == 0
는}}}{{{#!if ((넘어옴1[넘어옴1.length - 1] - 0xAC00) % 28) != 0
은}}}}}}{{{#!if 넘어옴1[넘어옴1.length - 1] < 0xAC00 || 넘어옴1[넘어옴1.length - 1] > 0xD7A3
은(는)}}}}}}{{{#!if 넘어옴2 != null
, ''''''{{{#!if 넘어옴3 == null
{{{#!if 넘어옴2[넘어옴2.length - 1] >= 0xAC00 && 넘어옴2[넘어옴2.length - 1] <= 0xD7A3
{{{#!if ((넘어옴2[넘어옴2.length - 1] - 0xAC00) % 28) == 0
는}}}{{{#!if ((넘어옴2[넘어옴2.length - 1] - 0xAC00) % 28) != 0
은}}}}}}{{{#!if 넘어옴2[넘어옴2.length - 1] < 0xAC00 || 넘어옴2[넘어옴2.length - 1] > 0xD7A3
은(는)}}}}}}}}}{{{#!if 넘어옴3 != null
, ''''''{{{#!if 넘어옴4 == null
{{{#!if 넘어옴3[넘어옴3.length - 1] >= 0xAC00 && 넘어옴3[넘어옴3.length - 1] <= 0xD7A3
{{{#!if ((넘어옴3[넘어옴3.length - 1] - 0xAC00) % 28) == 0
는}}}{{{#!if ((넘어옴3[넘어옴3.length - 1] - 0xAC00) % 28) != 0
은}}}}}}{{{#!if 넘어옴3[넘어옴3.length - 1] < 0xAC00 || 넘어옴3[넘어옴3.length - 1] > 0xD7A3
은(는)}}}}}}}}}{{{#!if 넘어옴4 != null
, ''''''{{{#!if 넘어옴5 == null
{{{#!if 넘어옴4[넘어옴4.length - 1] >= 0xAC00 && 넘어옴4[넘어옴4.length - 1] <= 0xD7A3
{{{#!if ((넘어옴4[넘어옴4.length - 1] - 0xAC00) % 28) == 0
는}}}{{{#!if ((넘어옴4[넘어옴4.length - 1] - 0xAC00) % 28) != 0
은}}}}}}{{{#!if 넘어옴4[넘어옴4.length - 1] < 0xAC00 || 넘어옴4[넘어옴4.length - 1] > 0xD7A3
은(는)}}}}}}}}}{{{#!if 넘어옴5 != null
, ''''''{{{#!if 넘어옴6 == null
{{{#!if 넘어옴5[넘어옴5.length - 1] >= 0xAC00 && 넘어옴5[넘어옴5.length - 1] <= 0xD7A3
{{{#!if ((넘어옴5[넘어옴5.length - 1] - 0xAC00) % 28) == 0
는}}}{{{#!if ((넘어옴5[넘어옴5.length - 1] - 0xAC00) % 28) != 0
은}}}}}}{{{#!if 넘어옴5[넘어옴5.length - 1] < 0xAC00 || 넘어옴5[넘어옴5.length - 1] > 0xD7A3
은(는)}}}}}}}}}{{{#!if 넘어옴6 != null
, ''''''{{{#!if 넘어옴7 == null
{{{#!if 넘어옴6[넘어옴6.length - 1] >= 0xAC00 && 넘어옴6[넘어옴6.length - 1] <= 0xD7A3
{{{#!if ((넘어옴6[넘어옴6.length - 1] - 0xAC00) % 28) == 0
는}}}{{{#!if ((넘어옴6[넘어옴6.length - 1] - 0xAC00) % 28) != 0
은}}}}}}{{{#!if 넘어옴6[넘어옴6.length - 1] < 0xAC00 || 넘어옴6[넘어옴6.length - 1] > 0xD7A3
은(는)}}}}}}}}}{{{#!if 넘어옴7 != null
, ''''''{{{#!if 넘어옴8 == null
{{{#!if 넘어옴7[넘어옴7.length - 1] >= 0xAC00 && 넘어옴7[넘어옴7.length - 1] <= 0xD7A3
{{{#!if ((넘어옴7[넘어옴7.length - 1] - 0xAC00) % 28) == 0
는}}}{{{#!if ((넘어옴7[넘어옴7.length - 1] - 0xAC00) % 28) != 0
은}}}}}}{{{#!if 넘어옴7[넘어옴7.length - 1] < 0xAC00 || 넘어옴7[넘어옴7.length - 1] > 0xD7A3
은(는)}}}}}}}}}{{{#!if 넘어옴8 != null
, ''''''{{{#!if 넘어옴9 == null
{{{#!if 넘어옴8[넘어옴8.length - 1] >= 0xAC00 && 넘어옴8[넘어옴8.length - 1] <= 0xD7A3
{{{#!if ((넘어옴8[넘어옴8.length - 1] - 0xAC00) % 28) == 0
는}}}{{{#!if ((넘어옴8[넘어옴8.length - 1] - 0xAC00) % 28) != 0
은}}}}}}{{{#!if 넘어옴8[넘어옴8.length - 1] < 0xAC00 || 넘어옴8[넘어옴8.length - 1] > 0xD7A3
은(는)}}}}}}}}}{{{#!if 넘어옴9 != null
, ''''''{{{#!if 넘어옴10 == null
{{{#!if 넘어옴9[넘어옴9.length - 1] >= 0xAC00 && 넘어옴9[넘어옴9.length - 1] <= 0xD7A3
{{{#!if ((넘어옴9[넘어옴9.length - 1] - 0xAC00) % 28) == 0
는}}}{{{#!if ((넘어옴9[넘어옴9.length - 1] - 0xAC00) % 28) != 0
은}}}}}}{{{#!if 넘어옴9[넘어옴9.length - 1] < 0xAC00 || 넘어옴9[넘어옴9.length - 1] > 0xD7A3
은(는)}}}}}}}}}{{{#!if 넘어옴10 != null
, ''''''{{{#!if 넘어옴10[넘어옴10.length - 1] >= 0xAC00 && 넘어옴10[넘어옴10.length - 1] <= 0xD7A3
{{{#!if ((넘어옴10[넘어옴10.length - 1] - 0xAC00) % 28) == 0
는}}}{{{#!if ((넘어옴10[넘어옴10.length - 1] - 0xAC00) % 28) != 0
은}}}}}}{{{#!if 넘어옴10[넘어옴10.length - 1] < 0xAC00 || 넘어옴10[넘어옴10.length - 1] > 0xD7A3
은(는)}}}}}} 여기로 연결됩니다. #!if 설명 == null && 리스트 == null
{{{#!if 설명1 == null
다른 뜻에 대한 내용은 아래 문서를}}}{{{#!if 설명1 != null
{{{#!html 유럽형 열차제어시스템 'European Train Control System'}}}에 대한 내용은 [[열차자동방호장치]] 문서{{{#!if (문단1 == null) == (앵커1 == null)
를}}}{{{#!if 문단1 != null & 앵커1 == null
의 [[열차자동방호장치#s-2|2]]번 문단을}}}{{{#!if 문단1 == null & 앵커1 != null
의 [[열차자동방호장치#|]] 부분을}}}}}}{{{#!if 설명2 != null
, {{{#!html }}}에 대한 내용은 [[]] 문서{{{#!if (문단2 == null) == (앵커2 == null)
를}}}{{{#!if 문단2 != null & 앵커2 == null
의 [[#s-|]]번 문단을}}}{{{#!if 문단2 == null & 앵커2 != null
의 [[#|]] 부분을}}}}}}{{{#!if 설명3 != null
, {{{#!html }}}에 대한 내용은 [[]] 문서{{{#!if (문단3 == null) == (앵커3 == null)
를}}}{{{#!if 문단3 != null & 앵커3 == null
의 [[#s-|]]번 문단을}}}{{{#!if 문단3 == null & 앵커3 != null
의 [[#|]] 부분을}}}}}}{{{#!if 설명4 != null
, {{{#!html }}}에 대한 내용은 [[]] 문서{{{#!if (문단4 == null) == (앵커4 == null)
를}}}{{{#!if 문단4 != null & 앵커4 == null
의 [[#s-|]]번 문단을}}}{{{#!if 문단4 == null & 앵커4 != null
의 [[#|]] 부분을}}}}}}{{{#!if 설명5 != null
, {{{#!html }}}에 대한 내용은 [[]] 문서{{{#!if (문단5 == null) == (앵커5 == null)
를}}}{{{#!if 문단5 != null & 앵커5 == null
의 [[#s-|]]번 문단을}}}{{{#!if 문단5 == null & 앵커5 != null
의 [[#|]] 부분을}}}}}}{{{#!if 설명6 != null
, {{{#!html }}}에 대한 내용은 [[]] 문서{{{#!if (문단6 == null) == (앵커6 == null)
를}}}{{{#!if 문단6 != null & 앵커6 == null
의 [[#s-|]]번 문단을}}}{{{#!if 문단6 == null & 앵커6 != null
의 [[#|]] 부분을}}}}}}{{{#!if 설명7 != null
, {{{#!html }}}에 대한 내용은 [[]] 문서{{{#!if (문단7 == null) == (앵커7 == null)
를}}}{{{#!if 문단7 != null & 앵커7 == null
의 [[#s-|]]번 문단을}}}{{{#!if 문단7 == null & 앵커7 != null
의 [[#|]] 부분을}}}}}}{{{#!if 설명8 != null
, {{{#!html }}}에 대한 내용은 [[]] 문서{{{#!if (문단8 == null) == (앵커8 == null)
를}}}{{{#!if 문단8 != null & 앵커8 == null
의 [[#s-|]]번 문단을}}}{{{#!if 문단8 == null & 앵커8 != null
의 [[#|]] 부분을}}}}}}{{{#!if 설명9 != null
, {{{#!html }}}에 대한 내용은 [[]] 문서{{{#!if (문단9 == null) == (앵커9 == null)
를}}}{{{#!if 문단9 != null & 앵커9 == null
의 [[#s-|]]번 문단을}}}{{{#!if 문단9 == null & 앵커9 != null
의 [[#|]] 부분을}}}}}}{{{#!if 설명10 != null
, {{{#!html }}}에 대한 내용은 [[]] 문서{{{#!if (문단10 == null) == (앵커10 == null)
를}}}{{{#!if 문단10 != null & 앵커10 == null
의 [[#s-|]]번 문단을}}}{{{#!if 문단10 == null & 앵커10 != null
의 [[#|]] 부분을}}}}}}#!if 설명 == null
{{{#!if 리스트 != null
다른 뜻에 대한 내용은 아래 문서를}}} 참고하십시오.#!if 리스트 != null
{{{#!if 문서명1 != null
* {{{#!if 설명1 != null
유럽형 열차제어시스템 'European Train Control System': }}}[[열차자동방호장치]] {{{#!if 문단1 != null & 앵커1 == null
문서의 [[열차자동방호장치#s-2|2]]번 문단}}}{{{#!if 문단1 == null & 앵커1 != null
문서의 [[열차자동방호장치#|]] 부분}}}}}}{{{#!if 문서명2 != null
* {{{#!if 설명2 != null
: }}}[[]] {{{#!if 문단2 != null & 앵커2 == null
문서의 [[#s-|]]번 문단}}}{{{#!if 문단2 == null & 앵커2 != null
문서의 [[#|]] 부분}}}}}}{{{#!if 문서명3 != null
* {{{#!if 설명3 != null
: }}}[[]] {{{#!if 문단3 != null & 앵커3 == null
문서의 [[#s-|]]번 문단}}}{{{#!if 문단3 == null & 앵커3 != null
문서의 [[#|]] 부분}}}}}}{{{#!if 문서명4 != null
* {{{#!if 설명4 != null
: }}}[[]] {{{#!if 문단4 != null & 앵커4 == null
문서의 [[#s-|]]번 문단}}}{{{#!if 문단4 == null & 앵커4 != null
문서의 [[#|]] 부분}}}}}}{{{#!if 문서명5 != null
* {{{#!if 설명5 != null
: }}}[[]] {{{#!if 문단5 != null & 앵커5 == null
문서의 [[#s-|]]번 문단}}}{{{#!if 문단5 == null & 앵커5 != null
문서의 [[#|]] 부분}}}}}}{{{#!if 문서명6 != null
* {{{#!if 설명6 != null
: }}}[[]] {{{#!if 문단6 != null & 앵커6 == null
문서의 [[#s-|]]번 문단}}}{{{#!if 문단6 == null & 앵커6 != null
문서의 [[#|]] 부분}}}}}}{{{#!if 문서명7 != null
* {{{#!if 설명7 != null
: }}}[[]] {{{#!if 문단7 != null & 앵커7 == null
문서의 [[#s-|]]번 문단}}}{{{#!if 문단7 == null & 앵커7 != null
문서의 [[#|]] 부분}}}}}}{{{#!if 문서명8 != null
* {{{#!if 설명8 != null
: }}}[[]] {{{#!if 문단8 != null & 앵커8 == null
문서의 [[#s-|]]번 문단}}}{{{#!if 문단8 == null & 앵커8 != null
문서의 [[#|]] 부분}}}}}}{{{#!if 문서명9 != null
* {{{#!if 설명9 != null
: }}}[[]] {{{#!if 문단9 != null & 앵커9 == null
문서의 [[#s-|]]번 문단}}}{{{#!if 문단9 == null & 앵커9 != null
문서의 [[#|]] 부분}}}}}}{{{#!if 문서명10 != null
* {{{#!if 설명10 != null
: }}}[[]] {{{#!if 문단10 != null & 앵커10 == null
문서의 [[#s-|]]번 문단}}}{{{#!if 문단10 == null & 앵커10 != null
문서의 [[#|]] 부분}}}}}}| [[범주론|'''범주론 {{{#!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> 개념 | 범주(종류 · 여러 가지 범주 · Set) · 대상(부분 대상) · 사상(정의역과 공역 · Hom · 항등 사상 · 동형 사상) · 함자(항등 함자 · Hom-함자 · 범주의 동치) · 자연 변환(자연 동형) · 수반쌍 · 보편 성질 · 퀴버(quiver) · 자기 동형 사상군 · 모노이달 범주(모노이드 대상) |
| 범주의 종류 및 구성 | 곱범주 · 콤마 범주(조각 범주) · 자유 범주 · 준군(groupoid)(기본준군) · 반대 범주 · 함자 범주(화살 범주) | |
| 극한 | 다이어그램(가환 다이어그램) · 극한↔쌍대극한op · 끝↔시작op(영대상 · 영사상) · 곱↔쌍대곱op · 이퀄라이저(핵)↔코이퀄라이저op(공핵) · 당김↔밂op · 완비 범주 | |
| 하위 분야 | 범주론적 대수학 · 고차 범주론 · 풍성 범주론(enriched category theory) · 토포스 이론(ETCS) · 대수적 집합론 | |
| 기타 | 교재(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> 기본 대상 | 집합(표기 · ∈) · 공집합 · 싱글톤 · 부분집합 · 모임(수학) · 공리 · 순서쌍 · 첨수 집합족 | ||
| [[모델 이론#theory|{{{#fff,#fff 이론}}}]] 및 [[모델 이론#model|{{{#fff,#fff 모델}}}]] | ZFC 공리계 · NBG 공리계 · ETCS · 그로텐디크 우주 · 대수적 집합론 | ||
| 연산 | 멱집합 · 곱집합 · 드모르간 법칙 · 분리 합집합 | ||
| 관계 | 이항 관계 · 반사성 · 대칭성 · 추이성 · 동치관계 · 부분함수 · 순서 관계(부분 순서 · 하세 다이어그램) · 삼항 관계 | ||
| 함수 | 정의역과 공역 · 단사와 전사 · 함수의 합성 · 역함수 · 자기함수 · 포함함수 · 항등함수 · 공함수 · 상수함수 | ||
| 자연수 | 페아노 공리계 · 재귀 정리 · 정렬 원리 · 수학적 귀납법 | ||
| 기수 · 서수 | 가산집합 · 선택공리(초른의 보조정리 · 하우스도르프 극대 원리) · 초한기수(힐베르트의 호텔) · 슈뢰더-베른슈타인 정리 · 대각선 논법 · 연속체 가설 · 추이적 집합 · 큰 가산서수 · 우주(집합론) | ||
| 기타 | 러셀의 역설 · 집합론 교재 | }}}}}}}}} | |
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.