English
Localization of modules commutes with binary products: if f and g are localized, then their product map f.prodMap g is localized as well.
Русский
Локализация модулей сохраняется при бинарных произведениях: если отображения f, g локализованы, то и их произведение f.prodMap g локализовано.
LaTeX
$$$IsLocalizedModule\\; S\\; (f.\\mathrm{prodMap}\\; g)$$$
Lean4
/-- Localization of modules commutes with binary products. -/
instance prodMap {M N M' N' : Type*} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [AddCommMonoid M']
[AddCommMonoid N'] [Module R M'] [Module R N'] (f : M →ₗ[R] M') (g : N →ₗ[R] N') [IsLocalizedModule S f]
[IsLocalizedModule S g] : IsLocalizedModule S (f.prodMap g) :=
by
letI : Module (Localization S) M' := IsLocalizedModule.module S f
letI : Module (Localization S) N' := IsLocalizedModule.module S g
rw [isLocalizedModule_iff_isBaseChange S (Localization S)]
apply IsBaseChange.prodMap
· rw [← isLocalizedModule_iff_isBaseChange S]
infer_instance
· rw [← isLocalizedModule_iff_isBaseChange S]
infer_instance
