eq_bot_of_isPurelyInseparable_of_isSeparable

English

If a subalgebra L of E/F is both purely inseparable and separable, then L equals F.

Русский

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

LaTeX

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

Lean4

/-- If a subalgebra of `E / F` is both purely inseparable and separable, then it is equal
to `F`. -/
theorem eq_bot_of_isPurelyInseparable_of_isSeparable (L : Subalgebra 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 (Subalgebra.val _) hy⟩

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