Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: applied category theory

Topic: kripke stuff for measure theory

sarahzrf (Apr 08 2020 at 19:53):

I saw someone mention kripke semantics stuff in the context of probability and/or measure theory earlier (in another place) and it got me wondering

sarahzrf (Apr 08 2020 at 19:54):

can you apply that somehow to automatically account for all of the "almosts" and "this is actually technically an equivalence class"?

sarahzrf (Apr 08 2020 at 19:56):

feels like maybe you're doing some kind of implicit shift to a smaller almost-everywhere set or something, the kind of thing where kripke semantics automatically moves you down some worlds

sarahzrf (Apr 08 2020 at 19:56):

or equivalently (?), maybe you're talking about some kind of germ

Matteo Capucci (he/him) (Apr 08 2020 at 21:21):

Idk about Kripke semantics, but if you have a measure space $(X, \mathcal F, \mu)$ , the topos of sheaves on $\mathcal F / \ker \mu$ has an 'almost everywhere on $\mathcal F$ ' internal logic. In other words: on $\mathrm{Sh}\mathcal F$ , there's a Lawvere-Tierney topology which corresponds to the 'almost everywhere' modality, and the closed sheaves for this topology are exactly the shaves on $\mathcal F/\ker \mu$ .

Matteo Capucci (he/him) (Apr 08 2020 at 21:22):

Here $\ker \mu = \{ A \in \mathcal F | \mu(A)=0\}$

Matteo Capucci (he/him) (Apr 08 2020 at 21:23):

I'm writing a thesis on this btw :joy:

sarahzrf (Apr 08 2020 at 21:23):

nice!

sarahzrf (Apr 08 2020 at 21:24):

/me squints

sarahzrf (Apr 08 2020 at 21:25):

when you say " $\operatorname{Sh} \mathcal{F}$ "

sarahzrf (Apr 08 2020 at 21:26):

do you mean like, $\mathcal F$ is a site where its objects are the elements of the σ-algebra and covers are just like in a topology?

sarahzrf (Apr 08 2020 at 21:27):

also what does $\mathcal F / \ker \mu$ mean o.O

sarahzrf (Apr 08 2020 at 21:28):

what kind of quotient?

Matteo Capucci (he/him) (Apr 08 2020 at 21:28):

sarahzrf said:

when you say " $\operatorname{Sh} \mathcal{F}$ "

Yeah, I mean $\mathcal F$ is a poset, so $\rm{Sh}\mathcal F = [\mathcal F^{\rm{op}}, \bf{Set}]$

sarahzrf (Apr 08 2020 at 21:28):

i mean i guess i could try to work backward to figure out what would correspond to the lawvere-tierney topology but that. sounds like a lot of work

sarahzrf (Apr 08 2020 at 21:28):

oh, i would call that $\operatorname{PSh} \mathcal{F}$ , not $\operatorname{Sh} \mathcal{F}$

sarahzrf (Apr 08 2020 at 21:29):

usually $\operatorname{Sh}$ means you have a coverage on the base category, right

sarahzrf (Apr 08 2020 at 21:30):

which youre restricting to sheaves for

Matteo Capucci (he/him) (Apr 08 2020 at 21:30):

sarahzrf said:

also what does $\mathcal F / \ker \mu$ mean o.O

It means you consider two sets equal if their symmetric difference has zero measure

sarahzrf (Apr 08 2020 at 21:30):

Matteo Capucci (he/him) (Apr 08 2020 at 21:30):

sarahzrf said:

oh, i would call that $\operatorname{PSh} \mathcal{F}$ , not $\operatorname{Sh} \mathcal{F}$

Mmh indeed, I might be too careless about that

sarahzrf (Apr 08 2020 at 21:30):

yeah ok that makes sense :3c

sarahzrf (Apr 08 2020 at 21:31):

what's a closed sheaf?

Matteo Capucci (he/him) (Apr 08 2020 at 21:31):

I mean sheaves btw, with a sheaf condition

sarahzrf (Apr 08 2020 at 21:31):

sarahzrf (Apr 08 2020 at 21:34):

wait so which instances of "sheaf" in your original post should be "presheaf" and which should really be "sheaf" >.<

sarahzrf (Apr 08 2020 at 21:34):

i'm a little confused

Matteo Capucci (he/him) (Apr 08 2020 at 21:34):

