instUniqueAlgHomOfIsPurelyInseparable

English

If E/F is purely inseparable, then there exists a unique F-algebra homomorphism E → L for any suitable L.

Русский

Если E/F чисто бесприводно, то для каждого подходящего L существует один единственный F-алгеброморфизм E → L.

LaTeX

$$$\text{Unique}(E \to_{F} L)$$$

Lean4

instance instUniqueAlgHomOfIsPurelyInseparable [IsPurelyInseparable F E] (L : Type w) [CommRing L] [IsReduced L]
    [Algebra F L] [Algebra E L] [IsScalarTower F E L] : Unique (E →ₐ[F] L) :=
  uniqueOfSubsingleton (IsScalarTower.toAlgHom F E L)

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