comap_ker

Mathlib.RingTheory.Ideal.Maps

URI: https://scilib.ai/kg/mathlib#RingHom.comap_ker

← MathLib Explorer

English

For ring homomorphisms f: S → R and g: T → S, we have (ker f).comap g = ker (f ∘ g).

Русский

Для гомоморфизмов f: S → R и g: T → S выполнено (ker f).comap g = ker (f ∘ g).

LaTeX

$$$\\ker f\\,\\mathrm{comap}\\ g = \\ker (f \\circ g)$$$

Lean4

theorem comap_ker (f : S →+* R) (g : T →+* S) : (ker f).comap g = ker (f.comp g) := by
  rw [RingHom.ker_eq_comap_bot, Ideal.comap_comap, RingHom.ker_eq_comap_bot]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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