mapExtendScalars — Mathlib

English

Given S-localized endomorphisms g₁ and g₂, extend a linear map l to act on localized modules, and then restrict as needed to compare in a localized setting.

Русский

Для локализованных по S эндоморфизмов g₁ и g₂ расширяем отображение l так, чтобы действовать на локализованных модулях, затем при необходимости ограничиваем для сопоставления в локализованной системе.

LaTeX

$$$\\text{mapExtendScalars} : (M \\to_R N) \\mapsto (M' \\to_{R_s} N')$$$

Lean4

/-- A linear map `M →ₗ[R] N` gives a map between localized modules `Mₛ →ₗ[Rₛ] Nₛ`. -/
@[simps!]
noncomputable def mapExtendScalars : (M →ₗ[R] N) →ₗ[R] (M' →ₗ[Rₛ] N') :=
  ((LinearMap.extendScalarsOfIsLocalizationEquiv S Rₛ).restrictScalars R).toLinearMap ∘ₗ map S f g

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