bijective_algebraMap_of_isSeparable

English

If E/F is purely inseparable and separable, then the algebra map F→E is bijective (under mild nontriviality conditions).

Русский

Если расширение E/F чисто безразделимо и сепарабельно, то карта F→E является биективной (при некоторых условиях ненулевости).

LaTeX

$$$ [Nontrivial\ E] [NoZeroSMulDivisors F E] [IsPurelyInseparable F E] [Algebra.IsSeparable F E] \Rightarrow \text{Bijective}(\text{algebraMap } F E). $$$

Lean4

/-- If `E / F` is both purely inseparable and separable, then `algebraMap F E` is bijective. -/
theorem bijective_algebraMap_of_isSeparable [Nontrivial E] [NoZeroSMulDivisors F E] [IsPurelyInseparable F E]
    [Algebra.IsSeparable F E] : Function.Bijective (algebraMap F E) :=
  ⟨FaithfulSMul.algebraMap_injective F E, surjective_algebraMap_of_isSeparable F E⟩

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