applicative ultrapower

Stream: maths

[David Wärn]

Currently if you want to lift a function / relation from the reals to the hyperreals, then there are separate functions for this depending on the arity of your function (1 or 2) and whether or not it is a relation -- see https://github.com/leanprover-community/mathlib/blob/master/src/order/filter/filter_product.lean#L40 .

We can do this more uniformly by noting that 'taking ultrapowers' is an applicative functor: https://gist.github.com/dwarn/35d168349a298d3312534fe622c7f56e .

Can we 'lift theorems' in a similar way? applicative provides very nice language for turning say a monoid structure on M into a monoid structure on upower M, but how do we prove the monoid axioms? It seems like we need more than just the applicative laws here. We have internal function types, but can we define 'internal dependent products'?

If Lean were a first-order theory like ZFC, you could say "pick a universe V, and consider the elementary embedding V -> *V" -- I'm trying to do something analogous to this, but it seems hard as the "theory of Lean" is fairly complicated.

[Jesse Michael Han]

i think your setup looks closer to the filterquotient construction for toposes than the ultrapower construction for first-order models; the category of types in Lean is not quite a topos, but there is a version of the transfer principle for filterquotients

[Bhavik Mehta]

Jesse Michael Han said:

category of types in Lean is not quite a topos

Could you justify this? I'm pretty sure it is, even if the proof needs some form of choice

[Jesse Michael Han]

oh, i think i meant not quite a Grothendieck topos; seems like filterquotients indeed make sense for just elementary toposes.

even if the proof needs some form of choice

i think you can do it with just unique choice (for inverting injections)

[Kevin Buzzard]

Isn't it great when mathematicians use the same word to mean two different things

[Bhavik Mehta]

Jesse Michael Han said:

oh, i think i meant not quite a Grothendieck topos; seems like filterquotients indeed make sense for just elementary toposes.

even if the proof needs some form of choice

i think you can do it with just unique choice (for inverting injections)

Yeah, I did it with unique choice

[David Wärn]

Jesse Michael Han said:

i think your setup looks closer to the filterquotient construction for toposes than the ultrapower construction for first-order models; the category of types in Lean is not quite a topos, but there is a version of the transfer principle for filterquotients

Ah, I don't know anything about toposes but it sounds like the right language for this construction

[Bhavik Mehta]

Actually out of interest, why is Type not a grothendieck topos?

[Johan Commelin]

It is, right?

[Johan Commelin]

It's sheaves on unit

[Johan Commelin]

Maybe I didn't understand the question.

[Bhavik Mehta]

Yeah that would be my guess as well...

[Jesse Michael Han]

Type thinks it's a Grothendieck topos, but externally it isn't (it lacks Type 1-indexed colimits)

[Jesse Michael Han]

(this is yet another case of mathematicians using the same words to mean two different things)

[Johan Commelin]

Are there examples of external Grothendieck topoi, apart from singletons?

[Reid Barton]

Right, this again comes down to whether or not the "implicit universe convention" is in effect, or to how one identifies the universe-based concepts with the non-universe-based concepts.