Theorems · Theorem · commutative algebra

IsBaseChange.directSum

∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {ι : Type u_3}
  {N : ι → Type u_4} [inst_3 : (i : ι) → AddCommMonoid (N i)] [inst_4 : (i : ι) → Module R (N i)] {P : ι → Type u_5}
  [inst_5 : (i : ι) → AddCommMonoid (P i)] [inst_6 : (i : ι) → Module R (P i)] [inst_7 : (i : ι) → Module S (P i)]
  [inst_8 : ∀ (i : ι), IsScalarTower R S (P i)] {ε : (i : ι) → N i →ₗ[R] P i},
  (∀ (i : ι), IsBaseChange S (ε i)) → IsBaseChange S (DirectSum.lmap ε)

Base change for direct sums.

Defined in

Mathlib.RingTheory.TensorProduct.IsBaseChangePi

Cited by

2 results in Mathlib

Foundations

Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringCommSemiringAlgebraAddCommMonoidModuleAddCommMonoidModuleModuleIsScalarTower