# Zulip Chat Archive

## Stream: general

### Topic: axiom of unique choice

#### Scott Morrison (Mar 06 2018 at 17:06):

Can I define a `def unique_choice {α} {P : α → Prop} (s : subsingleton {a // P a}) (e : ∃ a, P a) : {a // P a} := sorry`

without using classical choice? Or does Lean’s type theory not allow even this?

#### Scott Morrison (Mar 06 2018 at 17:10):

(Follow-up questions, if the answer is no: 1. Am I allowed to be sad about this? 2. Should I learn about `trunc`

?)

#### Reid Barton (Mar 06 2018 at 17:26):

I also wondered about this. My understanding is that `unique_choice`

would need to be `noncomputable`

. From a classical perspective, it ought to be valid without choice, so it could be added as a separate axiom, although I'm not sure there much use in doing so.

#### Reid Barton (Mar 06 2018 at 17:27):

It's annoying when dealing with limits/colimits (maybe the same situation you are thinking about), since it means that constructively there are really two versions of each of those notions.

#### Scott Morrison (Mar 06 2018 at 17:43):

I guess the closest computable analogue of `unique_choice`

is

import data.quot def constructive_unique_choice {α} {P : α → Prop} (s : subsingleton {a // P a}) (e : trunc {a // P a}) : {a // P a} := begin apply trunc.lift id _ e, apply subsingleton.elim end

#### Scott Morrison (Mar 06 2018 at 17:46):

With the idea that `trunc {a // P a}`

is a pretty-good replacement for `∃ a, P a`

.

#### Andrew Ashworth (Mar 06 2018 at 18:14):

are you aware of anything out there that discusses `trunc`

in an accessible manner? It's not something I've had to use so far, but several people have mentioned it now

#### Andrew Ashworth (Mar 06 2018 at 18:15):

i've seen a brief mention on https://homotopytypetheory.org/2012/09/16/truncations-and-truncated-higher-inductive-types/ but is that applicable?

#### Mario Carneiro (Mar 06 2018 at 19:11):

The answer to your first question, as you have already observed, is no. You can be sad about this if you like, but it is perfectly reasonable from a computational standpoint: Remember that from the VM's point of view, `subsingleton {a // P a}`

is `unit`

and `∃ a, P a`

is `unit`

, while `{a // P a}`

is `α`

. So you are asking the VM to invent an element of `α`

from basically nothing.

#### Mario Carneiro (Mar 06 2018 at 19:15):

There are two options for constructivizing the `∃ a, P a`

assumption. One is `trunc {a // P a}`

as you have observed.

#### Mario Carneiro (Mar 06 2018 at 19:15):

@Andrew Ashworth Note that the `trunc`

of mathlib is a bit different from the HoTT `trunc`

, or rather, it has different import in a proof irrelevant setting. `trunc A`

is simply a quotient of `A`

by the always true relation. Alternatively stated, `trunc A`

is the universal subsingleton generated by `A`

. Any two elements of `trunc A`

are propositionally equal, so `trunc A`

has one element if `A`

is nonempty and no elements if `A`

is empty.

#### Mario Carneiro (Mar 06 2018 at 19:17):

But in the VM, because quotients are forgotten, `trunc A`

is `A`

, while the prop analogue `nonempty A`

is `unit`

. So `trunc A`

has computational content and can be used to construct elements from constant functions, or from functions on a subsingleton.

#### Mario Carneiro (Mar 06 2018 at 19:19):

The second option for constructivizing `∃ a, P a`

is `Σ a, P a`

, or in the unique case we can replace `∃! a, P a`

with `Σ! a, P a`

(these are rarely used and so are not defined in mathlib, but it's not hard to guess what they mean). An element of `Σ! a, P a`

is an element of `A`

and a proof that every other element of `A`

is equal to it. In HoTT this would be called `contr`

I think, since it expresses that `A`

is contractible

#### Mario Carneiro (Mar 06 2018 at 19:20):

In this case, you can "unique choose" simply by projecting out the first component

#### Mario Carneiro (Mar 06 2018 at 19:24):

By the way, the best introduction to propositional truncation in the HoTT sense is the HoTT book, and most of it applies to reasoning about `trunc`

(although you can ignore anything that talks about n-truncating for n >= 0, or anything about equality of proofs)

https://hott.github.io/book/nightly/hott-online-1132-g5052dbc.pdf#section.3.7

#### Mario Carneiro (Mar 06 2018 at 19:26):

In the description there, you should replace the term "mere proposition" with "subsingleton". If you replace it with "proposition" instead you get `nonempty`

, which is the `Prop`

truncation operation

#### Reid Barton (Mar 06 2018 at 19:35):

There's also `A ≃ unit`

in mathlib as a constructive version of being a singleton.

#### Reid Barton (Mar 06 2018 at 19:36):

I'm a little surprised by "these are rarely used and so are not defined in mathlib", since a great many constructions are characterized by a universal property and for a constructivist I'd think it would be natural to ask that the existence part of the universal property be given constructively

#### Reid Barton (Mar 06 2018 at 19:38):

(For instance, imagine if the induction principle for an inductive data type only allowed you to conclude `∃!`

function which satisfies the recursive equations.)

#### Mario Carneiro (Mar 06 2018 at 19:43):

It is almost always better to state the two parts of sigma exists separately: one to make a definition and a second to assert everything satisfying the universal property is equal to it. What is not used is the pairing itself, which would only be useful if you are doing some kind of higher order construction like quantifying over all uniquely definable objects

#### Reid Barton (Mar 06 2018 at 19:48):

Well, here is an example: how one might write down the definition of a coproduct in a category.

variable {C : Type} variable {Hom : C → C → Type} variable {comp : Π {X Y Z}, Hom Y Z → Hom X Y → Hom X Z} def coprod (a b c : C) (i : Hom a c) (j : Hom b c) := Π (z : C) (f : Hom a z) (g : Hom b z), ∃! (h : Hom c z), comp h i = f ∧ comp h j = g

#### Reid Barton (Mar 06 2018 at 19:49):

I claim this definition is "wrong", because `∃!`

needs to be `Σ!`

.

#### Reid Barton (Mar 06 2018 at 19:50):

I'm not sure how to apply your suggestion in this situation

#### Mario Carneiro (Mar 06 2018 at 19:56):

`coprod`

should be a structure, with a first component that gives the hom, and two more components for the equalities

#### Scott Morrison (Mar 06 2018 at 20:39):

Thank you, Mario, for this very helpful explanation of how to think about `trunc`

.

#### Scott Morrison (Mar 06 2018 at 20:44):

@Reid Barton, my structure for Coproduct (rather long-winded, I know) is at https://github.com/semorrison/lean-category-theory/blob/master/src/categories/universal/universal.lean#L103. I am tempted to introduce and use the `Σ!`

notation, however. The price of course is less descriptive names.

#### Scott Morrison (Mar 06 2018 at 20:46):

The reason I was thinking about unique choice was being sad that the first isomorphism theorem (e.g. for vector spaces, in mathlib already, or for groups, which Mitchell is PR’ing soon) had to be marked as noncomputable.

#### Scott Morrison (Mar 06 2018 at 20:47):

Really I would like to be able to talk about the “constructive image” of a group homomorphism. One should then be able to prove `G / ker f`

is isomorphic to the constructive image, without choice.

#### Scott Morrison (Mar 06 2018 at 20:48):

But neither `trunc`

nor sigma types help here, as we would want the constructive image to still be a set.

#### Mario Carneiro (Mar 06 2018 at 20:49):

Do you have a link to the theorem you are referring to?

#### Mario Carneiro (Mar 06 2018 at 20:50):

But yes, this is a problem with using `set`

. Writing ideals as a subcollection of `set A`

is already going mostly classical

#### Scott Morrison (Mar 06 2018 at 20:50):

@Mario Carneiro https://github.com/leanprover/mathlib/blob/master/algebra/linear_algebra/linear_map_module.lean#L92

#### Scott Morrison (Mar 06 2018 at 20:50):

I guess one could just not define the image as a set.

#### Scott Morrison (Mar 06 2018 at 20:51):

But rather look at pairs, an element h of H, and a truncated sigma type \Sigma g : G, f g = h, and just put a group structure on those directly.

#### Scott Morrison (Mar 06 2018 at 20:52):

That thing is classically isomorphic to the usual image, but you should be able to (?) give a constructive first isomorphism theorem.

#### Mario Carneiro (Mar 06 2018 at 20:53):

Note that such a type is equivalent to the quotient of the domain of f by `f a = f b`

#### Mario Carneiro (Mar 06 2018 at 20:53):

i.e. it's basically true by equivalence of the underlying types already

#### Scott Morrison (Mar 06 2018 at 20:54):

Even better :simple_smile:

#### Mario Carneiro (Mar 06 2018 at 20:54):

I think the moral of the story is: don't use the first isomorphism theorem at all, just stick to the LHS

#### Scott Morrison (Mar 06 2018 at 20:56):

Or paraphrasing: if you want to do constructive group theory, _define_ the image of a morphism as the quotient of the domain by the kernel, and have this theorem be a tautology. :simple_smile:

#### Kevin Buzzard (Mar 06 2018 at 21:45):

It's this sort of talk that gives constructivism a bad name amongst mathematicians!

#### Patrick Massot (Mar 06 2018 at 21:53):

I couldn't agree more

#### Patrick Massot (Mar 06 2018 at 21:54):

I can only hope no such consideration will trigger design decision making it harder to do group theory with Lean

#### Mario Carneiro (Mar 06 2018 at 21:56):

why do you say that? It seems that the constructive interpretation reveals a deeper equivalence, that does not have anything to do with groups but extends to all the "first isomorphism theorems"

#### Patrick Massot (Mar 06 2018 at 21:58):

Errrr... Are your referring to "if you want to do constructive group theory, _define_ the image of a morphism as the quotient of the domain by the kernel, and have this theorem be a tautology."?

#### Mario Carneiro (Mar 06 2018 at 21:59):

that's the practical upshot of this observation

#### Kevin Buzzard (Mar 06 2018 at 22:01):

because what you're defining there is the co-image

#### Kevin Buzzard (Mar 06 2018 at 22:01):

we already have a name for it

#### Kevin Buzzard (Mar 06 2018 at 22:01):

and it's not the image

#### Kevin Buzzard (Mar 06 2018 at 22:02):

although it's often canonically isomorphic to it

#### Mario Carneiro (Mar 06 2018 at 22:03):

okay, then the import of the observation is "coimage is image but better"

#### Scott Morrison (Mar 06 2018 at 23:19):

Once Mitchell has finished with his PR, I may try to refactor his proof of the first isomorphism theorem into two pieces:

1. The (constructive) isomorphism between `G / ker f`

and `\Sigma h : H, trunc (\Sigma g : G, f g = h)`

(what I was calling the “constructive image” above)

2. The (noncomputable) isomorphism between the constructive image and the usual image `{h | \Exists g : G, f g = h}`

.

#### Scott Morrison (Mar 06 2018 at 23:20):

I’m curious if @Patrick Massot and @Kevin Buzzard would still disapprove of this. :simple_smile: The point is that the first isomorphism is very often all you need, because however you proved that `h \elem image f`

was probably (because it was probably constructive) enough to produce a point in the constructive image too, and then you can do calculations.

#### Scott Morrison (Mar 06 2018 at 23:22):

(And it’s not entirely good enough to say: “but we have Sage for calculations!” because group theory specific tactics will eventually want to do calculations internally...)

#### Scott Morrison (Mar 06 2018 at 23:23):

Alternatively, @Mitchell Rowett may like to do this himself, except that I probably should resist the temptation to suggest this to him, as he has to finish his assignment for my class, and all his other classes. :simple_smile:

#### Johannes Hölzl (Mar 07 2018 at 08:40):

@Scott Morrison the first and the second isomorphism laws are already in mathlib. You find them in `algebra/linear_algebra/prod_module.lean`

.

#### Kevin Buzzard (Mar 07 2018 at 08:49):

I cannot really comment on these issues because in my world you can't get anywhere constructively so I never worry.

#### Scott Morrison (Mar 07 2018 at 15:32):

@Johannes Hölzl, I was talking about the isomorphism theorems for groups, not vector spaces. (Sorry if I wasn’t clear — one of the undergrads here has been doing some basic group theory.) There are going to be a lot of these! (Every category where images and coimages agree.)

#### Johannes Hölzl (Mar 08 2018 at 07:59):

The first and second isormorphisms theorem is about modules. So when you see groups as Z-modules then you already got the group isomorphism laws. Or are the group isomorphism laws different statements?

#### Mario Carneiro (Mar 08 2018 at 08:04):

An abelian group is a Z-module, but general groups can't be expressed as a special case of modules AFAIK

#### Johannes Hölzl (Mar 08 2018 at 08:09):

Ah, now I see the difference. Thanks!

#### Kevin Buzzard (Mar 08 2018 at 08:35):

I think that even if you allow non-commutative rings, you can't model groups as modules, because a module is an abelian group by definition.

#### Mario Carneiro (Mar 08 2018 at 08:36):

In fact, even if you drop the abelian requirement, you can prove commutativity by expanding `(1+1)(x+y)`

in two ways

#### Kevin Buzzard (Mar 08 2018 at 08:39):

Ha ha, you have to be careful doing that sort of thing. When Kenny and I were on the home straight for schemes yesterday we had to define the zero element of a complicated type which we wanted to be a ring, and after the dust settled we had to check that a ring homomorphism sent 0 to 0. But Kenny had defined a ring homomorphism without putting this in as an axiom as he'd observed it followed from f(x+y)=f(x)+f(y) so we had to stop what we were doing and prove that this implied f(0)=0 :-)

#### Mario Carneiro (Mar 08 2018 at 08:42):

...that's a good thing, though

#### Kevin Buzzard (Mar 08 2018 at 09:01):

Talking of which, what should happen to the observation that the current definition of a basis of a topological space in mathlib asks for more than is necessary? Kenny and I defined `is_basis'`

and proved `basis iff basis'`

. It was much easier to prove that something was a `basis'`

and indeed when we prove affine schemes are schemes we will be working with a `basis'`

of the topology for Spec(R). Is this a satisfactory state of affairs? Because we proved basis iff basis' we don't need anything to change, I just thought it was a bit weird.

#### Mario Carneiro (Mar 08 2018 at 09:13):

Could you be more specific? What's the new definition?

#### Mario Carneiro (Mar 08 2018 at 09:16):

Hm, I think I know what you did. To me the last condition in `is_topological_basis`

feels a bit artificial; I would prefer that the definition not make any reference to a topological space, in which case the first two conditions are what you want. But it's true that if you know that a collection of sets is the generating set for a topology, then there are easier ways to say the same thing

#### Mario Carneiro (Mar 08 2018 at 09:17):

Probably `is_topological_basis_of_open_of_nhds`

is the characterization you would like?

#### Kevin Buzzard (Mar 08 2018 at 09:35):

We had a conversation a couple of weeks ago where I said "I was trying to prove something was a basis and I looked at the definition in mathlib, which Johannes had taken from a maths book, and it stank; I didn't want to prove two of the axioms because they followed from the rest". You replied "oh yeah, I just proved that basis -> something else without using these two axioms." And then Kenny proved that my definition of basis was equivalent to mathlibs. My definition (i.e. the standard one, as far as I am concerned) is much easier to work with. The question is whether you are interested in a PR which changes the definition of a basis in mathlib. I can be more specific over the weekend when I've got over my current deadlines. I'll look at the function you mention later, I've got to run :-/ I have starred your message :-)

#### Johannes Hölzl (Mar 08 2018 at 09:38):

The definition of `is_topological_basis_of_open_of_nhds`

changed in https://github.com/leanprover/mathlib/commit/e2a562a8df52c2b0fffad361605fcbc03cb99b4b . I'm happy if there are further simplifications. But I don't yet know what you want to change

#### Mario Carneiro (Mar 08 2018 at 09:46):

Maybe this will help to clarify my intent here. To me, a topological basis is a property of a set of sets, which does not depend on a prior notion of what a topology is. It is a necessary and sufficient condition so that the collection of unions of basis elements forms a topology. However, given a topological basis, there is of course a natural associated topology, and given a topology, one can express the property of being a basis that generates that topology, and this is what `is_topological_basis_of_open_of_nhds`

is for.

#### Mario Carneiro (Mar 08 2018 at 09:49):

So if your definition of topological basis starts "a basis is a collection of open sets" then it's missing the point, which is to classify what a basis is in the abstract, independently of the topology.

#### Johannes Hölzl (Mar 08 2018 at 09:54):

I agree! Interestingly, the mathlib definition of basis did not change, but the theorem got simpler.

#### Kevin Buzzard (Mar 08 2018 at 10:47):

I will get back to you on all this later (Saturday?). I really like this starring in Zulip; it really helps my workflow.

Last updated: May 15 2021 at 22:14 UTC