id_comp — Mathlib

English

Composition with an identity morphism leaves the other morphism unchanged: comp (id Q) f = f.

Русский

Сложение с тождестенным морфизмом оставляет другой морфизм неизменным: comp (id Q) f = f.

LaTeX

$$$\\mathrm{comp}(\\mathrm{id}_Q, f)=f$$$

Lean4

@[simp]
theorem id_comp {ι₂ M₂ N₂ : Type*} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
    (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : Hom P Q) : comp f (id P) = f := by ext x <;> simp

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