feat(FieldTheory): adjoin pth roots

[dleijnse]

For a field k of exponential characteristic p and a subset S of k, we define the extension of k obtained by adjoining all p-th roots of elements of S. We prove that this is a purely inseparable extension, and provide some basic API.

---

[github-actions[bot]]

PR summary 915cd38ee5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.FieldTheory.PurelyInseparable.AdjoinPthRoots (new file)	1489

---

Declarations diff

+ IntermediateField.adjoinPthRoots + adjoinPthRoots_finite_of_finite + adjoinPthRoots_mem_frobenius_img + adjoinPthRoots_mem_frobenius_img' + adjoinPthRoots_mono + adjoinPthRoots_purelyInseparable + instance : ExpChar (AlgebraicClosure k) p := ExpChar.of_injective_algebraMap' k _

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[dleijnse]

!bench

[leanprover-radar]

Benchmark results for 2f52a9975ec88641e5914c46c376fbbd001c34c6 against 915cd38ee571dc4dac8c536ff191c397abf53a5c are in! @dleijnse

No significant changes detected.

[artie2000]

Is it standard in this part of the library to construct field extensions as IntermediateFields below the algebraic closure? That's not the design of AdjoinRoot, IsAdjoinRoot, QuadraticExtension, or IsCyclotomicExtension, which are the examples I am familiar with.

[dleijnse]

I'm not sure whether this is standard or not, I don't know of a similar construction in the library which uses IntermediateField but also could have been constructed in another way. My main motivation for constructing it as an IntermediateField is that I automatically get instances such as Algebra k (adjoinPthRoots p S) and Field (adjoinPthRoots p S). And for some of the applications I have in mind I need to take the compositum of these fields together with other fields, which is easiest if we already have these fields as intermediate fields. But now that you mentioned AdjoinRoot and cyclotomic extensions, I see that these constructions work more generally; also over commutative rings. The same holds of course for adjoining pth roots, so the construction could maybe be generalized.

[artie2000]

@dleijnse those constructions could have equally been implemented using Subalgebra. I wasn't trying to point out he distinction between ring and field, but rather the distinction between defining the extension as a substructure of the algebraic closure and defining the extension as a type in itself.