ofHom — Mathlib

English

A linear map f: V → W induces a morphism FGModuleCat.of R V ⟶ FGModuleCat.of R W.

Русский

Линейное отображение f: V → W индуцирует морфизм FGModuleCat.of R V ⟶ FGModuleCat.of R W.

LaTeX

$$$f: V \\to W \\quad \\Rightarrow\\quad \\mathrm{FGModuleCat}.of(R,V) \\to \\mathrm{FGModuleCat}.of(R,W)$$$

Lean4

/-- Lift a linear map between finitely generated modules to `FGModuleCat R`. -/
abbrev ofHom {V W : Type v} [AddCommGroup V] [Module R V] [Module.Finite R V] [AddCommGroup W] [Module R W]
    [Module.Finite R W] (f : V →ₗ[R] W) : of R V ⟶ of R W :=
  ModuleCat.ofHom f

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