ファイル置き場 Sendai Logic Homepage speaker1

Categorical Structures of Basic Pairs and

Concrete Spaces

Tatsuji Kawai

Japan Advanced Institute of Science and Technology

February 24, 2012

Introduction

Several competing notions of general topology exist in constructive mathematics:

◮ Neighbourhood space — Topology with base

◮ Formal topology — Point-free

◮ Basic pair and concrete space — Similar to neighbourhood space but with difference in maps

Theorem (Ishihara and K, 2012)

The category of basic pairs and concrete spaces are complete and cocomplete.

Constructive Zermelo-Frankel Set Theory (CZF)

Set theory for constructive mathematics based on ZF.

◮ Uses intuitionistic logic — no excluded middle ϕ∨ ¬ϕ.

◮ No Powerset — Pow(X) is not a set.

◮ Restricted separation —{x ∈ X | ϕ(x)} is a set only for restricted formula ϕ; quantifications must be of the forms

∀x ∈ a or ∃x ∈ a.

◮ Has an interpretation in Martin-Löf’s Intuitionistic Type Theory (ITT) [Aczel 1977,1982,1986].

Basic Pairs

Definition (Basic Pair)

Abasic pairis a triple(X, , S) where X and S are sets and ⊆ X × S is a relation.

Maps between basic pairs

Definition (Relation Pair)

A mapping between basic pairs(X¹, ¹, S¹) and (X², ², S²) is a pair(r, s) of relations r ⊆ X1× X2and s⊆ S1× S2 such that

₂ ◦ r = s ◦ 1

X1 r



₁

//_S

1 s



X2 2

//_S2

where◦ is the composition of relations:

r²◦ r¹= {(x, z) ∈ X × Z | (∃y ∈ Y) x r¹y∧ y r²z} for r1⊆ X × Y, and r2⊆ Y × Z.

The pair(r, s) is called arelation pair.

Equivalent relation pairs

Definition

Two relation pairs(r¹, s1_{), (r}2, s2) : (X, , S) → (X^′, ^′, S^′) are said to beequivalent,(r1, s1) ∼ (r2, s2), if

^′ _◦r1 ₌ ^′ _◦r2

s1◦ = s2◦

X

r1



r2



//_S

s1



s2



X^′

′

//_S′

∼ is an equivalence relation on the relation pairs from X to X^′.

Category

Definition (Category) AcategoryC consists of:

◮ Objects — A, B, C, . . .

◮ Arrows — f , g, h, . . .

◮ Each arrow f is assigned objects dom(f ), cod(f ). f : A → B ⇐⇒ dom(f ) = A & cod(f ) = B^def

◮ _{For any f} : A → B and g : B → C, there is an arrow g◦ f : A → C.

◮ For each object A, there is an arrow 1A: A → A. Those are required to satisfy

(Associativity) h◦ (g ◦ f ) = (h ◦ g) ◦ f , (Identity) f◦ 1dom_{(f )}= f = 1cod_{(f )}◦ f .

Category of Basic Pair (BP)

Definition (The category BP)

The category of basic pair BP consists of

◮ Objects — basic pairs(X, , S), (Y, ^′, T), · · ·

◮ Arrows — equivalence classes of relation pairs (r, s), (u, v), · · ·

◮ Composition is defined by

(u, v)◦(r, s) = (u ◦ r, v ◦ s)

X1 1

//

r



u◦r



S1 s



v◦s



