Theorems · Theorem · commutative algebra

IsBaseChange.comp

∀ {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] {T : Type u_4} {O : Type u_5} [inst_9 : CommSemiring T]
  [inst_10 : Algebra R T] [inst_11 : Algebra S T] [IsScalarTower R S T] [inst_13 : AddCommMonoid O]
  [inst_14 : Module R O] [inst_15 : Module S O] [inst_16 : Module T O] [inst_17 : IsScalarTower S T O]
  [inst_18 : IsScalarTower R S O] [inst_19 : IsScalarTower R T O] {f : M →ₗ[R] N},
  IsBaseChange S f → ∀ {g : N →ₗ[S] O}, IsBaseChange T g → IsBaseChange T (↑R g ∘ₗ f)

Defined in

Mathlib.RingTheory.IsTensorProduct

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommMonoidAddCommMonoidCommSemiringCommSemiringAlgebraModuleModuleModuleIsScalarTowerCommSemiringAlgebraAlgebraIsScalarTowerAddCommMonoidModuleModuleModuleIsScalarTowerIsScalarTowerIsScalarTower