Zulip Chat Archive

Stream: general

Topic: type with two indistinguishable elements


Kevin Buzzard (Jul 18 2020 at 09:21):

I am currently derailing the "Hahn-Banach" topic thread on differential geometry by talking about a field (in the maths sense) which is isomorphic to the complex numbers but not canonically. I've realised that in some sense I don't know how to formalise such an object and I think it boils down to a purely type-theoretic question which I can ask here.

First the maths background. The real numbers turn out to be completely characterised by a list of axioms: they are the unique complete totally ordered archimedean field, up to unique isomorphism. The complex numbers however has this non-identity automorphism, namely complex conjugation, sending x+iyx+iy to xiyx-iy. This automorphism commutes with all the algebraic structure (one, mul etc) and all the topological structure too. The complex numbers have two square roots of 1-1, namely (using Lean's terminology) I and -I. These square roots "have names".

I sometimes work with an "abstract" algebraic closure of the real numbers however. This is a field kk equipped with a map Rk\mathbb{R}\to k, such that kk is isomorphic to the complex numbers, but there are two isomorphisms. The polynomial x2+1x^2+1 has two roots in kk; if you choose a root of this polynomial then you get an isomorphism Ck\mathbb{C}\to k sending I to this root.

But in my mental model of kk, the two square roots are "completely indistinguishable". In the past I have constructed kk in the following way. Take a diagram category with two un-named objects and one isomorphism between these objects. Now take a functor from this category into the category of fields, sending both unnamed objects to the complexes, and sending the isomorphism to complex conjugation. Now take the (or a) limit of this diagram. It's a field, isomorphic to both of the copies of the complexes, but "with no preferred isomorphism". Except that when I mentioned this to Scott, he pointed out that when making the diagram category you probably named the two objects, so you can just choose the object whose name is the first in the alphabet and hence get a "lexicographically first" isomorphism, and argue that it is "preferred".

Is there any way of making the object I want? This has nothing to do with the complex numbers. I am asking for a type which has two terms, and whilst the terms are definitely distinct, it is "impossible" to choose one? I'm sorry that this is such a vague question. I am not even sure what I entirely mean here. I am just looking for a way of formalising my mental model -- I literally want to make it impossible to "choose a term of type X" without assuming some form of choice principle -- I want them to be as anonymous as possible. Can anyone make sense of what I'm saying?

Dima Pasechnik (Jul 18 2020 at 09:58):

Aren't you constructing your field by taking C[x]/(x^2+1)C[x] ?

Where is the choice of what is i, and what is -i, entering the picture there (as long as you are not fixing the embedding of your field into a copy of C) ?

Is Scott's objection merely staying that an order can be assumed?

Patrick Massot (Jul 18 2020 at 10:01):

When writing C[X]/(X2+1)\mathbb{C}[X]/(X^2+1), there is definitely a preferred root of X2+1X^2+1, the image of XX in the quotient.

Patrick Massot (Jul 18 2020 at 10:02):

And I think Kevin is asking a question in psychology that has neither math content nor type theory content.

Patrick Massot (Jul 18 2020 at 10:03):

There are certainly variations on this question that make sense, talking about stuff commuting with automorphisms or functorial constructions.

Scott Morrison (Jul 18 2020 at 10:03):

I think Patrick is right here -- we're entering philosophical territory about the possibility of forgetting something you once knew. (Easy to demonstrate in practice, of course!)

Scott Morrison (Jul 18 2020 at 10:04):

I think you shouldn't be upset at all by my objection.

Scott Morrison (Jul 18 2020 at 10:04):

It's just fine to forget the identity of the two objects that you used as crutches in building the limit diagram.

Scott Morrison (Jul 18 2020 at 10:05):

(That is, my objection was in jest.)

Kevin Buzzard (Jul 18 2020 at 10:52):

Oh OK -- I'm happy to accept that my question is psychological. It's definitely how my mental model works though.

Kevin Buzzard (Jul 18 2020 at 10:53):

(Patrick and Dima -- your C's should be R's but I know what you mean)

Ruben Van de Velde (Jul 18 2020 at 11:05):

Is there even a way to tell that the I in mathlib is ii rather than i-i?

Chris Hughes (Jul 18 2020 at 11:06):

It is ii by definition. It's not a meaningful question.

Chris Hughes (Jul 18 2020 at 11:09):

What is the purpose of forgetting which root is preferred? Is it more or less a psychological trick to make sure that my definitions are about rings or whatever, and not rings with a constant so I can transfer proofs of them across ring isomorphisms and not just ring isomorphisms that the preserve the constant. This is more or less it, right? But that's not really necessary in a theorem prover since it's impossible to make mistakes anyway.

Kevin Buzzard (Jul 18 2020 at 11:18):

One time when I used it was when I made a conceptual definition in the Langlands program, by choosing an isomorphism of R-bar with C, and then I checked that my definition was independent of the choice, which gave me evidence that the definition was the one I was looking for.

Adam Topaz (Jul 18 2020 at 12:16):

What about the type of all degree 2 extensions of R?

David Wärn (Jul 18 2020 at 12:57):

Adam Topaz said:

What about the type of all degree 2 extensions of R?

As far as I understand, this is the type of the object Kevin is asking for. The question is how to construct a generic term of this type. I'm not so sure this is the right question -- I think instead you want to prove things for arbitrary terms of the type. But if you want a generic term, you can take the one given by classical.choice -- it has no preferred isomorphism with C\mathbb C.

FWIW, this type is (morally) equivalent to "the type of two-element types" -- map a field to the type of square roots of -1. So the question could be stated more elementarily as "how to construct a generic two-element type".

Sebastian Reichelt (Jul 18 2020 at 13:19):

Not sure if this is a good solution, but: If you state and prove, as a Prop, that R\R has an algebraic closure, then use classical.some to obtain one such closure, I believe the two roots of 1-1 will be indistinguishable.

David Wärn (Jul 18 2020 at 13:30):

Yes, I believe this works -- this is what I meant by "take the one given by classical.choice"

David Wärn (Jul 18 2020 at 13:30):

Aren't Lean 4 constants meant to also do something like this?

David Wärn (Jul 18 2020 at 13:34):

Probably this is only useful if you can internalise some metatheorems like "any subset of R-bar which can be defined without using choice is stable under conjugation"

Adam Topaz (Jul 18 2020 at 14:13):

This is just about Galois theory. The category of algebraic closures of R has many objects, but it's equivalent to a category with a single object whose automorphism group is Z/2. But this is just an equivalence of categories. I guess from the point of view of HoTT, the type of algebraic closures of a field is homotopy equivalent to BGBG where G is the absolute Galois group.

Adam Topaz (Jul 18 2020 at 14:14):

But of course the homotopy point of view doesn't mean anything in lean

Sebastien Gouezel (Jul 18 2020 at 14:40):

In Lean, there will always be a distinguished root of -1, the one that is given by the choice function applied to the predicate "there exists x such that x ^ 2 = -1"!

Adam Topaz (Jul 18 2020 at 14:45):

Agreed, but I think this is an instance where it is natural to think of that predicate having two distinct proofs :)

