English
Localization commutes with finite products: the pi-construction for families of localized modules is itself localized.
Русский
Локализация сохраняется при конечном произведении: конструкция pi для семей локализованных модулей сохраняется локализацией.
LaTeX
$$$IsLocalizedModule\\; S\\; (.pi f_i)$$$
Lean4
/-- Localization of modules commutes with finite products. -/
instance pi {ι : Type*} [Finite ι] {M M' : ι → Type*} [∀ i, AddCommMonoid (M i)] [∀ i, AddCommMonoid (M' i)]
[∀ i, Module R (M i)] [∀ i, Module R (M' i)] (f : ∀ i, M i →ₗ[R] M' i) [∀ i, IsLocalizedModule S (f i)] :
IsLocalizedModule S (.pi fun i ↦ f i ∘ₗ .proj i) :=
by
letI (i : ι) : Module (Localization S) (M' i) := IsLocalizedModule.module S (f i)
rw [isLocalizedModule_iff_isBaseChange S (Localization S)]
apply IsBaseChange.pi
intro i
rw [← isLocalizedModule_iff_isBaseChange S]
infer_instance
