Theorems · Theorem · field theory

exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow

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

Suppose k has characteristic p and a₁,...,aₙ is a transcendence 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 transcendence basis over which a₁,...,aₙ₊₁ are separable.

Defined in

Mathlib.FieldTheory.SeparablyGenerated

Cited by

2 results in Mathlib

Foundations

Depth 152 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebraExpChar