Theorems · Theorem · field theory

exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_adjoin_eq_top

∀ {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],
        IntermediateField.adjoin k (Set.range a) = ⊤ →
          (IsTranscendenceBasis k fun i => a ↑i) →
            ∃ i,
              (IsTranscendenceBasis k fun j => a ↑j) ∧ Algebra.IsSeparable (↥(IntermediateField.adjoin k (a '' {i}ᶜ))) K

Suppose k has characteristic p and K/k is generated by a₁,...,aₙ₊₁, where a₁,...aₙ form a transcendence 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 separating transcendence basis.

Defined in

Mathlib.FieldTheory.SeparablyGenerated

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraExpChar