actionHom_id — Mathlib

English

For any morphism f: c ⟶ c' in C and any object d in D, the action of f on the identity morphism id_d equals the left action by f: f ⊙ₗ (id_d) = c ⊴ₗ f.

Русский

Для морфизма f: c ⟶ c' в C и любого объекта d в D, действие f на идентичность id_d равно левому действию f: f ⊙ₗ (id_d) = c ⊴ₗ f.

LaTeX

$$$\\forall f: c\\to c',\\; d:\\, D:\\; f ⊙ₗ (\\mathbb{1}_d) = c \\ ⊴ₗ f$$$

Lean4

@[simp]
theorem actionHom_id {c c' : C} (f : c ⟶ c') (d : D) : f ⊙ₗₘ (𝟙 d) = f ⊵ₗ d := by simp [actionHom_def]

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