bijective_of_isScalarTower' — Mathlib

English

If R is a field with an injective K-algebra map to L and L is algebraic over K, then any K-algebra hom from R to L is bijective.

Русский

Если R — поле и есть инъективное отображение K-алгебра из R в L, и L алгебраичен над K, то любая K-алгебраическая гомоморфизм R→L биективен.

LaTeX

$$$[\mathrm{Field\ R}] [\mathrm{Algebra\ K\ R}] [\mathrm{NoZeroSMulDivisors\ K\ R}] [\mathrm{Algebra.IsAlgebraic\ K\ R}] [\mathrm{Algebra\ K\ L}] [\mathrm{IsScalarTower\ K\ L\ R}] (f : R \to_{K} L) : \mathrm{Function.Bijective}\ f$$$

Lean4

theorem bijective_of_isScalarTower' [Field R] [Algebra K R] [NoZeroSMulDivisors K R] [Algebra.IsAlgebraic K R]
    [Algebra L R] [IsScalarTower K L R] (f : R →ₐ[K] L) : Function.Bijective f :=
  (algHom_bijective₂ f (IsScalarTower.toAlgHom K L R)).1

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