eq_bot_of_isPurelyInseparable_of_isSeparable

English

If an intermediate field L of E/F is both purely inseparable and separable, then L = F.

Русский

Если промежуточное поле L внутри E/F одновременно чисто безразделимо и сепарабельно, то L = F.

LaTeX

$$$L = \bot$ under [IsPurelyInseparable F L] and [Algebra.IsSeparable F L].$$

Lean4

/-- If an intermediate field of `E / F` is both purely inseparable and separable, then it is equal
to `F`. -/
theorem eq_bot_of_isPurelyInseparable_of_isSeparable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E]
    (L : IntermediateField F E) [IsPurelyInseparable F L] [Algebra.IsSeparable F L] : L = ⊥ :=
  bot_unique fun x hx ↦
    by
    obtain ⟨y, hy⟩ := IsPurelyInseparable.surjective_algebraMap_of_isSeparable F L ⟨x, hx⟩
    exact ⟨y, congr_arg (algebraMap L E) hy⟩

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