comp_id_fgModuleCat — Mathlib

English

The forgetful functor FGModuleCat k → ModuleCat k creates all finite colimits: colimits in FGModuleCat can be realized by the corresponding colimits in ModuleCat.

Русский

Функтор забывания FGModuleCat k → ModuleCat k создаёт все конечные конические пределы: пределы в FGModuleCat могут быть реализованы как пределы в ModuleCat.

LaTeX

$$def forget₂CreatesColimit (F : J ⥤ FGModuleCat k) : CreatesColimit F (forget₂ (FGModuleCat k) (ModuleCat k))$$

Lean4

@[simp]
theorem comp_id_fgModuleCat {R} [Ring R] {G : FGModuleCat.{v} R} {H : Type v} [AddCommGroup H] [Module R H]
    (f : G →ₗ[R] H) : f.comp (ModuleCat.Hom.hom (𝟙 G)) = f :=
  ModuleCat.hom_ext_iff.mp <| Category.id_comp (ModuleCat.ofHom f)

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