English
For modules with finite presentation, the ExtendScalars map evaluated at f coincides with the mapExtendScalars construction.
Русский
Для модулей с конечной презентацией отображение ExtendScalars, применённое к f, совпадает с конструктором mapExtendScalars.
LaTeX
$$$$ \\text{Module.FinitePresentation.linearEquivMapExtendScalars apply } S ((LocalizedModule.mkLinearMap S (M \\to N)) f) = (IsLocalizedModule.mapExtendScalars S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N) (Localization S)) f. $$$$
Lean4
instance gmulAction [AddMonoid M] [DistribMulAction A M] [SetLike σ M] [SetLike.GradedMonoid 𝓐]
[SetLike.GradedSMul 𝓐 𝓜] : GradedMonoid.GMulAction (fun i => 𝓐 i) fun i => 𝓜 i :=
{
SetLike.toGSMul 𝓐
𝓜 with
one_smul := fun ⟨_i, _m⟩ => Sigma.subtype_ext (zero_vadd _ _) (one_smul _ _)
mul_smul := fun ⟨_i, _a⟩ ⟨_j, _a'⟩ ⟨_k, _b⟩ => Sigma.subtype_ext (add_vadd _ _ _) (mul_smul _ _ _) }
