[Merged by Bors] - feat(FieldTheory/PurelyInseparable): definition and basic results of purely inseparable extensions #9488

acmepjz · 2024-01-06T14:34:50Z

Main defintions:

IsPurelyInseparable: typeclass for purely inseparable field extension: an algebraic extension
E / F is purely inseparable if and only if the minimal polynomial of every element of E ∖ F
is not separable.

Main results (not exhaustive):

isPurelyInseparable_iff_mem_pow: a field extension E / F of exponential characteristic q is
purely inseparable if and only if for every element x of E, there exists a natural number n
such that x ^ (q ^ n) is contained in F.
IsPurelyInseparable.trans: if E / F and K / E are both purely inseparable extensions, then
K / F is also purely inseparable.
isPurelyInseparable_iff_natSepDegree_eq_one: E / F is purely inseparable if and only if for
every element x of E, its minimal polynomial has separable degree one.
isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C: a field extension E / F of exponential
characteristic q is purely inseparable if and only if for every element x of E, the minimal
polynomial of x over F is of form X ^ (q ^ n) - y for some natural number n and some
element y of F.
isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow: a field extension E / F of exponential
characteristic q is purely inseparable if and only if for every element x of E, the minimal
polynomial of x over F is of form (X - x) ^ (q ^ n) for some natural number n.
isPurelyInseparable_iff_finSepDegree_eq_one: an algebraic extension is purely inseparable
if and only if it has (finite) separable degree one.

TODO: remove the algebraic assumption. (will be in later PR)
IsPurelyInseparable.normal: a purely inseparable extension is normal.
separableClosure.isPurelyInseparable: if E / F is algebraic, then E is purely inseparable
over the (relative) separable closure of E / F.
IsPurelyInseparable.injective_comp_algebraMap: if E / F is purely inseparable, then for any
reduced ring L, the map (E →+* L) → (F →+* L) induced by algebraMap F E is injective.
In other words, a purely inseparable field extension is an epimorphism in the category of fields.
isPurelyInseparable_adjoin_iff_mem_pow: if F is of exponential characteristic q, then
F(S) / F is a purely inseparable extension if and only if for any x ∈ S, x ^ (q ^ n) is
contained in F for some n : ℕ.
Field.finSepDegree_eq: if E / F is algebraic, then the Field.finSepDegree F E is equal to
Field.sepDegree F E as a natural number. This means that the cardinality of Field.Emb F E
and the degree of (separableClosure F E) / F are both finite or infinite, and when they are
finite, they coincide.

TODO: (will be in later PR)

IsPurelyInseparable.of_injective_comp_algebraMap: if L is an algebraically closed field
containing E, such that the map (E →+* L) → (F →+* L) induced by algebraMap F E is
injective, then E / F is purely inseparable. In other words, epimorphisms in the category of
fields must be purely inseparable extensions. Need to use the fact that Emb F E is infintie
when E / F is (purely) transcendental.
Prove that the (infinite) inseparable degree are multiplicative; linearly disjoint argument is needed.

Mathlib/FieldTheory/IsSepClosed.lean

Mathlib/FieldTheory/PurelyInseparable.lean

Mathlib/FieldTheory/IsSepClosed.lean

Mathlib/FieldTheory/Perfect.lean

erdOne

I think the reviewing process will be faster if you can split everything except the new file into a new PR.

Mathlib/FieldTheory/PurelyInseparable.lean

Mathlib/FieldTheory/IsAlgClosed/Basic.lean

acmepjz · 2024-01-07T11:32:09Z

I think the reviewing process will be faster if you can split everything except the new file into a new PR.

OK, will do it later.

Mathlib/FieldTheory/PurelyInseparable.lean

acmepjz · 2024-02-04T01:05:22Z

I also have this

/-- If `E` is a perfect field of characteristic `p`, then the (relative) perfect closure
`perfectClosure F E` is perfect. -/
instance perfectClosure.perfectRing (p : ℕ) [ExpChar F p] [ExpChar E p]
    [PerfectRing E p] : PerfectRing (perfectClosure F E) p := .ofSurjective _ p fun x ↦ by

