Base change properties #
This file proves that several constructions in linear algebra
commute with base change, as expressed by IsBaseChange.
IsBaseChange.prodMap,IsBaseChange.pi: binary and finite products.
In particular, localization of modules commutes with binary and finite products.
IsBaseChange.directSum: base change for direct sumsHomomorphism modules
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.
theorem
IsBaseChange.finitePow
{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}
[AddCommMonoid M]
[AddCommMonoid M']
[Module R M]
[Module R M']
[Module S M']
[IsScalarTower R S M']
{f : M →ₗ[R] M'}
(hf : IsBaseChange S f)
:
IsBaseChange S (f.compLeft ι)
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.
theorem
IsBaseChange.directSum
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[CommSemiring S]
[Algebra R S]
{ι : Type u_3}
{N : ι → Type u_4}
[(i : ι) → AddCommMonoid (N i)]
[(i : ι) → Module R (N i)]
{P : ι → Type u_5}
[(i : ι) → AddCommMonoid (P i)]
[(i : ι) → Module R (P i)]
[(i : ι) → Module S (P i)]
[∀ (i : ι), IsScalarTower R S (P i)]
{ε : (i : ι) → N i →ₗ[R] P i}
(ibc : ∀ (i : ι), IsBaseChange S (ε i))
:
IsBaseChange S (DirectSum.lmap ε)
Base change for direct sums.
theorem
IsBaseChange.directSumPow
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[CommSemiring S]
[Algebra R S]
(ι : Type u_3)
{M : Type u_6}
{M' : Type u_7}
[AddCommMonoid M]
[AddCommMonoid M']
[Module R M]
[Module R M']
[Module S M']
[IsScalarTower R S M']
{ε : M →ₗ[R] M'}
(ibc : IsBaseChange S ε)
:
IsBaseChange S (DirectSum.lmap fun (x : ι) => ε)
Base change for direct sums of a constant module.
theorem
IsBaseChange.finsuppPow
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[CommSemiring S]
[Algebra R S]
(ι : Type u_3)
{M : Type u_6}
{M' : Type u_7}
[AddCommMonoid M]
[AddCommMonoid M']
[Module R M]
[Module R M']
[Module S M']
[IsScalarTower R S M']
{ε : M →ₗ[R] M'}
(ibc : IsBaseChange S ε)
: