linearDisjoint_of_isPurelyInseparable_of_isSeparable

English

With separability, each basis vector raised to q^n remains within the span.

Русский

При разделяемости каждый вектор базиса, возведенный в q^n, продолжает находиться в порождении.

LaTeX

$$$\operatorname{span}\{b_i^{q^n}\}=E$$$

Lean4

/-- If `K / E / F` is a field extension tower such that `E / F` is purely inseparable,
if `S` is an intermediate field of `K / F` which is separable over `F`, then `S` and `E` are
linearly disjoint over `F`. -/
theorem linearDisjoint_of_isPurelyInseparable_of_isSeparable [IsPurelyInseparable F E] (S : IntermediateField F K)
    [Algebra.IsSeparable F S] : S.LinearDisjoint E :=
  have ⟨ι, ⟨b⟩⟩ := Module.Basis.exists_basis F S
  .of_basis_left b <|
    b.linearIndependent.map' S.val.toLinearMap
        (LinearMap.ker_eq_bot_of_injective S.val.injective) |>.map_of_isPurelyInseparable_of_isSeparable
      E fun i ↦ by simpa only [IsSeparable, minpoly_eq] using Algebra.IsSeparable.isSeparable F (b i)

Похожие утверждения