congr_map_apply — Mathlib

English

A presheaf morphism is semilinear with respect to the action of R: for any f, r, m, M.map f (r • m) = R.map f r • M.map f m.

Русский

Морфизм прешефа линейноSemilinear относительно действия R: для любых f, r, m выполняется M.map f (r • m) = R.map f r • M.map f m.

LaTeX

$$$M.map f (r \cdot m) = R.map f r \cdot M.map f m,$$$

Lean4

theorem congr_map_apply {X Y : Cᵒᵖ} {f g : X ⟶ Y} (h : f = g) (m : M.obj X) : M.map f m = M.map g m := by rw [h]

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