Base change commutes with finite products #
In particular, localization of modules commutes with finite products. We also show the binary product versions.
theorem
IsBaseChange.prodMap
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[CommSemiring S]
[Algebra R S]
{M : Type u_3}
{N : Type u_4}
{M' : Type u_5}
{N' : Type u_6}
[AddCommMonoid M]
[AddCommMonoid N]
[Module R M]
[Module R N]
[AddCommMonoid M']
[AddCommMonoid N']
[Module R M']
[Module R N']
[Module S M']
[Module S N']
[IsScalarTower R S M']
[IsScalarTower R S N']
(f : M →ₗ[R] M')
(g : N →ₗ[R] N')
(hf : IsBaseChange S f)
(hg : IsBaseChange S g)
:
IsBaseChange S (f.prodMap g)
Base change commutes with binary products.
theorem
IsBaseChange.pi
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[CommSemiring S]
[Algebra R S]
{ι : Type u_3}
[Finite ι]
{M : ι → Type u_4}
{M' : ι → Type u_5}
[(i : ι) → AddCommMonoid (M i)]
[(i : ι) → AddCommMonoid (M' i)]
[(i : ι) → Module R (M i)]
[(i : ι) → Module R (M' i)]
[(i : ι) → Module S (M' i)]
[∀ (i : ι), IsScalarTower R S (M' i)]
(f : (i : ι) → M i →ₗ[R] M' i)
(hf : ∀ (i : ι), IsBaseChange S (f i))
:
IsBaseChange S (LinearMap.pi fun (i : ι) => f i ∘ₗ LinearMap.proj i)
Base change commutes with finite products.
instance
IsLocalizedModule.prodMap
{R : Type u_1}
[CommSemiring R]
(S : Submonoid R)
{M : Type u_3}
{N : Type u_4}
{M' : Type u_5}
{N' : Type u_6}
[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)
Localization of modules commutes with binary products.
instance
IsLocalizedModule.pi
{R : Type u_1}
[CommSemiring R]
(S : Submonoid R)
{ι : Type u_3}
[Finite ι]
{M : ι → Type u_4}
{M' : ι → Type u_5}
[(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 (LinearMap.pi fun (i : ι) => f i ∘ₗ LinearMap.proj i)
Localization of modules commutes with finite products.