Separably generated extensions

We aim to formalize the following result:

Let K/k be a finitely generated field extension with characteristic p > 0, then TFAE

1. K/k is separably generated
2. If { sᵢ } ⊆ K is an arbitrary k-linearly independent set, { sᵢᵖ } ⊆ K is also k-linearly independent
3. K ⊗ₖ k^{1/p} is reduced
4. K is geometrically reduced over k.
5. k and Kᵖ are linearly disjoint over kᵖ in K.

Main result

• exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow: (2) ⇒ (1)

def MvPolynomial.toPolynomialAdjoinImageCompl {k : Type u_1} {K : Type u_2} {ι : Type u_3} [Field k] [Field K] [Algebra k K] (F : MvPolynomial ι k) (a : ι → K) (i : ι) : Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))

View a multivariate polynomial F(x₁,...,xₙ) as a polynomial in xᵢ with coefficients in F(x₁,...,xᵢ₋₁,xᵢ₊₁,...,xₙ).

Equations

• One or more equations did not get rendered due to their size.

theorem MvPolynomial.aeval_toPolynomialAdjoinImageCompl_eq_zero {k : Type u_1} {K : Type u_2} {ι : Type u_3} [Field k] [Field K] [Algebra k K] {a : ι → K} {F : MvPolynomial ι k} (hFa : (aeval a) F = 0) (i : ι) : (Polynomial.aeval (a i)) (F.toPolynomialAdjoinImageCompl a i) = 0

theorem MvPolynomial.irreducible_toPolynomialAdjoinImageCompl {k : Type u_1} {K : Type u_2} {ι : Type u_3} [Field k] [Field K] [Algebra k K] {a : ι → K} {F : MvPolynomial ι k} (hF : Irreducible F) (i : ι) (H : AlgebraicIndependent k fun (x : ↑{j : ι | j ≠ i}) => a ↑x) : Irreducible (F.toPolynomialAdjoinImageCompl a i)

theorem MvPolynomial.irreducible_of_forall_totalDegree_le {k : Type u_1} {K : Type u_2} {ι : Type u_3} [Field k] [Field K] [Algebra k K] {a : ι → K} {F : MvPolynomial ι k} (HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree) (hF0 : F ≠ 0) (hFa : (aeval a) F = 0) : Irreducible F

If F has minimal total degree among the relations of a, then F is irreducible.

theorem MvPolynomial.coeff_toPolynomialAdjoinImageCompl_ne_zero {k : Type u_1} {K : Type u_2} {ι : Type u_3} [Field k] [Field K] [Algebra k K] {a : ι → K} {F : MvPolynomial ι k} (HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree) (σ : ι →₀ ℕ) (hσ : σ ∈ F.support) (i : ι) (hσi : σ i ≠ 0) : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) ≠ 0

theorem MvPolynomial.isAlgebraic_of_mem_vars_of_forall_totalDegree_le {k : Type u_1} {K : Type u_2} {ι : Type u_3} [Field k] [Field K] [Algebra k K] {a : ι → K} {F : MvPolynomial ι k} (HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree) (hFa : (aeval a) F = 0) (i : ι) (hi : i ∈ F.vars) : IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)

theorem MvPolynomial.exists_mem_support_not_dvd_of_forall_totalDegree_le {k : Type u_1} {K : Type u_2} {ι : Type u_3} [Field k] [Field K] [Algebra k K] (p : ℕ) (hp : Nat.Prime p) (H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun (x : K) => x ^ p) ↑s) {a : ι → K} {F : MvPolynomial ι k} (HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree) (hF0 : F ≠ 0) (hFa : (aeval a) F = 0) : ∃ (i : ι), ∃ σ ∈ F.support, ¬p ∣ σ i

