axiom of unique choice

Stream: general

[Scott Morrison]

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]

(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]

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]

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]

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]

With the idea that trunc {a // P a} is a pretty-good replacement for ∃ a, P a.

[Andrew Ashworth]

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]

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]

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]

There are two options for constructivizing the ∃ a, P a assumption. One is trunc {a // P a} as you have observed.

[Mario Carneiro]

@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]

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]

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]

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

[Mario Carneiro]

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]

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]

There's also A ≃ unit in mathlib as a constructive version of being a singleton.

[Reid Barton]

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]

(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]

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]

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]

I claim this definition is "wrong", because ∃! needs to be Σ!.

[Reid Barton]

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

[Mario Carneiro]

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

[Scott Morrison]

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

[Scott Morrison]

@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]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

But yes, this is a problem with using set. Writing ideals as a subcollection of set A is already going mostly classical

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Scott Morrison]

Even better :simple_smile:

[Mario Carneiro]

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

[Scott Morrison]

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]

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

[Patrick Massot]

I couldn't agree more

[Patrick Massot]

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

[Mario Carneiro]

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]

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]

that's the practical upshot of this observation

[Kevin Buzzard]

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

[Kevin Buzzard]

we already have a name for it

[Kevin Buzzard]

and it's not the image

[Kevin Buzzard]

although it's often canonically isomorphic to it

[Mario Carneiro]

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

[Scott Morrison]

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]

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]

(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]

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]

@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]

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

[Scott Morrison]

@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]

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]

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

[Johannes Hölzl]

Ah, now I see the difference. Thanks!

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

...that's a good thing, though

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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]

Probably is_topological_basis_of_open_of_nhds is the characterization you would like?

[Kevin Buzzard]

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]

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]

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]

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]

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

[Kevin Buzzard]

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