map_id

Mathlib.RingTheory.Ideal.Maps

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

English

The composition of two maps corresponds to the map of the composed homomorphism.

Русский

Слоение двух отображений соответствует отображению композиции гомоморфизмов.

LaTeX

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

Lean4

@[simp]
theorem map_id : I.map (RingHom.id R) = I :=
  (gc_map_comap (RingHom.id R)).l_unique GaloisConnection.id comap_id

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

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

Разделы

Аффилиация

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