is_prime_field

Stream: Is there code for X?

[Adam Topaz]

What is the idiomatic way to say that a field K is a prime field (i.e. isomorphic to either $\mathbb{Q}$ or $\mathbb{F}_p$ for some prime $p$)?

[Eric Rodriguez]

here's a silly one: (n : \N) [field K] [is_fraction_ring (zmod n) K].

[Eric Rodriguez]

or maybe that includes F_p^ns, never mind

[Adam Topaz]

One option could be to say that any morphism of fields $L \to K$ is an isomorphism (presumably where $L$ has the same universe level as $K$)

[Eric Rodriguez]

that feels like a far more mathlibby definition, and leave the fact that they're isomorphic to F_p/Q as a theorem

[Adam Topaz]

Alternatively one could try to somehow say that $K$ is generated as a field by the image of the canonical ring hom from $\mathbb{Z}$.

[Adam Topaz]

But I don't know if we have a good way to say that.

[Eric Rodriguez]

why do we need them to be in the same universe?

[Adam Topaz]

If we want a characteristic predicate, we want to make sure that there aren't any additional universe parameters that are not necessary. So we could take $L$ to be in Type 0 or in Type u where K : Type u.

[Adam Topaz]

The two would be equivalent because there would be an isomorphism with $\mathbb{Q}$ or $\mathbb{F}_p$ which are in Type 0.

[Adam Topaz]

But if we let L : Type v while K : Type u, then a priori there would be many predicates is_prime_field K which depend not only on u where K : Type u, but also on the v.

[Adam Topaz]

We can use docs#subfield.closure and say that the subfield generated by empty is top.

[Adam Topaz]

Or maybe just bot = top in subfield