Kevin Buzzard (Jul 18 2020 at 16:20):

Sebastien Gouezel said:

In Lean, there will always be a distinguished root of -1, the one that is given by the choice function applied to the predicate "there exists x such that x ^ 2 = -1"!

OK I give in :-) What I want can't be done in Lean.

Mario Carneiro (Jul 18 2020 at 17:13):

It can certainly be done in type theory, you just need a few axioms to allow the construction of types with stated isomorphisms

Mario Carneiro (Jul 18 2020 at 17:13):

This sounds much like "nominal sets"

Mario Carneiro (Jul 18 2020 at 17:14):

It might not be possible in lean without choice (it's obviously not possible in lean with choice), but I feel like you can do something with quotient types here

Kevin Buzzard (Jul 18 2020 at 17:16):

I want a proof that the type has two terms but I want it to be very hard to create a term of that type without using choice

Mario Carneiro (Jul 18 2020 at 17:17):

hm, when you put it that way it does sound rather unlikely; in lean without choice there aren't many ways to prove the existence of terms that doesn't produce an actual term

Mario Carneiro (Jul 18 2020 at 17:24):

To reiterate, though, the easy solution is to say

constant T : Type
axiom T_not_subsing : \exists a b : T, a != b

You might argue that I cheated by adding a new axiom, but this is exactly as respectable as the construction of quotient types (which is also a family of axioms), and it's obviously consistent. It just needs to be cleaned up a bit to give it an air of respectability as an axiom

Sebastian Reichelt (Jul 18 2020 at 18:26):

Maybe I'm missing the point, but doesn't this yield a generic two-element type?

import set_theory.cardinal

lemma two_element_type_exists:  α : Type, cardinal.mk α = 2 := begin
  use bool,
  simp
end

def two_element_type := classical.some two_element_type_exists

Reid Barton (Jul 18 2020 at 18:35):

Why not just use variable?

Jack J Garzella (Jul 18 2020 at 19:19):

At risk of making a philosophical statement, what's wrong with "pretending that lexicographical order doesn't exist"? At a low enough, all computer memory is ordered bits and bytes, so there is always some implicit order, even when we write an "unordered set" or "hash table" data structure, for example. Writing such a structure is (more or less) shielding the user from knowledge of the implicit order. So why not just use the same ordered type with two elements, but pinky-promise not to ever use the first lexicographical element? Or even better, write a layer of abstraction that prevents the user from doing this?

Jack J Garzella (Jul 18 2020 at 19:21):

In addition, I'd like to point that this question isn't as esoteric as it first looks: there are many reasons why one might want to think of a number field like Q(2)\mathbb{Q} (\sqrt{2}) as an abstract field with two indistinguishable real embeddings rather than a subset of R\R with a fixed embedding.

Kevin Buzzard (Jul 18 2020 at 20:11):

Yes this is all coming from infinite places of number fields and local-global compatibility in the Langlands program.

Scott Morrison (Jul 19 2020 at 01:42):

@Sebastian Reichelt, this is an embarrassing demonstration of how I don't know how to work with the cardinal API, but this sort of trick is no obstacle to the power of classical.some:

import set_theory.cardinal
import tactic.fin_cases

open cardinal

lemma two_element_type_exists:  α : Type, mk α = 2 := begin
  use bool,
  simp
end

def two_element_type := classical.some two_element_type_exists

lemma A : mk two_element_type = 2 := classical.some_spec two_element_type_exists

noncomputable def B : two_element_type :=
begin
  have nz : mk two_element_type  0 :=
  begin
    rw A,
    apply ne_of_gt,
    transitivity (1 : cardinal),
    { apply not_le.1,
      intro h,
      have : (1 : cardinal) = mk (fin 1) := by { rw mk_fin, simp, },
      conv at h { to_rhs, rw this },
      rw two_le_iff at h,
      rcases h with x,y,h,
      fin_cases x, fin_cases y, simpa using h, },
    { exact zero_lt_one, }
  end,
  have ne := ne_zero_iff_nonempty.1 nz,
  apply @classical.some _ (λ x, true),
  cases ne with x,
  exact x, trivial,
end

David Wärn (Jul 19 2020 at 07:28):

Surely this informal notion of "choice-free construction on R-bar" translates to "hygienic construction on an arbitrary alg closure of R", where hygienic means "functorial in isomorphisms", and arbitrary means "takes any alg closure as input" (i.e. use variable instead of axiom)

What classical.some shows is that hygiene is non-vacuous in Lean -- it is possible to write down non-hygienic constructions

Scott Morrison (Jul 19 2020 at 07:40):

You should checkout my iso_transport branch, which is a total mess, but tries formalise hygienic and provide some associated tactics.

Kevin Buzzard (Jul 19 2020 at 09:32):

The problem with algebraic closures is that they are not functorial! They are unique up to non-unique isomorphism. If K->L is a morphism of fields then you don't get a natural Kbar->Lbar. Pedantic mathematicians write "Let Kbar be an algebraic closure of K". It is exactly like turning a nonempty space into a pointed space. You can choose a point in each space, but then don't expect all morphisms of spaces to turn into morphisms of pointed spaces.

David Wärn (Jul 19 2020 at 11:17):

That's what makes this interesting :-)
The category (indeed groupoid) of algebraic closures of R is non-trivial -- we are interested in functors from it

Sebastian Reichelt (Jul 19 2020 at 12:17):

@Scott Morrison I had no doubt that you could pick an arbitrary element of two_element_type using classical.some. But Kevin Buzzard said:

I literally want to make it impossible to "choose a term of type X" without assuming some form of choice principle.

I would argue that everything that can be constructed from or proved about two_element_type must follow from the fact that it has two elements, i.e. nothing else is "known" about that type.


Last updated: Dec 20 2023 at 11:08 UTC