theorem exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow {k : Type u_1} {K : Type u_2} {ι : Type u_3} [Field k] [Field K] [Algebra k K] (p : ℕ) (hp : Nat.Prime p) (H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun (x : K) => x ^ p) ↑s) {a : ι → K} (n : ι) [ExpChar k p] (ha' : IsTranscendenceBasis k fun (i : { i : ι // i ≠ n }) => a ↑i) : ∃ (i : ι), (IsTranscendenceBasis k fun (j : { j : ι // j ≠ i }) => a ↑j) ∧ IsSeparable (↥(IntermediateField.adjoin k (a '' {i}ᶜ))) (a i)

Suppose k has chararcteristic p and a₁,...,aₙ is a transcendental basis of K/k. Suppose furthermore that if { sᵢ } ⊆ K is an arbitrary k-linearly independent set, { sᵢᵖ } ⊆ K is also k-linearly independent (which is true when K ⊗ₖ k^{1/p} is reduced).

Then some subset of a₁,...,aₙ₊₁ forms a transcedental basis that a₁,...,aₙ₊₁ are separable over.

theorem exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow' {k : Type u_1} {K : Type u_2} {ι : Type u_3} [Field k] [Field K] [Algebra k K] (p : ℕ) (hp : Nat.Prime p) (H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun (x : K) => x ^ p) ↑s) {a : ι → K} [ExpChar k p] (s : Set ι) (n : ι) (ha : IsTranscendenceBasis k fun (i : ↑s) => a ↑i) (hn : n ∉ s) : ∃ (i : ι), (IsTranscendenceBasis k fun (j : ↑(insert n s \ {i})) => a ↑j) ∧ IsSeparable (↥(IntermediateField.adjoin k (a '' (insert n s \ {i})))) (a i)

theorem exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_adjoin_eq_top {k : Type u_1} {K : Type u_2} {ι : Type u_3} [Field k] [Field K] [Algebra k K] (p : ℕ) (hp : Nat.Prime p) (H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun (x : K) => x ^ p) ↑s) {a : ι → K} (n : ι) [ExpChar k p] (ha : IntermediateField.adjoin k (Set.range a) = ⊤) (ha' : IsTranscendenceBasis k fun (i : { i : ι // i ≠ n }) => a ↑i) : ∃ (i : ι), (IsTranscendenceBasis k fun (j : { j : ι // j ≠ i }) => a ↑j) ∧ Algebra.IsSeparable (↥(IntermediateField.adjoin k (a '' {i}ᶜ))) K

Suppose k has chararcteristic p and K/k is generated by a₁,...,aₙ₊₁, where a₁,...aₙ forms a transcendental basis. Suppose furthermore that if { sᵢ } ⊆ K is an arbitrary k-linearly independent set, { sᵢᵖ } ⊆ K is also k-linearly independent (which is true when K ⊗ₖ k^{1/p} is reduced).

Then some subset of a₁,...,aₙ₊₁ forms a separable transcedental basis.

theorem exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_fg {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (p : ℕ) (hp : Nat.Prime p) (H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun (x : K) => x ^ p) ↑s) [ExpChar k p] (Hfg : ⊤.FG) : ∃ (s : Finset K), IsTranscendenceBasis k Subtype.val ∧ Algebra.IsSeparable (↥(IntermediateField.adjoin k ↑s)) K

Suppose k has chararcteristic p and K/k is finitely generated. Suppose furthermore that if { sᵢ } ⊆ K is an arbitrary k-linearly independent set, { sᵢᵖ } ⊆ K is also k-linearly independent (which is true when K ⊗ₖ k^{1/p} is reduced).

Then K/k is finite separably generated.

TODO: show that this is an if and only if.

theorem exists_isTranscendenceBasis_and_isSeparable_of_perfectField {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [PerfectField k] (Hfg : ⊤.FG) : ∃ (s : Finset K), IsTranscendenceBasis k Subtype.val ∧ Algebra.IsSeparable (↥(IntermediateField.adjoin k ↑s)) K

Any finitely generated extension over perfect fields are separably generated.