It turns out I'm way less prepared on this matter than I thought, Everything is here btw:
jackson_sheaf_theoretic_measure_theory.pdf

Matteo Capucci (he/him) (Apr 08 2020 at 21:35):

Because actually I'm taking another path in my thesis so I didn't really work out the details of this

sarahzrf (Apr 08 2020 at 21:35):

ok lol i did a double take and was about to say "wait i thought your name was matteo not matthew"

Matteo Capucci (he/him) (Apr 08 2020 at 21:35):

ahahah

sarahzrf (Apr 08 2020 at 21:36):

aha, i wasnt quite right image.png

Matteo Capucci (he/him) (Apr 08 2020 at 21:36):

btw roughly the topology is that of countable joins, i.e. you take as sieves downward closed subfamilies of $\mathcal F$ which are moreover closed under countable joins

sarahzrf (Apr 08 2020 at 21:36):

that makes more sense anyway

Matteo Capucci (he/him) (Apr 08 2020 at 21:37):

yeah exactly

Matteo Capucci (he/him) (Apr 08 2020 at 21:38):

Then you define the Lawevere-Tierney topology as $j : S \mapsto S \lor \ker \mu$

Matteo Capucci (he/him) (Apr 08 2020 at 21:38):

Where $S \in \Omega$ is a sieve as above

sarahzrf (Apr 08 2020 at 21:38):

The definition of a measure on a σ-algebra (Definition 20) can be extended to a locale:

sarahzrf (Apr 08 2020 at 21:38):

extended?

Matteo Capucci (he/him) (Apr 08 2020 at 21:38):

why not?

sarahzrf (Apr 08 2020 at 21:39):

frames and σ-algebras are sort of orthogonal, aren't they?

sarahzrf (Apr 08 2020 at 21:39):

frames are supposed to have all joins, not just countable

Matteo Capucci (he/him) (Apr 08 2020 at 21:39):

oh well

sarahzrf (Apr 08 2020 at 21:39):

but they need not have complementation or infinite infs

Matteo Capucci (he/him) (Apr 08 2020 at 21:39):

yes

Matteo Capucci (he/him) (Apr 08 2020 at 21:39):

but you still can picture a measure on them

Matteo Capucci (he/him) (Apr 08 2020 at 21:40):

as a real-valued positive function with some compatibility conditions

Matteo Capucci (he/him) (Apr 08 2020 at 21:40):

for example $\sigma$ -additivity becomes commutativity with directed joins

Matteo Capucci (he/him) (Apr 08 2020 at 21:40):

if i recall correctly

sarahzrf (Apr 08 2020 at 21:41):

looks like it yeah

Matteo Capucci (he/him) (Apr 08 2020 at 21:41):

ofc you get a different beast in general

Matteo Capucci (he/him) (Apr 08 2020 at 21:41):

the cool thing is that on the locale of closed sieves of a sigma-algebra, the two notions coincide

sarahzrf (Apr 08 2020 at 21:41):

oh hey this is reminding me of norms on cones in that talk...

sarahzrf (Apr 08 2020 at 21:41):

tangent.

Matteo Capucci (he/him) (Apr 08 2020 at 21:42):

sarahzrf said:

oh hey this is reminding me of norms on cones in that talk...

Panangaden's?

Matteo Capucci (he/him) (Apr 08 2020 at 21:42):

i accidentally missed it

Matteo Capucci (he/him) (Apr 08 2020 at 21:43):

it should be very interesting for my purposes

sarahzrf (Apr 08 2020 at 21:43):

it's only a very distant reminder :)

Matteo Capucci (he/him) (Apr 08 2020 at 21:43):

there a lot of ct approaches to this stuff!

sarahzrf (Apr 08 2020 at 21:43):

btw for the record when you said "Idk about Kripke semantics":

sarahzrf (Apr 08 2020 at 21:44):

kripke semantics for intuitionistic logic are pretty much strictly generalized by presheaf and sheaf theory

Matteo Capucci (he/him) (Apr 08 2020 at 21:44):

yeah I'm aware

sarahzrf (Apr 08 2020 at 21:44):

ah :)

Matteo Capucci (he/him) (Apr 08 2020 at 21:45):

but I'm far more familiar with the latter than the former

sarahzrf (Apr 08 2020 at 21:45):

:thumbs_up:

Matteo Capucci (he/him) (Apr 08 2020 at 21:45):

and as you see I'm not very familiar with the latter actually XD

