map_mapₐ — Mathlib

English

For AlgHom f and g, the composition of maps equals the map of the composed AlgHom.

Русский

Для AlgHom f и g композиция отображений равна отображению композиции AlgHom.

LaTeX

$$$ (I.map f).map g = I.map (g \circ f) $$$

Lean4

theorem map_mapₐ {R A B C : Type*} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C]
    [Algebra R C] {I : Ideal A} (f : A →ₐ[R] B) (g : B →ₐ[R] C) : (I.map f).map g = I.map (g.comp f) :=
  I.map_map f.toRingHom g.toRingHom

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