algebraMap_injective_of_field_isFractionRing

English

The base algebra map is injective under the stated fraction-ring hypotheses.

Русский

Базовое отображение алгебраического отображения инъективно при заданных условиях дробной локализации.

LaTeX

$$algebraMap_injective_of_field_isFractionRing R S K L$$

Lean4

theorem algebraMap_injective_of_field_isFractionRing (K L : Type*) [Field K] [Semiring L] [Nontrivial L] [Algebra R K]
    [IsFractionRing R K] [Algebra S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] :
    Function.Injective (algebraMap R S) :=
  by
  refine Function.Injective.of_comp (f := algebraMap S L) ?_
  rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R K L]
  exact (algebraMap K L).injective.comp (IsFractionRing.injective R K)

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