[Merged by Bors] - feat(Mathlib/FieldTheory/IsSepClosed) separably closed field and separable closure - basic definition

[acmepjz]

Main changes

• Add IsSepClosed and basic properties.
• Add IsSepClosure and basic properties.

---

[kbuzzard]

This looks great to me! Thank you very much! I've left a few comments.

[kbuzzard]

I think it should be clarified here in the docstring that K is still a field (given that you are allowing R to be a commutative ring). Maybe "This means that K is a field, the map from..."?

Mathematical question: if K is a field, separable over a commutative ring R, and if the map from R to K is injective, then is R also necessarily a field?

[acmepjz]

I think the concept "separable over a commutative ring R" itself is quite dangerous. In mathlib4 the definition of IsSeparable R K require that all element of K is integral over R. So I think your mathematical question should be true (by considering Frac(R) in K).

However there are another definition of separable algebra https://en.wikipedia.org/wiki/Separable_algebra which claims to be the generalization of separable field extension. Using this definition I think Q is a separable Z algebra, while it's not integral over Z. So maybe we should stick on fields when talking about separable extension.

[kbuzzard]

This PR is already nearly 200 lines long -- don't add any more stuff to it! It looks ready to go to me; do future work in a different PR.

[acmepjz]

Sure, let me clean it up later today.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Build failed (retrying...):

• Lint style

[bors]

Build failed (retrying...):

• Lint style

[bors]

Build failed:

• Lint style

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style