Zulip Chat Archive

Stream: general

Topic: uses of choice


Floris van Doorn (Oct 07 2018 at 19:24):

Inspired by my post in the thread "what is wrong with HoTT" I had two questions:

(1) What are some uses of classical.choice in mathlib. I'm not interested in uses of LEM or the axiom of choice, but in the strong form of choice which is inconsistent with HoTT. Are the applications of them avoidable if some things were designed a little differently?

(2) Can you define something of the following type without using choice?
Π(A : ℕ → Type) (f : Πn, A n → A (n+1)) (n m : ℕ) : n ≤ m → A n → A m
It is easy to do if lives in Type, by induction on (as an inductive family), but it is less obvious when lives in Prop, since then it doesn't eliminate into Type.

Johan Commelin (Oct 07 2018 at 19:26):

Re (1): Would you please recall the difference between AoC and "strong form of choice". Mere mathematicians don't exactly know the difference...

Floris van Doorn (Oct 07 2018 at 19:40):

classical.choice states nonempty A -> A (it allows you to construct "data" out of a proposition). The axiom of choice states for every surjective function there exists a section (which is still a proposition).

Kenny Lau (Oct 07 2018 at 19:41):

example (A :   Type) (f : Πn, A n  A (n+1)) (n m : ) : n  m  A n  A m :=
nat.rec_on m
  (λ n H An, @eq.rec_on _ _ A _ (nat.eq_zero_of_le_zero H) An)
  (λ m ih n H An, if h : n  m then f m (ih n h An)
    else eq.rec_on (le_antisymm H (lt_of_not_ge h)) An) n

Kenny Lau (Oct 07 2018 at 19:42):

@Floris van Doorn

Floris van Doorn (Oct 07 2018 at 19:45):

nice!

Bryan Gin-ge Chen (Oct 07 2018 at 20:34):

Regarding (1), this recent thread is distantly related (at least we talk about using choice in the context of defining the dimension of a vector space.)

Mario Carneiro (Oct 08 2018 at 00:28):

@Floris van Doorn One interesting use of choice is in filter.lim, which constructs the limit of a filter

Mario Carneiro (Oct 08 2018 at 00:29):

It's a unique choice only if we assume the topology is T2 (and it is a topology)

Mario Carneiro (Oct 08 2018 at 00:31):

There are also things like quotient.out (pick an element from an equivalence class), which are fully nonconstructive. You might be able to encapsulate this in a proof method for subsingletons, though

Johan Commelin (Oct 08 2018 at 08:14):

@Floris van Doorn I think this might be a deal-breaker. I would like to explore it further.

Johan Commelin (Oct 08 2018 at 08:14):

I don't even know what "eliminating into Prop" or "into Type" means.

Johan Commelin (Oct 08 2018 at 08:14):

But my gut feeling says that we need to be able to choose data.

Kevin Buzzard (Oct 08 2018 at 08:19):

I don't even know what "eliminating into Prop" or "into Type" means.

I think it means that if you do cases on A or B then stuff breaks if your goal is data, because or "only eliminates into Prop", i.e. or.rec is protected eliminator or.rec : ∀ {a b C : Prop}, (a → C) → (b → C) → a ∨ b → C

Mario Carneiro (Oct 08 2018 at 08:19):

The idea is that you can construct choicy things but at the end of the day it has to be in service of proving an exists

Kevin Buzzard (Oct 08 2018 at 08:19):

Note that the "motive" C has to be a Prop.

Mario Carneiro (Oct 08 2018 at 08:20):

incidentally, this is the way things are in metamath - with ZFC the axiom of choice ends in an exists

Johan Commelin (Oct 08 2018 at 08:20):

So there might not be a problem after all?

Johan Commelin (Oct 08 2018 at 08:21):

Can we do algebraic closures with HoTT's AoC?

Johan Commelin (Oct 08 2018 at 08:21):

And Zorn, and all the other things?

Mario Carneiro (Oct 08 2018 at 08:21):

Zorn's lemma proves there exists a maximal element

Mario Carneiro (Oct 08 2018 at 08:21):

and there exists an algebraic closure

Mario Carneiro (Oct 08 2018 at 08:22):

but unless you can turn these into unique exists this isn't actually a construction

Johan Commelin (Oct 08 2018 at 08:22):

Aah, you forgot to typeset that as exists

Johan Commelin (Oct 08 2018 at 08:22):

Are constructions important for these things?

Mario Carneiro (Oct 08 2018 at 08:22):

it is for various conveniences

Mario Carneiro (Oct 08 2018 at 08:23):

i.e. it is messy to talk about "a complete ordered field" every time you just want R

Mario Carneiro (Oct 08 2018 at 08:23):

it makes all your theorems longer and gives you more things to juggle

Johan Commelin (Oct 08 2018 at 08:23):

Ok... I don't understand enough of this.

Mario Carneiro (Oct 08 2018 at 08:24):

But for example if all you have is a proof that there exists an alg closure, then you just have a relatively long lived hypothesis saying E is an algebraic closure of F

Johan Commelin (Oct 08 2018 at 08:24):

@Mario Carneiro Do you think it means that algebraic closures are harder to do in HoTT than in DTT?

