map_id_id — Mathlib

English

Applying the coproduct map to identity maps on M and N yields the identity on the coproduct M ∗ N: map(id_M, id_N) = id_{M ∗ N}.

Русский

Применение отображения копрода к тождественным отображениям на M и N даёт тождественное отображение на копрод M ∗ N: map(id_M, id_N) = id_{M ∗ N}.

LaTeX

$$$ \operatorname{map}(\mathrm{id}_M, \mathrm{id}_N) = \mathrm{id}_{M \ast N}$$$

Lean4

@[to_additive (attr := simp)]
theorem map_id_id : map (.id M) (.id N) = .id (M ∗ N) :=
  hom_ext rfl rfl

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