map_idₐ

Mathlib.RingTheory.Ideal.Maps

URI: https://scilib.ai/kg/mathlib#Ideal.map_idₐ

English

For algebra homomorphisms, the same map-map compatibility holds for AlgebraHom maps.

Русский

Для алгебра-гомоморфизмов сохраняется совместимость map-map для алгебрических отображений.

LaTeX

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

Lean4

@[simp]
theorem map_idₐ {R S : Type*} [CommSemiring R] [Semiring S] [Algebra R S] (I : Ideal S) :
    Ideal.map (AlgHom.id R S) I = I :=
  I.map_id

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru