linearEquivMap_apply — Mathlib

English

For a finitely presented M, the value of the canonical map on f equals the IsLocalizedModule.map action on f.

Русский

Для модуля с конечной презентацией значение канонического отображения на f совпадает с действием IsLocalizedModule.map на f.

LaTeX

$$$$ \\text{Module.FinitePresentation.linearEquivMap } S ((\\mathrm{LocalizedModule.mkLinearMap} S (M \\to N)) f) = (\\mathrm{IsLocalizedModule.map} S (\\mathrm{LocalizedModule.mkLinearMap} S M) (\\mathrm{LocalizedModule.mkLinearMap} S N)) f. $$$$

Lean4

theorem linearEquivMap_apply [Module.FinitePresentation R M] (f : M →ₗ[R] N) :
    Module.FinitePresentation.linearEquivMap S ((LocalizedModule.mkLinearMap S (M →ₗ[R] N)) f) =
      (IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N)) f :=
  IsLocalizedModule.linearEquiv_apply S _ _ f

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