Theorems · Theorem · commutative algebra

DirectedSystem.lTensor

∀ (R : Type u) (M : Type u_1) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_3}
  [inst_3 : Preorder ι] {F : ι → Type u_4} [inst_4 : (i : ι) → AddCommMonoid (F i)] [inst_5 : (i : ι) → Module R (F i)]
  {f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j},
  (DirectedSystem F fun x x_1 h => ⇑(f h)) →
    DirectedSystem (fun i => TensorProduct R M (F i)) fun x x_1 h => ⇑(LinearMap.lTensor M (f h))

Given a directed system of R-modules, tensoring it on the left gives a directed system

Defined in

Mathlib.RingTheory.TensorProduct.DirectLimitFG

Cited by

1 results in Mathlib

Foundations

Depth 71 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringAddCommMonoidModulePreorderAddCommMonoidModule