Predicate and type versions of theorems

Stream: general

[metakuntyyy]

Sometimes there exist different structures for similar things, like for primitive roots we have
https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.html#IsPrimitiveRoot
and
https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.html#primitiveRoots.

Here all, or most of the theorems assume IsPrimitiveRoot as hypothesis.

Roots of unity is opposite, https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/RootsOfUnity/Basic.html#rootsOfUnity
There are no definitions of IsRootOfUnity for example.

Another example would be IsAlgClosure and AlgebraicClosure.

I've read somewhere that theorems should preferably written to use the former (i.e. IsPrimitiveRoot) instead of the latter (i.e. primitiveRoots) for more generality, but unfortunately I can't find it anymore.

What are the benefits and drawbacks of either approach?

[Ruben Van de Velde]

For the last one I can give an example: \C is the algebraic closure of \R, but it is not AlgebraicClosure \R - it is defined as the pair of a real and an imaginary part, and these are different types. So if you stated your theorems about AlgebraicClosure, you couldn't apply them to \C and \R

[metakuntyyy]

Ah I see, so this is basically a construction argument, we could have defined $\mathbb{C}$ to be the algebraic closure of $\mathbb{R}$, but then we would have the trouble of having to use the construction. We would not get the imaginary part. Instead we define $\mathbb{C}$ differently and prove separately that it is an algebraic closure.

I think I understand that, there is a benefit of using IsAlgClosed, but is there a benefit of using AlgebraicClosure directly. And similar with other theorems.

Well is the following correct. There is one AlgebraicClosure in lean, per construction, but there could be many IsAlgClosed, which are all pairwise isomorphic. Two instances for $\mathbb{R}$ could both be $\mathbb{C}$ and AlgebraicClosure $\mathbb{R}$

[Ruben Van de Velde]

Yes, that's correct. (At least I assume they're isomorphic - otherwise we wouldn't talk about the algebraic closure)

[metakuntyyy]

Thanks a lot.

And what is the benefit of the other one, is this something that allows to prove more theorems, as it's more specific?
I assume there is some (construction-dependent) structure in AlgebraicClosure that isn't exposed in IsAlgClosure, and that is forgotten once one obtains an instance of IsAlgClosure.

[Johan Commelin]

@metakuntyyy I think the main benefit is that it proves the existence of a field that satisfies the IsAlgClosure predicate.

[Johan Commelin]

If you have a theorem that doesn't involve algebraic closures, but you want to use one in the proof, then you need to pull an algebraic closure out of a hat. IsAlgClosure doesn't do that for you, but AlgebraicClosure does.

[Kevin Buzzard]

Ruben Van de Velde said:

Yes, that's correct. (At least I assume they're isomorphic - otherwise we wouldn't talk about the algebraic closure)

In my area it's quite common to avoid the phrase "the algebraic closure" because although it's unique up to isomorphism, it's in general not unique up to unique isomorphism. You often see "let $\overline{\mathbb{Q}}$ denote an algebraic closure of $\mathbb{Q}$" at the beginnings of papers.

[Damiano Testa]

In my area, I've seen "Let $\mathbb{C}$ be an algebraic closure of $\mathbb{Q}$"! It was kind of a joke, but it was important that the field was algebraically closed and uncountable!

[Ruben Van de Velde]

I remember a professor warning about that now, though I never understood what went wrong if you swapped i and -i

[Ruben Van de Velde]

(no need to explain, it's just of the many things I'm ignorant about)

[metakuntyyy]

Ah I guess I understand it now, assume we have a theorem that does not have IsAlgClosure and AlgebraicClosure as hypothesis, but for some reason we need to use a theorem that depends on IsAlgClosure inside of a Proof. We can generate an AlgebraicClosure and with that use IsAlgClosure to use the theorem.

Anyways, very thankful for the good answers.

[Luigi Massacci]

(deleted)

[Luigi Massacci]

(deleted)