Categories of Filters
as Fibered Completions
Toshiki Kataoka
2016.08.08

Butz '04, “Saturated models of intuitionistic theories”•Filter logics•BFB
𝔹 ↪ F𝔹satisfies a saturation principle

Kataoka (UTokyo)

2Models withsaturation principles•

ultrafilter construction
Set(classical)
US
•

U S

filter construction [Pitts '83][Palmgren '97]
B
FB
B

•

Set(intuitionistic)
Sh(FB)( )B[Butz '04]
B

Kataoka (UTokyo)

FB
3

Blass '74, “Two closed categories of filters”•Filt(𝔹), F𝔹

Kataoka (UTokyo)

4•Filt(𝔹), F𝔹

Question

Why F𝔹 has good properties?
Why not Filt(𝔹)?

Kataoka (UTokyo)

5Answercategorical models

fibrational models
EB
Sub(B)

Filt(B)[Butz '04]

B

B

F𝔹 ≅ Filt(𝔹)[W-1](localization)

B

•

B

Kataoka (UTokyo)

FB

6

Overview
0. Introduction
1. Categories of filters [Koubek & Reiterman '70][Blass '74]
2. Categorical logic for filters [Butz '04]
3. Categorical models vs. fibrational models

Kataoka (UTokyo)

7

Overview
0. Introduction
1. Categories of filters [Koubek & Reiterman '70][Blass '74]
2. Categorical logic for filters [Butz '04]
3. Categorical models vs. fibrational models

Kataoka (UTokyo)

8Filters of a semilattice•L: (bounded) (meet-)semilattice
Definition

F : filter of L
def.

{F ⊆ L: upward closed subset s.t.
•⊤∈F•x∧y ∈ F if x ∈ F and y ∈ F
def.

F ≤ G ―――F ⊇ G
Kataoka (UTokyo)

9Definition

FL := { F : filter of L }≅ SLat(L, 2)op
cat. ofcompletesemilattices

cat. ofsemilattices
Theorem

SLat

Kataoka (UTokyo)

F-SLat

LFLMM10Filters on an object•

𝔹: category with pullbacks
Definition

F : filter on I ∈ 𝔹
def.

Kataoka (UTokyo)

F : filter of Sub𝔹(I)11Definition

Filt𝔹(I) := { F : filter on I }= F(Sub𝔹(I))

FiltB

Bop

Kataoka (UTokyo)

SubB

SLat

F-SLat12

Two categories of filters[Blass, '74]•

The category of concrete filters

Filt(𝔹)•The category of abstract filters

F𝔹

Kataoka (UTokyo)

13

Cat. of concrete filters
Filt(𝔹)•object (I, F )•morphism

Kataoka (UTokyo)(I ∈ 𝔹, F : filter on I)
u : (I, F)(J, G) in Filt(B)u: IJ in BY G. u 1 Y F

14Filt(Set)

Set[Blass '74]

Lemma

Filt(B)B

is the Grothendieck construction

from the functor FiltB : Bop

Kataoka (UTokyo)-SLat.

15

Cat. of abstract filters
F𝔹(I ∈ 𝔹, F : filter on I)•object (I, F )•morphism [v] : (I, F)(J, G)in FB

is deﬁned asv
F X
J in B
1
Y G. v Y F (under v 1 Y
underdef.
[v] = [v ]v|X = v |X (XKataoka (UTokyo)

XI)

XX)
16F(Set)

Kataoka (UTokyo)[Blass '74]

17

Definition

F = Colim B(X,X F)

:B

Set

is called the reduced product[K. ?]

Lemma𝔹 op∏(_): F𝔹 → (Set ) : fully faithful
Kataoka (UTokyo)

18

Overview
0. Introduction
1. Categories of filters [Koubek & Reiterman '70][Blass '74]
2. Categorical logic for filters [Butz '04]
3. Categorical models vs. fibrational models

Kataoka (UTokyo)

19

First-order logic andits fragments
terms
formulas“left exact logic”
regular logic
coherent logic

Kataoka (UTokyo)

t ::= x | f (t1 , . . . , t|f | )::= R(t1 , . . . , t|R| ) | t1 = t2
| | 1
2| x.
|||

1

122 |x.

20

Categorical models•

𝔹: category with finite products•

interpretation in 𝔹
•

types

⟦σ⟧ ∈ 𝔹•function symbols⟦f⟧ ∈ 𝔹(⟦σ⟧1 × … × ⟦σ⟧|f|)•relation symbols⟦R⟧ ∈ Sub𝔹(⟦σ⟧1 × … × ⟦σ⟧|R|)

Kataoka (UTokyo)

21

•

•

𝔹: left exact category(has finite limits)

𝔹 models left exact logics

𝔹: regular category

𝔹 models regular logics(lex. & has p.b.-stablecoequalizers of kernel pairs)•

𝔹: coherent category

𝔹 models coherent logics(reg. & hasp.b.-stable finite unions)•

𝔹: Heyting category

Kataoka (UTokyo)

𝔹 models first-orderlogics

22Filter logics•[Butz '04]

F𝔹 models filter logics
t ::= x | f (t1 , . . . , t|f | )::= R(t1 , . . . , t|R| ) | t1 = t2

“left exact filter logic”
regular filter logic
coherent filter logic

|| x.
| ||

Kataoka (UTokyo)

|

1

12 |

122 |x.
23Filter logics[Butz '04]

for each
0x.

1···n

for each { 1 , . . . ,n}

ﬁn.

x.

saturation(Kataoka (UTokyo))24

Characterization of F𝔹[Blass '74]

Lemma

SubF𝔹(I, F ) ≅ { (I, G ) | G ≤ F }: complete (meet-)semilattice[Butz '04]

Definition

𝔸: filtered meet lex categorydef.

𝔸: lex category,
Sub𝔸: 𝔸op →Kataoka (UTokyo)⋀-SLat25

[Butz '04]

Definition

𝔸: filtered meet lex categorydef.

𝔸: lex category,
Sub𝔸: 𝔸op →⋀-SLat[Butz '04]

Theorem

Lex

Ffilt-Lex

BFBAA

Kataoka (UTokyo)

Lex: category oflex categories
filt⋀ -Lex: category offiltered meetlex categories

26

Filtered meet vs.
arbitrary meet
arbitrary meets=ﬁnite meets + ﬁltered meetsx=(x1x X{x1 ,...,xn } X···xn )ﬁn.

Kataoka (UTokyo)27

x. (x)(x)x. (x)✗x. (x)✓✗arbitrary meets=ﬁnite meets + ﬁltered meetsx=(x1x X{x1 ,...,xn } X···xn )

ﬁn.

Kataoka (UTokyo)

28

[Butz '04]

Definitiona filtered meet regular (resp. coherent) category
is a regular (resp. coherent) category
with filtered meets s.t.
∃ (and ∨) distributes over filtered meets[Butz '04]

TheoremLex
Reg

Kataoka (UTokyo)

F

filt

F

filt

-Lex

restricts to-Reg and CohF

filt-Coh29

Filter logics[Butz '04]

for each
0x.

1···n

for each { 1 , . . . ,n}

ﬁn.

x.

()

distributive laws
Kataoka (UTokyo)

30

Overview
0. Introduction
1. Categories of filters [Koubek & Reiterman '70][Blass '74]
2. Categorical logic for filters [Butz '04]
3. Categorical models vs. fibrational models

Kataoka (UTokyo)

31

Fibrational models• Ep| : fibration, 𝔹 has finite products

B••⟦R⟧ ∈ 𝔼⟦σ⟧1 × … × ⟦σ⟧|R|Generalization of categorical model 𝔹
Sub(B)B

R
Kataoka (UTokyo)(subobject model)

for B: lex category

Sub(B)

1···|R|= SubB (1···|R| )32

Fibered completion•

Filt(B)|B

is the fibered completion ofB

FiltB

recallB
Kataoka (UTokyo)

Sub(B)

opSubBSLat

F-SLat33

Given
𝔹: categorical model ofa (lex/regular/coherent) logic[Butz '04]•

F𝔹 is the “free” (categorical) model of its filter logic[K.]•Filt(B)|B

Kataoka (UTokyo)

is the “free” fibrational model its filter logic

34

Fibrations vs. categories(General preicates vs. subobjects)

Sub(B)
B

Kataoka (UTokyo)

idFilt(B)

Sub(FB)

B

FB

35

Coproducts overmonomorphisms
Sub(B)B

X=Im( m)XJhas}m m for each monomorphism m in 𝔹
satisfying the Beck-Chevalley condition

and the Frobenius reciprocity

Kataoka (UTokyo)

m: coproduct36

Coproducts overmonomorphisms
Lemma
Sub(B)

BSub(B)

[K.]

mK
Hm
Sub(A)B

K = Sub(H)Kataoka (UTokyo)

AK
H: morphism of fibrations
preserving (1, ×, ⊤, ∧)preserves m for m: mono37

Left exact fibrations[K.]

Definition

A left exact fibration
is a fibered poset

EpBs.t.

•𝔹 has finite limits•

p has fibered finite meets•p has coproducts over monomorphisms
satisfying Frobenius

Kataoka (UTokyo)

38

[K.]

TheoremL

Lex

LexFibR

E[W1L]B
Sub(A)

A
B
where W = {(XKataoka (UTokyo)

E

A
R

E
B( m)X | m : I

J, X

EI }
39

Localization of a category•

QW: 𝔼 → 𝔼[W-1] is universal among
F: 𝔼 → 𝔻 s.t. F(w): isom. for w ∈ W

Kataoka (UTokyo)

40

Proof of the theorem (1)
H: AK
H

B: lexSub(A):E
B

A: mor. of lex ﬁbrations

L

K(A ) := ( i)where i : A

A for AA

SubA (A)Lex

LexFibR

E[W1L]B
Sub(A)A
B

Kataoka (UTokyo)

E

A
R

E
B

41

Proof of the theorem (2)K
H:E

Sub(A)BA

H : E[Wcod1]: mor. of lex ﬁbrations

A: lexL

where W = {(XM := (EK

Sub(A)

dom( m)X | m : I

J, X

EI }

Lex
RE[WA)

LexFib
1]

Kataoka (UTokyo)

B

For w ∈ W, M'w is isom. (because
Kw is opCartesian lifting, too)E
B
Sub(A)A

M induces M by the universality
•L

A
R

E
B

42Proof of the theorem (3)H : E[WK
H:1

A: lex]E

Sub(A)

B

A

where W = {(X( m)X | m : I

J, X

EI }

: mor. of lex ﬁbrations
LLex

LexFibR

M := (EQW

H(I) := M (E[W]I ) for I

K(X) := M X

Kataoka (UTokyo)

1 M

E[WA)

L]

EI

B

E
B
Sub(A)A

B

SubB (H(I)) for X

1A
R

E
B

43

fibered
completion

filt

LexFib-LexFib

Thm. [K.]Cor. [K.]

L
R

F

Lex

filt

-Lex

[Butz '04]

B
Kataoka (UTokyo)

Sub(B)

Filt(B)

B

B

FB
44

Technical condition (*)
[K.]

Lemma

EI

SubE[W 1 ] (I)Condition (*)
The embedding is an isomorphism

Kataoka (UTokyo)

45

[K.]

TheoremLex
filt-Lex

LL

LexFibfilt

restricts to-LexFib

defined on filtered meet lex fibrations satisfying (*)

filt

LexFib-LexFib
LRLex

Kataoka (UTokyo)

Ffilt-Lex46

•Define regular fibrations and coherent fibrations
as usual (e.g. [Jacobs '99])
but we require base categories 𝔹 have finite limits(not only finite products)[K.]

Theoremfilt

filt⋀ -](Reg/Coh)Fib  [⋀ -](Reg/Coh)

L restricts to [defined on fibrations satisfying (*)
R restricts to (Reg/Coh)Fib (Reg/Coh)defined on fibrations satisfying (*)
filt

LexFib-LexFibLRLex

Kataoka (UTokyo)

Ffilt-Lex47

Related work (1)••FRel(p): category of functional relations
FRel: RegFib → Reg•

objects X ∈ 𝔼•morphisms R ∈ 𝔼I×J s.t. “functional relation”

i.e. a pair (I ∈ 𝔹, X ∈ 𝔼I)

The tripos-topos construction [Pitts '81]
•objects (I ∈ 𝔹, X ∈ 𝔼I×I : “partial equivalence”)

Kataoka (UTokyo)

48

Related work (2)•Logical characterization of subobject fibrations(e.g. [Jacobs '99])•

Eq-fibration with strong equality•

has full subset types•

has unique-choice

Kataoka (UTokyo)

49

SummaryL

categorical models

ﬁbrational models
RB

FB[Butz '04]

Sub(B)

Filt(B)

B

B

Filt(B)FB = L

Kataoka (UTokyo)B, which is a localization of Filt(B)50