The field C_p

Stream: Is there code for X?

[Jiang Jiedong]

Is the completion of the algebraic closure of $\mathbb{Q}_p$ formalized in mathlib?

[Adam Topaz]

I think @María Inés de Frutos Fernández has indeed formalized this.

[Adam Topaz]

It's possible that Krasner's lemma (and hence the proof that $\mathbb{C}_p$ is algebraically closed) is still missing?

[María Inés de Frutos Fernández]

Yes, I have formalized $\mathbb{C}_p$ but it is not in mathlib yet. I have two open PRs that are a prerequisite for this: #15445 and #15373.

[Jiang Jiedong]

I nearly finished Krasner‘s lemma based on the work of @María Inés de Frutos Fernández . So I want to know if I can apply this lemma on C_p

[Adam Topaz]

Very nice!

[María Inés de Frutos Fernández]

You can find the formalization here.

[Johan Commelin]

@María Inés de Frutos Fernández Thanks for those PRs! I reviewed the shorter one. Are you planning to split up the large one?

[Riccardo Brasca]

I am also happy to review those, but I agree the bigger one should be split

[María Inés de Frutos Fernández]

I have extracted some parts of #15373 to #16767, #16768, #16770.

[Kim Morrison]

(Ruben has reviewed, these are all awaiting-author again.)

[María Inés de Frutos Fernández]

#16768, #16770, #16767 and #15445 are all ready for review again (based on the current comments, the last two seem ready to be merged).

[María Inés de Frutos Fernández]

María Inés de Frutos Fernández said:

I have extracted some parts of #15373 to #16767, #16768, #16770.

#15373 should now be ready for review.

[María Inés de Frutos Fernández]

I opened several more PRs towards the definition of C_p. The main ones are:

• #23184 : given a nonarchimedean normed field K and a finite extensionL/K, the function L → ℝ sending x : L to the maximum of ‖ σ x ‖ over all σ : L ≃ₐ[K] L is an algebra norm on L.
• #23301: the spectral value and the spectral norm.
• #23333: proof of the unique extension theorem for nonarchimedean norms.