Theorems · Definition · commutative algebra

TensorProduct.fromDirectLimit

{R : Type u_1} →
  [inst : CommSemiring R] →
    {ι : Type u_2} →
      [inst_1 : DecidableEq ι] →
        [inst_2 : Preorder ι] →
          {G : ι → Type u_3} →
            [inst_3 : (i : ι) → AddCommMonoid (G i)] →
              [inst_4 : (i : ι) → Module R (G i)] →
                (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) →
                  (M : Type u_4) →
                    [inst_5 : AddCommMonoid M] →
                      [inst_6 : Module R M] →
                        (Module.DirectLimit (fun x => TensorProduct R (G x) M) fun i j h =>
                            LinearMap.rTensor M (f i j h)) →ₗ[R]
                          TensorProduct R (Module.DirectLimit G f) M

the map limᵢ (Gᵢ ⊗ M) → (limᵢ Gᵢ) ⊗ M induced by the family of maps Gᵢ ⊗ M → (limᵢ Gᵢ) ⊗ M given by gᵢ ⊗ m ↦ [gᵢ] ⊗ m.

Defined in

Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringDecidableEqPreorderAddCommMonoidModuleAddCommMonoidModule