but maybe let's leave it for next PR?

alreadydone · 2024-02-04T03:39:59Z

As you like!

Mathlib/FieldTheory/PurelyInseparable.lean

riccardobrasca · 2024-02-06T13:05:06Z

Mathlib/FieldTheory/PurelyInseparable.lean

+
+variable (E)
+
+-- TODO: remove `halg` assumption


What are we missing for this TODO?

I think we need some result that for a transcendental extension E / F, the finSepDegree cannot be one, namely, there are at least two F-embeddings from E to the algebraic closure of E. Maybe @alreadydone has some preliminary works on it.

Let's keep this for another PR, has this one is already pretty long.

Mainly we need a version of IsTranscendenceBasis.isAlgebraic with IntermediateField.adjoin rather than Algebra.adjoin, and we need to construct different embeddings of these IntermediateField.adjoin (which are purely transcendental extensions, and for this purpose IsTranscendenceBasis can be relaxed to AlgebraicIndependent).
If we want to count the number of embeddings, even more work need to be done.
All these would better be done in another PR touching RingTheory/AlgebraicIndependent.

Co-authored-by: Riccardo Brasca <[email protected]>

riccardobrasca · 2024-02-06T13:58:01Z

Thanks!

bors d+

mathlib-bors · 2024-02-06T13:58:04Z

✌️ acmepjz can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

acmepjz · 2024-02-06T15:32:41Z

bors r+

