comp_algebraMap_of_tower — Mathlib

English

The composition of the underlying ring hom with the R-algebra map equals the R-algebra map on B: (f : A →ₐ[S] B).comp (algebraMap_R A) = algebraMap_R B.

Русский

Композиция тождественна алгебраMap_R_B: (f : A →ₐ[S] B).comp (algebraMap_R A) = algebraMap_R B.

LaTeX

$$$ ((f : A \to_{{\mathsf{S}}} B).comp (algebraMap_R A)) = algebraMap_R B$$

Lean4

@[simp]
theorem _root_.AlgHom.comp_algebraMap_of_tower (f : A →ₐ[S] B) : (f : A →+* B).comp (algebraMap R A) = algebraMap R B :=
  RingHom.ext
    (AlgHom.map_algebraMap f)
      -- conflicts with IsScalarTower.Subalgebra

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