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 ε) :