…purely inseparable extensions (#9488) Main defintions: - `IsPurelyInseparable`: typeclass for purely inseparable field extension: an algebraic extension `E / F` is purely inseparable if and only if the minimal polynomial of every element of `E ∖ F` is not separable. Main results (not exhaustive): - `isPurelyInseparable_iff_mem_pow`: a field extension `E / F` of exponential characteristic `q` is purely inseparable if and only if for every element `x` of `E`, there exists a natural number `n` such that `x ^ (q ^ n)` is contained in `F`. - `IsPurelyInseparable.trans`: if `E / F` and `K / E` are both purely inseparable extensions, then `K / F` is also purely inseparable. - `isPurelyInseparable_iff_natSepDegree_eq_one`: `E / F` is purely inseparable if and only if for every element `x` of `E`, its minimal polynomial has separable degree one. - `isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C`: a field extension `E / F` of exponential characteristic `q` is purely inseparable if and only if for every element `x` of `E`, the minimal polynomial of `x` over `F` is of form `X ^ (q ^ n) - y` for some natural number `n` and some element `y` of `F`. - `isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow`: a field extension `E / F` of exponential characteristic `q` is purely inseparable if and only if for every element `x` of `E`, the minimal polynomial of `x` over `F` is of form `(X - x) ^ (q ^ n)` for some natural number `n`. - `isPurelyInseparable_iff_finSepDegree_eq_one`: an algebraic extension is purely inseparable if and only if it has (finite) separable degree one. **TODO:** remove the algebraic assumption. (will be in later PR) - `IsPurelyInseparable.normal`: a purely inseparable extension is normal. - `separableClosure.isPurelyInseparable`: if `E / F` is algebraic, then `E` is purely inseparable over the (relative) separable closure of `E / F`. - `IsPurelyInseparable.injective_comp_algebraMap`: if `E / F` is purely inseparable, then for any reduced ring `L`, the map `(E →+* L) → (F →+* L)` induced by `algebraMap F E` is injective. In other words, a purely inseparable field extension is an epimorphism in the category of fields. - `isPurelyInseparable_adjoin_iff_mem_pow`: if `F` is of exponential characteristic `q`, then `F(S) / F` is a purely inseparable extension if and only if for any `x ∈ S`, `x ^ (q ^ n)` is contained in `F` for some `n : ℕ`. - `Field.finSepDegree_eq`: if `E / F` is algebraic, then the `Field.finSepDegree F E` is equal to `Field.sepDegree F E` as a natural number. This means that the cardinality of `Field.Emb F E` and the degree of `(separableClosure F E) / F` are both finite or infinite, and when they are finite, they coincide. TODO: (will be in later PR) - `IsPurelyInseparable.of_injective_comp_algebraMap`: if `L` is an algebraically closed field containing `E`, such that the map `(E →+* L) → (F →+* L)` induced by `algebraMap F E` is injective, then `E / F` is purely inseparable. In other words, epimorphisms in the category of fields must be purely inseparable extensions. Need to use the fact that `Emb F E` is infintie when `E / F` is (purely) transcendental. - Prove that the (infinite) inseparable degree are multiplicative; linearly disjoint argument is needed. Co-authored-by: Junyan Xu <[email protected]> Co-authored-by: Junyan Xu <[email protected]>

mathlib-bors · 2024-02-06T16:16:20Z

Build failed (retrying...):

Build

mathlib-bors · 2024-02-06T16:34:09Z

Canceled.

alreadydone · 2024-02-06T17:01:09Z

Mathlib/Algebra/CharP/Reduced.lean

-    · rw [pow_mul', h, one_pow]
+  rw [pow_mul']
+  convert ← (iterateFrobenius_inj R p k).eq_iff
+  apply map_one


@riccardobrasca I moved one new lemma and two golfs from #9311 to this PR to streamline this proof below.

acmepjz · 2024-02-06T18:15:30Z

bors r+

…purely inseparable extensions (#9488) Main defintions: - `IsPurelyInseparable`: typeclass for purely inseparable field extension: an algebraic extension `E / F` is purely inseparable if and only if the minimal polynomial of every element of `E ∖ F` is not separable. Main results (not exhaustive): - `isPurelyInseparable_iff_mem_pow`: a field extension `E / F` of exponential characteristic `q` is purely inseparable if and only if for every element `x` of `E`, there exists a natural number `n` such that `x ^ (q ^ n)` is contained in `F`. - `IsPurelyInseparable.trans`: if `E / F` and `K / E` are both purely inseparable extensions, then `K / F` is also purely inseparable. - `isPurelyInseparable_iff_natSepDegree_eq_one`: `E / F` is purely inseparable if and only if for every element `x` of `E`, its minimal polynomial has separable degree one. - `isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C`: a field extension `E / F` of exponential characteristic `q` is purely inseparable if and only if for every element `x` of `E`, the minimal polynomial of `x` over `F` is of form `X ^ (q ^ n) - y` for some natural number `n` and some element `y` of `F`. - `isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow`: a field extension `E / F` of exponential characteristic `q` is purely inseparable if and only if for every element `x` of `E`, the minimal polynomial of `x` over `F` is of form `(X - x) ^ (q ^ n)` for some natural number `n`. - `isPurelyInseparable_iff_finSepDegree_eq_one`: an algebraic extension is purely inseparable if and only if it has (finite) separable degree one. **TODO:** remove the algebraic assumption. (will be in later PR) - `IsPurelyInseparable.normal`: a purely inseparable extension is normal. - `separableClosure.isPurelyInseparable`: if `E / F` is algebraic, then `E` is purely inseparable over the (relative) separable closure of `E / F`. - `IsPurelyInseparable.injective_comp_algebraMap`: if `E / F` is purely inseparable, then for any reduced ring `L`, the map `(E →+* L) → (F →+* L)` induced by `algebraMap F E` is injective. In other words, a purely inseparable field extension is an epimorphism in the category of fields. - `isPurelyInseparable_adjoin_iff_mem_pow`: if `F` is of exponential characteristic `q`, then `F(S) / F` is a purely inseparable extension if and only if for any `x ∈ S`, `x ^ (q ^ n)` is contained in `F` for some `n : ℕ`. - `Field.finSepDegree_eq`: if `E / F` is algebraic, then the `Field.finSepDegree F E` is equal to `Field.sepDegree F E` as a natural number. This means that the cardinality of `Field.Emb F E` and the degree of `(separableClosure F E) / F` are both finite or infinite, and when they are finite, they coincide. TODO: (will be in later PR) - `IsPurelyInseparable.of_injective_comp_algebraMap`: if `L` is an algebraically closed field containing `E`, such that the map `(E →+* L) → (F →+* L)` induced by `algebraMap F E` is injective, then `E / F` is purely inseparable. In other words, epimorphisms in the category of fields must be purely inseparable extensions. Need to use the fact that `Emb F E` is infintie when `E / F` is (purely) transcendental. - Prove that the (infinite) inseparable degree are multiplicative; linearly disjoint argument is needed. Co-authored-by: Junyan Xu <[email protected]> Co-authored-by: Junyan Xu <[email protected]>

mathlib-bors · 2024-02-06T19:27:02Z

Pull request successfully merged into master.

Build succeeded:

Change the expression "separable closure of `E / F`" to "separable closure of `F` in `E`", which IMO is closer to everyday usage. I think we should do the same for "perfect closure" in #9488. Also remove the use of some parenthesized adjectives: IMO "(some adjective)" signifies that "some adjective" will be assumed to be the default in subsequent text, making it unnecessary to mention "some adjective" every time. This applies to "(relative)" and "(infinite)" in the file SeparableClosure. Writing both "(infinite)" and "(finite)" signifies that both are assumed to be default, which is not our intention (I think we intend to make "infinite" the default). Therefore I kept the first "(infinite)" and removed all subsequent "(infinite)" and parentheses around "finite". In the file SeparableDegree, the infinite separable degree is not yet defined, so "finite" is the default instead: indeed the file omits "finite" almost everywhere, so I just remove the remaining three occurrences of "(finite)". Co-authored-by: Junyan Xu <[email protected]> Co-authored-by: acmepjz <[email protected]>

…purely inseparable extensions (#9488) Main defintions: - `IsPurelyInseparable`: typeclass for purely inseparable field extension: an algebraic extension `E / F` is purely inseparable if and only if the minimal polynomial of every element of `E ∖ F` is not separable. Main results (not exhaustive): - `isPurelyInseparable_iff_mem_pow`: a field extension `E / F` of exponential characteristic `q` is purely inseparable if and only if for every element `x` of `E`, there exists a natural number `n` such that `x ^ (q ^ n)` is contained in `F`. - `IsPurelyInseparable.trans`: if `E / F` and `K / E` are both purely inseparable extensions, then `K / F` is also purely inseparable. - `isPurelyInseparable_iff_natSepDegree_eq_one`: `E / F` is purely inseparable if and only if for every element `x` of `E`, its minimal polynomial has separable degree one. - `isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C`: a field extension `E / F` of exponential characteristic `q` is purely inseparable if and only if for every element `x` of `E`, the minimal polynomial of `x` over `F` is of form `X ^ (q ^ n) - y` for some natural number `n` and some element `y` of `F`. - `isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow`: a field extension `E / F` of exponential characteristic `q` is purely inseparable if and only if for every element `x` of `E`, the minimal polynomial of `x` over `F` is of form `(X - x) ^ (q ^ n)` for some natural number `n`. - `isPurelyInseparable_iff_finSepDegree_eq_one`: an algebraic extension is purely inseparable if and only if it has (finite) separable degree one. **TODO:** remove the algebraic assumption. (will be in later PR) - `IsPurelyInseparable.normal`: a purely inseparable extension is normal. - `separableClosure.isPurelyInseparable`: if `E / F` is algebraic, then `E` is purely inseparable over the (relative) separable closure of `E / F`. - `IsPurelyInseparable.injective_comp_algebraMap`: if `E / F` is purely inseparable, then for any reduced ring `L`, the map `(E →+* L) → (F →+* L)` induced by `algebraMap F E` is injective. In other words, a purely inseparable field extension is an epimorphism in the category of fields. - `isPurelyInseparable_adjoin_iff_mem_pow`: if `F` is of exponential characteristic `q`, then `F(S) / F` is a purely inseparable extension if and only if for any `x ∈ S`, `x ^ (q ^ n)` is contained in `F` for some `n : ℕ`. - `Field.finSepDegree_eq`: if `E / F` is algebraic, then the `Field.finSepDegree F E` is equal to `Field.sepDegree F E` as a natural number. This means that the cardinality of `Field.Emb F E` and the degree of `(separableClosure F E) / F` are both finite or infinite, and when they are finite, they coincide. TODO: (will be in later PR) - `IsPurelyInseparable.of_injective_comp_algebraMap`: if `L` is an algebraically closed field containing `E`, such that the map `(E →+* L) → (F →+* L)` induced by `algebraMap F E` is injective, then `E / F` is purely inseparable. In other words, epimorphisms in the category of fields must be purely inseparable extensions. Need to use the fact that `Emb F E` is infintie when `E / F` is (purely) transcendental. - Prove that the (infinite) inseparable degree are multiplicative; linearly disjoint argument is needed. Co-authored-by: Junyan Xu <[email protected]> Co-authored-by: Junyan Xu <[email protected]>

Change the expression "separable closure of `E / F`" to "separable closure of `F` in `E`", which IMO is closer to everyday usage. I think we should do the same for "perfect closure" in #9488. Also remove the use of some parenthesized adjectives: IMO "(some adjective)" signifies that "some adjective" will be assumed to be the default in subsequent text, making it unnecessary to mention "some adjective" every time. This applies to "(relative)" and "(infinite)" in the file SeparableClosure. Writing both "(infinite)" and "(finite)" signifies that both are assumed to be default, which is not our intention (I think we intend to make "infinite" the default). Therefore I kept the first "(infinite)" and removed all subsequent "(infinite)" and parentheses around "finite". In the file SeparableDegree, the infinite separable degree is not yet defined, so "finite" is the default instead: indeed the file omits "finite" almost everywhere, so I just remove the remaining three occurrences of "(finite)". Co-authored-by: Junyan Xu <[email protected]> Co-authored-by: acmepjz <[email protected]>

acmepjz added 2 commits January 6, 2024 20:51

add purely inseparable

582e1bd

add docs and results in earlier files

4c4de95

acmepjz added awaiting-review awaiting-CI t-algebra Algebra (groups, rings, fields, etc) labels Jan 6, 2024

acmepjz mentioned this pull request Jan 6, 2024

[Merged by Bors] - feat(FieldTheory/IsPerfectClosure): predicate IsPerfectClosure #8696

Closed

13 tasks

erdOne reviewed Jan 6, 2024

View reviewed changes

Mathlib/FieldTheory/IsSepClosed.lean Outdated Show resolved Hide resolved

erdOne reviewed Jan 6, 2024

View reviewed changes

alreadydone mentioned this pull request Jan 6, 2024

[Merged by Bors] - feat: cardinality of Field.Emb for algebraic extensions of infinite separable degree #9480

Closed

3 tasks

acmepjz added 2 commits January 7, 2024 05:01

apply suggestions

3aaa7de

add IsSepClosure.of_isAlgClosure_of_perfectField and apply suggestions

5d04ec9

alreadydone reviewed Jan 6, 2024

View reviewed changes

Mathlib/FieldTheory/IsSepClosed.lean Outdated Show resolved Hide resolved

alreadydone reviewed Jan 6, 2024

View reviewed changes

Mathlib/FieldTheory/Perfect.lean Outdated Show resolved Hide resolved

acmepjz added 4 commits January 7, 2024 07:55

move exists_finset_of_mem_adjoin to correct location

03df461

finish the proof and apply suggestion

df984a3

add a TODO in IsAlgClosed

8660aed

add Algebra.IsAlgebraic.isSepClosed

51ad728

github-actions bot removed the awaiting-CI label Jan 7, 2024

erdOne reviewed Jan 7, 2024

View reviewed changes

erdOne added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Jan 7, 2024

erdOne reviewed Jan 7, 2024

View reviewed changes

Mathlib/FieldTheory/PurelyInseparable.lean Outdated Show resolved Hide resolved

acmepjz added 3 commits January 7, 2024 21:50

apply suggestions and golf

eb0b50f

revert some file changes

a630bd6

Merge branch 'master' into acmepjz_purely_insep

025a2a7

This was referenced Jan 7, 2024

[Merged by Bors] - doc(FieldTheory/IsAlgClosed/Basic): add a TODO #9519

Closed

[Merged by Bors] - feat(FieldTheory/IsSepClosed): add some results on separable closure and perfect field #9522

Closed

acmepjz added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jan 7, 2024

alreadydone and others added 2 commits February 3, 2024 13:20

Merge branch 'purely_insep_merge' into acmepjz_purely_insep

a21436c

fix zero_pow

463e1ec

alreadydone force-pushed the acmepjz_purely_insep branch from 99637a3 to 463e1ec Compare February 3, 2024 18:42

minigolf

b7ea322

riccardobrasca approved these changes Feb 6, 2024

View reviewed changes

acmepjz and others added 2 commits February 6, 2024 21:17

Apply suggestions from code review

a18a36f

Co-authored-by: Riccardo Brasca <[email protected]>

fix compile error

97f82a8

github-actions bot added delegated and removed awaiting-review labels Feb 6, 2024

Merge branch 'master' into acmepjz_purely_insep

bfcc85b

fix

e0c5313

alreadydone reviewed Feb 6, 2024

View reviewed changes

mathlib-bors bot changed the title ~~feat(FieldTheory/PurelyInseparable): definition and basic results of purely inseparable extensions~~ [Merged by Bors] - feat(FieldTheory/PurelyInseparable): definition and basic results of purely inseparable extensions Feb 6, 2024

mathlib-bors bot closed this Feb 6, 2024

mathlib-bors bot deleted the acmepjz_purely_insep branch February 6, 2024 19:27

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(FieldTheory/PurelyInseparable): definition and basic results of purely inseparable extensions #9488

[Merged by Bors] - feat(FieldTheory/PurelyInseparable): definition and basic results of purely inseparable extensions #9488

acmepjz commented Jan 6, 2024 •

edited

Loading

erdOne left a comment

acmepjz commented Jan 7, 2024

acmepjz commented Feb 4, 2024

alreadydone commented Feb 4, 2024

riccardobrasca Feb 6, 2024

acmepjz Feb 6, 2024

riccardobrasca Feb 6, 2024

alreadydone Feb 6, 2024 •

edited

Loading

riccardobrasca commented Feb 6, 2024

mathlib-bors bot commented Feb 6, 2024

acmepjz commented Feb 6, 2024

mathlib-bors bot commented Feb 6, 2024

mathlib-bors bot commented Feb 6, 2024

alreadydone Feb 6, 2024

acmepjz commented Feb 6, 2024

mathlib-bors bot commented Feb 6, 2024

[Merged by Bors] - feat(FieldTheory/PurelyInseparable): definition and basic results of purely inseparable extensions #9488

[Merged by Bors] - feat(FieldTheory/PurelyInseparable): definition and basic results of purely inseparable extensions #9488

Conversation

acmepjz commented Jan 6, 2024 • edited Loading

erdOne left a comment

Choose a reason for hiding this comment

acmepjz commented Jan 7, 2024

acmepjz commented Feb 4, 2024

alreadydone commented Feb 4, 2024

riccardobrasca Feb 6, 2024

Choose a reason for hiding this comment

acmepjz Feb 6, 2024

Choose a reason for hiding this comment

riccardobrasca Feb 6, 2024

Choose a reason for hiding this comment

alreadydone Feb 6, 2024 • edited Loading

Choose a reason for hiding this comment

riccardobrasca commented Feb 6, 2024

mathlib-bors bot commented Feb 6, 2024

acmepjz commented Feb 6, 2024

mathlib-bors bot commented Feb 6, 2024

mathlib-bors bot commented Feb 6, 2024

alreadydone Feb 6, 2024

Choose a reason for hiding this comment

acmepjz commented Feb 6, 2024

mathlib-bors bot commented Feb 6, 2024

acmepjz commented Jan 6, 2024 •

edited

Loading

alreadydone Feb 6, 2024 •

edited

Loading