sarahzrf (Apr 08 2020 at 21:45):

well, the kripke semantics for intuitionistic logic over some preordered kripke frame F are recovered pretty much literally in the heyting algebra of subsingletons/truth-values of PSh(F)

Matteo Capucci (he/him) (Apr 08 2020 at 21:45):

I intuitively grasp a lot in topos theory, but my katas are quite weak tbh

sarahzrf (Apr 08 2020 at 21:46):

or equivalently

sarahzrf (Apr 08 2020 at 21:46):

the heyting algebra of (0, 1)-presheaves (downward-closed subsets) on PSh(F)

sarahzrf (Apr 08 2020 at 21:46):

also me too lol

Matteo Capucci (he/him) (Apr 08 2020 at 21:47):

mmh so a Kripke frame is that pair (W, accessbility relation)?

sarahzrf (Apr 08 2020 at 21:48):

yeah

sarahzrf (Apr 08 2020 at 21:48):

upward-closed subsets is probably more traditional in kripke semantics but it's not really a big difference

Matteo Capucci (he/him) (Apr 08 2020 at 21:48):

now it's me who don't follow how you put a sheaf on that XD

sarahzrf (Apr 08 2020 at 21:48):

just ^op the W

sarahzrf (Apr 08 2020 at 21:48):

i said PSh

Matteo Capucci (he/him) (Apr 08 2020 at 21:48):

sarahzrf said:

just ^op the W

that's my fav sport

Matteo Capucci (he/him) (Apr 08 2020 at 21:49):

sarahzrf said:

i said PSh

yeah

Matteo Capucci (he/him) (Apr 08 2020 at 21:49):

oh well the accessibility is a preorder right?

sarahzrf (Apr 08 2020 at 21:49):

yeah

sarahzrf (Apr 08 2020 at 21:49):

for intuitionistic logic

Matteo Capucci (he/him) (Apr 08 2020 at 21:49):

sarahzrf (Apr 08 2020 at 21:49):

kripke semantics for modal logic is a little dicier i guess

Matteo Capucci (he/him) (Apr 08 2020 at 21:49):

i guess

sarahzrf (Apr 08 2020 at 21:50):

"dicier" as far as mapping cleanly to a categorical notion i mean

Matteo Capucci (he/him) (Apr 08 2020 at 21:50):

sarahzrf said:

well, the kripke semantics for intuitionistic logic over some preordered kripke frame F are recovered pretty much literally in the heyting algebra of subsingletons/truth-values of PSh(F)

ok now i see this

sarahzrf (Apr 08 2020 at 21:50):

Matteo Capucci (he/him) (Apr 08 2020 at 21:50):

it's almost tautological, indeed

Matteo Capucci (he/him) (Apr 08 2020 at 21:50):

your truth values are these sieves of worlds

sarahzrf (Apr 08 2020 at 21:51):

yup

Matteo Capucci (he/him) (Apr 08 2020 at 21:51):

it's a good idea

Matteo Capucci (he/him) (Apr 08 2020 at 21:51):

good boy kripke

sarahzrf (Apr 08 2020 at 21:51):

and then the heyting algebra structure corresponds exactly to the written-out clauses youd see for kripke semantics

Matteo Capucci (he/him) (Apr 08 2020 at 21:52):

magnifique!

sarahzrf (Apr 08 2020 at 21:52):

which is not too surprising for ∨ and ∧

sarahzrf (Apr 08 2020 at 21:52):

but it freaked me out when i saw it the first time for →

sarahzrf (Apr 08 2020 at 21:52):

image.png

Matteo Capucci (he/him) (Apr 08 2020 at 21:53):

sarahzrf said:

image.png

HAHAHAHAHA that's so true

Matteo Capucci (he/him) (Apr 08 2020 at 21:54):

I think kripke semantics is one of those cases of future math discovered earlier, so it's clean concepts in sheaf theory with a lot of bizarre costumes

Matteo Capucci (he/him) (Apr 08 2020 at 21:55):

same thing goes on with forcing: you have this wild idea of cohen whose core is basically 'do set theory in a topos of sheaves'

sarahzrf (Apr 08 2020 at 21:56):

:harvest:

sarahzrf (Apr 08 2020 at 21:58):

maybe someday i will truly understand why the cartesian closed structure of the category of functors into a complete CCC is what it is...... til then i just remember "its the kripke thing" and the yoneda argument for it :pensive: