[isabelle-dev] NEWS: avoid the Complex constructor, use the more natural Re/Im view

[Manuel Eberl]

Hallo,

I stumbled across this just now and thought about it for a bit. I don't
know much about category theory, but I would say the intuitive “reason”
why complex numbers can be represented this way is the following:

1. ℂ is a field extension of ℝ with degree 2 (since it is constructed
from the ℝ-irreducible polynomial X² + 1, which has degree 2)
2. Therefore, ℂ is a 2-dimensional ℝ-vector space (by some basic results
from algebra) and {1, i} is a basis of it

This already means that given functions f₁, f₂ : ℝ → ℝ, one can extend
them to a function f: ℂ → ℂ such that
f(a + bi) = f1(a) + f2(b)i, and that two complex numbers are equal iff
their real and imaginary parts are equal. This is the handwaving-free
justification for what you described as “it is possible to define
functions on complex by specifying the observation of Re/Im.”.

The remaining steps are now:

3. An n-dimensional K-vector space is isomorphic to the canonical
n-dimensional K-vector space K^n, so ℂ is isomorphic to ℝ×ℝ
4. The binary product type can be expressed as a codatatype.

In fact, in some way, the “simplest nontrivial codatatype”, similarly to
how the binary sum type is the “simplest nontrivial codatatype”.
Categorically speaking, the two are the right and left adjoints of the
diagonal functor (which is one of the “simplest” functors), and
codatatypes / datatypes in general are the right / left adjoints of some
supported sets of functors. (That is my understanding so far – my
knowledge on this subject is a bit fuzzy, so I might have misunderstood
something)

Product types themselves can be defined as codatatypes very easily.
Compare the definition of a custom product type to that of the “complex”
type:

codatatype ('a, 'b) prod = Prod (fst: 'a) (snd: 'b)
codatatype complex = Complex (Re: real) (Im: real)

The latter is basically a “special case” of the former. As I see it,
considering that the original definition of complex was

datatype complex = Complex real real

which is also isomorphic to real × real, the change from the old
definition to the new one was mostly a bureaucratic one, it didn't
really do much categorically – it only exploited some obvious
isomorphisms; the nice benefit is, of course, the ability to use
primcorec instead of primrec, which makes definitions a bit more
“direct”, since, as explained above, complex numbers are a “natural”
product type and product types are “natural” codatatypes, so defining
them as datatypes makes everything a bit more clumsy.

Cheers,
Manuel Eberl


On 07.05.2014 16:50, Makarius wrote:
> On Wed, 7 May 2014, Johannes Hölzl wrote:
>
>> * Theorems about complex numbers are now stated only using Re and Im,
>> the Complex
>> constructor is not used anymore. It is possible to use primcorec to
>> defined the
>> behaviour of a complex-valued function.
>>
>> This is also a surprising application of primcorec!
>
> That is indeed very nice. Is that a new invention or an old trick that
> every category theorist knows?
>
> In mathematics books / lectures there is usually some handwaving only,
> to justify why it is possible to define functions on complex by
> specifying the observation of Re/Im.
>
>
> Makarius
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev