# Zulip Chat Archive

## 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?

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

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