## Stream: maths

### Topic: applicative ultrapower

#### David Wärn (Apr 30 2020 at 11:47):

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 (Apr 30 2020 at 22:50):

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 (Apr 30 2020 at 23:00):

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 (Apr 30 2020 at 23:24):

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 (Apr 30 2020 at 23:26):

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

#### Bhavik Mehta (Apr 30 2020 at 23:27):

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 (May 01 2020 at 09:31):

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 (May 01 2020 at 14:35):

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

It is, right?

#### Johan Commelin (May 01 2020 at 14:44):

It's sheaves on unit

#### Johan Commelin (May 01 2020 at 14:45):

Maybe I didn't understand the question.

#### Bhavik Mehta (May 01 2020 at 14:53):

Yeah that would be my guess as well...

#### Jesse Michael Han (May 01 2020 at 21:28):

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

#### Jesse Michael Han (May 01 2020 at 21:29):

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

#### Johan Commelin (May 02 2020 at 05:17):

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

#### Reid Barton (May 02 2020 at 11:18):

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.

Last updated: May 14 2021 at 18:28 UTC