Johan Commelin (Oct 08 2018 at 08:25):

And harder to use

Mario Carneiro (Oct 08 2018 at 08:25):

and then when you get to the end of whatever you needed them for you use the exists assumption to discharge the hypothesis

Mario Carneiro (Oct 08 2018 at 08:26):

it means there is no function alg_closure : field -> field

Johan Commelin (Oct 08 2018 at 08:26):

I see

Johan Commelin (Oct 08 2018 at 08:26):

But we can prove that such a function exists.

Mario Carneiro (Oct 08 2018 at 08:26):

but there is a kind of yoneda version (closure -> p) -> (field -> p) (where p : Prop)

Kevin Buzzard (Oct 08 2018 at 08:29):

But we can prove that such a function exists.

I think in number theory it's very easy to forget that you have to make a big choice here.

Kevin Buzzard (Oct 08 2018 at 08:33):

This is one of those issues where a whole bunch of stuff (Frobenius elements, traces of Galois representations etc etc) is all built with an implicit understanding that nobody will ever say anything which will depend on the choice of algebraic closure. Some people probably don't check this or even understand it. But you follow what other people do and it works. Any statement you make about "the" absolute Galois group of Q\mathbb{Q} or "the" maximal extension of Q\mathbb{Q} unramified outside a finite set of primes SS -- all these sentences should have an inbuilt resiliance to changing your choice. The moment you make such a choice you are in some sense running the risk that someone else might need your constructions or theorems but with a different choice, and then you need this transfer tactic to make sure that you can move from your choice to theirs.

Mario Carneiro (Oct 08 2018 at 08:35):

Now ZF (even without the C) has unique choice, so you can actually do constructions if you can prove the choice doesn't matter

Mario Carneiro (Oct 08 2018 at 08:36):

but mathematicians actually take this one step further, by conflating unique with unique up to isomorphism

Johan Commelin (Oct 08 2018 at 08:36):

Well, we are ok with "unique up to contractible choice"

Mario Carneiro (Oct 08 2018 at 08:37):

I am pretty sure that lots of field extension arguments are not unique in the strict sense required by ZFC or DTT

Mario Carneiro (Oct 08 2018 at 08:38):

Interestingly HoTT has exactly the right combination of univalence + unique choice to make this work

Mario Carneiro (Oct 08 2018 at 08:40):

actually, maybe not... it depends on how the isomorphisms are presented. If you just prove there exists an isomorphism even HoTT won't swallow it

Kevin Buzzard (Oct 08 2018 at 08:41):

The choice of algebraic closure is unique up to hugely non-unique isomorphism and this exactly the problem. It makes talking about elements of absolute Galois groups almost meaningless. Even if you choose a different algebraic closure to me and instantly fix an isomorphism of yours with mine, I might find that I want to fix a different isomorphism of mine with yours, so our dictionaries from moving between the two isomorphic absolute Galois groups are different -- they differ by an inner automorphism. This is why Langlands' philosophy is so successful -- it pushed the idea of looking at representations of Galois groups rather than understanding the structure of the groups themselves. Representations are not changed (up to isomorphism) by an inner automorphism of the group.

Mario Carneiro (Oct 08 2018 at 08:42):

right, it's only stuff that is invariant under inner automorphism that would be HoTT constructible

Mario Carneiro (Oct 08 2018 at 08:44):

ZFC might still have trouble turning this into a construction, unless you can get the carrier to sit still

Mario Carneiro (Oct 08 2018 at 08:45):

and lean will of course use its global choice function to construct anything you like with no assumptions

Kevin Buzzard (Oct 08 2018 at 08:54):

and lean will of course use its global choice function to construct anything you like with no assumptions

Right -- but then you need the transport de structure tactic to ensure that people can apply the theorem.

Floris van Doorn (Oct 08 2018 at 16:48):

These are interesting comments. My experience in undergraduate math courses is that mathematicians are careful with things like non-unique limits in a topological space which is not T2. But maybe that just in undergraduate math courses :)
For something like algebraic closures, I think mathematicians will be careless, since the algebraic closure is unique, even though the isomorphism between two instances is non-unique. This means that in HoTT you indeed cannot write a function algebraic_closure : field -> field.

What's interesting, is that we can express this situation very nicely in HoTT. In HoTT, the type field is considered as the groupoid of fields and isomorphisms. If we just knew that for every field there exists an algebraic closure, we can write that as a function: field -> ∥ field ∥_{-1}, where ∥ X ∥_{-1} is called the propositional truncation of X, which is the HoTT-analogue of nonempty (turning a type into a prop by making all elements equal). However, we can express the fact "for every field there exists an algebraic closure unique up to non-unique isomorphism" as a function field -> ∥ field ∥_{0}. Here ∥ X ∥_{0} is the set of connected components of X, turning a type into a set by making all proof of equality in X equal. This means that in HoTT, as long as you are constructing an element in a set (or proposition), you may assume that a given field has a chosen algebraic closure.

Johan Commelin (Oct 08 2018 at 16:50):

This sounds really cool!


Last updated: Dec 20 2023 at 11:08 UTC