map'_id — Mathlib

English

A companion statement that the map' for extension of scalars respects identity morphisms on modules.

Русский

Сопутствующее утверждение: отображение map' при расширении скаляров сохраняет идентичность морфизмов на модулях.

LaTeX

$$$\mathrm{map'} f (\mathrm{id}_M) = \mathrm{id}_{\mathrm{ExtendScalars}(f) M}$$$

Lean4

theorem map'_id {M : ModuleCat.{v} R} : map' f (𝟙 M) = 𝟙 _ := by simp [map', obj']

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