bijective_of_isScalarTower — Mathlib

English

Given a K-algebra hom f from R to L in a scalar tower K ⊆ L ⊆ R, f is bijective.

Русский

При наличии тетрады K ⊆ L ⊆ R и т.д., отображение f будет биективно.

LaTeX

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

Lean4

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

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