ofHom — Mathlib

English

There is a canonical way to regard a linear map f: X →ₗ[R] Y as a morphism in ModuleCat(R) from of R X to of R Y.

Русский

Существуют канонические отображения линейного отображения f: X →ₗ[R] Y в морфизм в ModuleCat(R) от of R X к of R Y.

LaTeX

$$$ \\forall f:\\; X \\to_{R} Y:\\; \\mathrm{ofHom}(f) : \\mathrm{of}(R,X) \\to \\mathrm{of}(R,Y). $$$

Lean4

/-- Typecheck a `LinearMap` as a morphism in `ModuleCat`. -/
abbrev ofHom {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] (f : X →ₗ[R] Y) :
    of R X ⟶ of R Y :=
  ConcreteCategory.ofHom (C := ModuleCat R) f

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