X^{2 2 //}

u



S²

v



X^{3 3 //}S3

◮ The identity on(X, , S) is (idX^{, id}S) where id_X = {(x, x) | x ∈ X} .

Completeness of categories

Definition (Completeness)

A category iscompleteif it has all limits. Proposition

A category is complete if and only if it has

◮ a product for any family of objects(A_i)_i∈I,

◮ an equaliser for any pair of arrows A ^{f //}

g ^{//B .}

Products

Definition (Product)

Aproductfor a family of objects(A_i)_i∈I is an object^Q_i∈IA_i together with a family of arrows

π_i :^Q_i∈IA_i → A_i
i∈I such that for any family of arrows(f_i: T → A_i)_i∈I, there is unique arrow h: T →^Q_i∈IAisuch that

T

fi

%%

KK KK KK KK KK KK

h



Q

i∈I^Ai πi

//_A

i

f_i = π_i◦ h

for all i∈ I.

Equalisers

Definition (Equaliser)

Anequaliserfor any pair of arrows A

f //

g ^//B is an arrow e: E → A such that

◮ _E ^e //_A

f //

g ^//B , i.e. f ◦ e = g ◦ e,

◮ _{for any h}: T → A such that T ^{h //}A

f //

g ^{//B ,}

there is a unique arrow u: T → E such that T

h

##

FF FF F FF FF

u



E ^{e //}A

f //

g ^//B

h= e ◦ u.

Cocompleteness of categories

Definition (Cocompleteness)

A category iscocompleteif it has all colimits. Proposition

A category is cocomplete if and only if it has

◮ a coproduct for any family of objects(A_i)_i∈I,

◮ a coequaliser for any pair of arrows A ^{f //}

g ^{//B .}

Coproduct

Definition (Coproducts)

Acoproductfor a family of objects(A_i)_i∈I is an object^`_i∈IAi

together with a family of arrows

σ_i : Ai→^`_i∈IAi

i∈I

such that for any family of arrows(f_i: A_i → T)_i∈I, there is unique arrow h:^`_i∈IA_i→ T such that

A_i ^{σi //`}_i∈IA_i

h



T

fi

%%

KK KK KK KK KK KK

fi = h ◦ σi

for all i∈ I.

Coequaliser

Definition (Coequalisers)

Acoequaliserfor any pair of arrows A

f //

g ^//B is an arrow q: B → Q such that

◮ _A f //

g ^//B

q //_{Q, i.e. q}◦ f = q ◦ g,

◮ _{for any h}: B → T such that A ^{f //}

g ^//B h

//_{T ,}

there is a unique arrow u: Q → T such that

A

f //

g ^//B

q //_Q

u



T

h ^II_I$$ II II

II _{h= u ◦ q.}

Coproducts in BP

Proposition

BP has coproducts.

Proof.

Given a family of basic pairs(X_i)_i∈I, define a basic pair

`

i∈I^{Xi= (}

P

i∈I^{Xi, Σ,}

P

i∈I^{Si) by}

_Σ=((i, x), (j, a)) ∈ P_i∈IXi×^P_i∈ISi | i = j & x i a and a family of relation pairs (r_i, s_i) : X_i→^`_i∈IX_i
i∈I by

ri =(x, (j, x^′)) ∈ Xi×^P_i∈IXi | i = j & x = x^′ , si ⁼(a, (j, a^′)) ∈ S_i×^P_i∈ISi | i = j & a = a^′ .

Set-generated Class

Definition

A class C of subsets of a set S isset-generatedif there is a subset G of C such that

(∀U ∈ C) (∀σ ∈ Fin (U)) (∃V ∈ G) σ ⊆ V ⊆ U, where

◮ Fin(X) is the set of finitely enumerable subsets X A set A isfinitely enumerable

⇐⇒ there is a surjection f : n = {0, · · · , n − 1} → Adef

◮ _Gis called agenerating subsetof C

Generalized Geometric Theory

Definition

Ageneralized geometric implication(simply implication) and ageneralized geometric theory(simply theory) over a set S, and their ranks, are defined simultaneously by

1. sis an implication of rank 0 for each s∈ S;

2. if σ∈ Fin(S) and Γ is a set of theories of rank n, then V σ → W_U∈ΓV U

is an implication of rank n+ 1;

3. a set T of implications of rank≤ n is a theory of rank n.

Model of a theory

Definition

The relation|= between a set α ∈ Pow(S), and implications s (of rank 0),V σ → W_U∈ΓV U (of positive rank) and a theory T over Sis defined by

1. α|= s if s ∈ α;

2. α|=V σ → W_U∈ΓV U if σ ⊆ α implies α |= U for some U∈ Γ;

3. α|= T if α |= θ for all θ ∈ T.

A set α∈ Pow(S) is amodelof a theory T if α|= T.

Fundamental theorem

Theorem (Aczel, Ishihara, Nemoto, Sangu 2012)

Assuming RRS²-uREA or RDC, the class M(T) of models of a theory T of rank n is set-generated.

Coequalisers in BP

Proposition

BP has coequalisers. Proof.

Given a pair of relation pairs (X1, 1, S1) = X1

(r¹,s1₎

//

(r2,s2)

//X2= (X2, 2, S2) ,

define a class Q by

Q=U ∈ Pow(S²) | (s1◦ 1)⁻U = (s2◦ 1)⁻U . Qis the class of models of the theory T over the set S2.

T =ⁿV{a} → V_{x∈(s1◦ 1)}⁻_{a}^W_{b∈(s2◦ ){x}}V{b}a∈ S2

o

∪ⁿV{a} → V_{x∈(s2◦ 1)}⁻_{a}^W_{b∈(s1◦ ){x}}V{b}a∈ S^2o.

Coequalisers in BP Proof continued.

Q=U ∈ Pow(S²) | (s¹◦ ¹)⁻U = (s²◦ ¹)⁻U . (s¹◦ ¹)⁻U = (s²◦ ¹)⁻U

⇐⇒ (s1◦ 1)⁻U⊆ (s2◦ 1)⁻U& (s1◦ 1)⁻U ⊇ (s2◦ 1)⁻U. (s1◦ 1)⁻U ⊆ (s2◦ 1)⁻U

⇐⇒ (∀a ∈ U) (s1◦ 1)⁻{a} ⊆ (s2◦ 1)⁻U

⇐⇒ (∀a ∈ U) ∀x (s¹◦ ¹)⁻{a}
(∃b ∈ (s²◦ ¹) {x}) b ∈ U T =ⁿV{a} → V_{x∈(s1◦ 1)}⁻_{a}^W_{b∈(s2◦ ){x}}V{b}a∈ S^2o

∪ⁿV{a} → V_{x∈(s2◦ 1)}−_{a}

W

b∈(s1◦ ){x}^V{b}

 a∈ S2

o .

Coequalisers in BP

Proof continued.

Therefore, the class Q has a generating subset G. Then

X2

(id_X2,∈)

//_{G = (X}

2, _G, G)

X2 id_X2



2

//_S2

∈



X2 _G

//_G

where

_G = {(x, U) ∈ X2× G | (∃a ∈ U) x 2a}

is a coequaliser for X¹

(r1,s1)

//

(r2,s2)

//_X2_.

Completeness and Cocompleteness of BP

Corollary

BP is cocomplete.

Proposition

BP is isomorphic to its own dual, i.e. BP ∼= BP^op.

Corollary BP is complete.

Concrete Space

Definition (Concrete Space)

Aconcrete spaceis a basic pair(X, , S) which satisfies (B1) ext(S) = X,

(B2) ext(a) ∩ ext(b) = ext(a ↓ b), where

ext(a) = {x ∈ X | x a} , ext(U) =^S_a∈Uext(a),

a↓ b = {c ∈ S | ext(c) ⊆ ext(a) ∩ ext(b)} . for a, b∈ S and U ⊆ S.

Convergent Relation Pair

Definition (Convergent Relation Pair)

A mapping between concrete spacesX¹ = (X¹, ¹, S¹) and X2= (X2, 2, S2) is a relation pair (r, s) : X1→ X2such that

(C1) r⁻ext(a ↓ b) = ext (s⁻a↓ s⁻b), (C2) r⁻ext S2= ext S1

for a, b∈ S², where

r⁻(U) = {x ∈ X | (∃y ∈ U) x r y} for a relation r⊆ X × Y.

A relation pair(r, s) which satisfies (C1) and (C2) is called a convergent relation pair.

Category of Concrete Space (CSpa)

Definition (The category CSpa)

The category of concrete spaces CSpa consists of

◮ Objects — concrete spaces(X, , S), (Y, ^′, T), · · ·

◮ Arrows — convergent relation pairs(r, s), (u, v), · · ·

◮ Composition of arrows and identity arrows

— defined as in BP:

(u, v) ◦ (r, s) = (u ◦ r, v ◦ s), 1_{X = (idX, idS)} for a concrete spaceX = (X, , S).

Completeness and Cocompleteness of CSpa

Proposition

The category of concrete spaces (CSpa) has (co)products and (co)equalisers.

Theorem (Ishihara and K, 2012) CSpa is complete and cocomplete.

RRS_2-uREA

A set A isregularif

◮ it is transitive, i.e. a⊆ A for each a ∈ A,

◮ _{for each a}∈ A and R ⊆ a × A such that

(∀x ∈ a) (∃y ∈ A) (x, y) ∈ R, there exists b ∈ A such that (∀x ∈ a) (∃y ∈ b) (x, y) ∈ R & (∀y ∈ b) (∃x ∈ a) (x, y) ∈ R. A set A isunion-closedifS a ∈ A for each a ∈ A.

A regular set A is^RRS2-regularif for each A^′ ∈ Pow(A) and R⊆ (A^′× A^′) × A^′such that∀(x, y) ∈ A^′× A^′∃z ∈ A^′((x, y), z) ∈ R, for each a⁰∈ A^′, there exists A⁰∈ A such that a⁰∈ A⁰⊆ A^′ and

∀(x, y) ∈ A0× A0∃z ∈ A0((x, y), z) ∈ R. Definition (RRS²-uREA)

Every set is a subset of a union-closed RRS2-regular set.

Relativised Dependent Choice

Definition (RDC)

For any formulae ϕ and ψ, if∀x [ϕ(x) → ∃y [ϕ(y) ∧ ψ(x, y)]] and ϕ(a0), then there exists a function f with domain N such that f(0) = a⁰ and∀n ∈ N [ϕ(f (n)) ∧ ψ(f (n), f (n + 1))].