Localization of modules commutes with direct sums #
If each fᵢ : Mᵢ →ₗ[R] M'ᵢ is a localization of modules at a submonoid S of R, then so is
the componentwise map ⨁ i, Mᵢ →ₗ[R] ⨁ i, M'ᵢ, for an arbitrary index type. This is the
direct-sum counterpart of Mathlib's IsLocalizedModule.prodMap and IsLocalizedModule.pi.
instance
IsLocalizedModule.directSum
{R : Type u_1}
[CommSemiring R]
(S : Submonoid R)
{ι : Type u_2}
{M : ι → Type u_3}
{M' : ι → Type u_4}
[(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)]
:
Localization of modules commutes with direct sums.