ihom_map_apply — Mathlib

English

In ModuleCat, for f: N → P and g: ModuleCat.of R (M → N), the induced map (ihom M).map f g equals the composite g ≫ f.

Русский

В ModuleCat, для отображения f: N → P и g: ModuleCat.of R (M → N), полученное отображение (ihom M).map f g равно композиции g ≫ f.

LaTeX

$$$\\big( (\\mathrm{ihom}\\ M).\\mathrm{map} \\ f \\ g \\big) = g \\circ f$$$

Lean4

theorem ihom_map_apply {M N P : ModuleCat.{u} R} (f : N ⟶ P) (g : ModuleCat.of R (M ⟶ N)) : (ihom M).map f g = g ≫ f :=
  rfl

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