injective_restrictDomain — Mathlib

English

In a tower with a reduced base, the restrictDomain map associated to an algebra homomorphism is injective.

Русский

В цилиндре с редуцированной базой отображение restrictDomain у алгебраического гомоморфа инъективно.

LaTeX

$$$ [CommRing L] [IsReduced L] [Algebra R L] [IsScalarTower R F E] \Rightarrow \text{Injective}(\text{AlgHom.restrictDomain } F)$$$

Lean4

theorem injective_restrictDomain [CommRing L] [IsReduced L] [Algebra R L] [IsScalarTower R F E] :
    Function.Injective (AlgHom.restrictDomain (A := R) F (C := E) (D := L)) := fun _ _ eq ↦
  AlgHom.coe_ringHom_injective <| injective_comp_algebraMap F E L <| congr_arg AlgHom.toRingHom eq

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