type with two indistinguishable elements

Stream: general

[Kevin Buzzard]

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+iy$ to $x-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$, 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 $k$ equipped with a map $\mathbb{R}\to k$, such that $k$ is isomorphic to the complex numbers, but there are two isomorphisms. The polynomial $x^2+1$ has two roots in $k$; if you choose a root of this polynomial then you get an isomorphism $\mathbb{C}\to k$ sending I to this root.

But in my mental model of $k$, the two square roots are "completely indistinguishable". In the past I have constructed $k$ 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]

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]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Scott Morrison]

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]

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

[Scott Morrison]

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

[Scott Morrison]

(That is, my objection was in jest.)

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Ruben Van de Velde]

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

[Chris Hughes]

It is $i$ by definition. It's not a meaningful question.

[Chris Hughes]

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]

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]

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

[David Wärn]

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 $\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]

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

[David Wärn]

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

[David Wärn]

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

[David Wärn]

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]

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 $BG$ where G is the absolute Galois group.

[Adam Topaz]

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

[Sebastien Gouezel]

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]

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

[Kevin Buzzard]

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]

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]

This sounds much like "nominal sets"

[Mario Carneiro]

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]

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]

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]

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]

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]

Why not just use variable?

[Jack J Garzella]

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]

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 $\mathbb{Q} (\sqrt{2})$ as an abstract field with two indistinguishable real embeddings rather than a subset of $\R$ with a fixed embedding.

[Kevin Buzzard]

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

[Scott Morrison]

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

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]

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

[Kevin Buzzard]

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]

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]

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