uses of choice

Stream: general

[Floris van Doorn]

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]

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]

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]

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]

@Floris van Doorn

[Floris van Doorn]

nice!

[Bryan Gin-ge Chen]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

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

[Johan Commelin]

So there might not be a problem after all?

[Johan Commelin]

Can we do algebraic closures with HoTT's AoC?

[Johan Commelin]

And Zorn, and all the other things?

[Mario Carneiro]

Zorn's lemma proves there exists a maximal element

[Mario Carneiro]

and there exists an algebraic closure

[Mario Carneiro]

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

[Johan Commelin]

Aah, you forgot to typeset that as exists

[Johan Commelin]

Are constructions important for these things?

[Mario Carneiro]

it is for various conveniences

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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]

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

[Johan Commelin]

And harder to use

[Mario Carneiro]

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]

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

[Johan Commelin]

I see

[Johan Commelin]

But we can prove that such a function exists.

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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 $\mathbb{Q}$ or "the" maximal extension of $\mathbb{Q}$ unramified outside a finite set of primes $S$ -- 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]

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]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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]

This sounds really cool!