map_id

Mathlib.RingTheory.AdicCompletion.Functoriality

URI: https://scilib.ai/kg/mathlib#AdicCompletion.AdicCauchySequence.map_id

English

The map applied to the identity on M behaves identically on the adic completion: map I (id M) = id.

Русский

Отображение региона ядра на адическом завершении совпадает с тождественным отображением.

LaTeX

$$$\mathrm{map} \ I\ (\mathrm{id}\ M) = \mathrm{id}$$$

Lean4

@[simp]
theorem map_id : map I (LinearMap.id (M := M)) = LinearMap.id :=
  rfl

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

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

Разделы

Аффилиация

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