Theorems · Definition · commutative algebra

TensorProduct.toDirectLimit

{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] →
                        TensorProduct R (Module.DirectLimit G f) M →ₗ[R]
                          Module.DirectLimit (fun x => TensorProduct R (G x) M) fun i j h =>
                            LinearMap.rTensor M (f i j h)

the map (limᵢ Gᵢ) ⊗ M → limᵢ (Gᵢ ⊗ M) from the bilinear map limᵢ Gᵢ → M → limᵢ (Gᵢ ⊗ M) given by the family of maps Gᵢ → M → limᵢ (Gᵢ ⊗ M) where 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