Documentation

Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Tensor product and direct limits commute with each other. #

Given a family of R-modules Gᵢ with a family of compatible R-linear maps fᵢⱼ : Gᵢ → Gⱼ for every i ≤ j and another R-module M, we have (limᵢ Gᵢ) ⊗ M and lim (Gᵢ ⊗ M) are isomorphic as R-modules.

Main definitions: #

noncomputable def TensorProduct.fromDirectLimit {R : Type u_1} [CommRing R] {ι : Type u_2} [DecidableEq ι] [Preorder ι] {G : ιType u_3} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) (M : Type u_4) [AddCommGroup M] [Module R M] :
(Module.DirectLimit (fun (x : ι) => TensorProduct R (G x) M) fun (i j : ι) (h : i j) => 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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem TensorProduct.fromDirectLimit_of_tmul {R : Type u_1} [CommRing R] {ι : Type u_2} [DecidableEq ι] [Preorder ι] {G : ιType u_3} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) {M : Type u_4} [AddCommGroup M] [Module R M] {i : ι} (g : G i) (m : M) :
    (TensorProduct.fromDirectLimit f M) ((Module.DirectLimit.of R ι (fun (x : ι) => TensorProduct R (G x) M) (fun (i j : ι) (h : i j) => LinearMap.rTensor M (f i j h)) i) (g ⊗ₜ[R] m)) = (Module.DirectLimit.of R ι G f i) g ⊗ₜ[R] m
    noncomputable def TensorProduct.toDirectLimit {R : Type u_1} [CommRing R] {ι : Type u_2} [DecidableEq ι] [Preorder ι] {G : ιType u_3} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) (M : Type u_4) [AddCommGroup M] [Module R M] :
    TensorProduct R (Module.DirectLimit G f) M →ₗ[R] Module.DirectLimit (fun (x : ι) => TensorProduct R (G x) M) fun (i j : ι) (h : i j) => 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]

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem TensorProduct.toDirectLimit_tmul_of {R : Type u_1} [CommRing R] {ι : Type u_2} [DecidableEq ι] [Preorder ι] {G : ιType u_3} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) {M : Type u_4} [AddCommGroup M] [Module R M] {i : ι} (g : G i) (m : M) :
      (TensorProduct.toDirectLimit f M) ((Module.DirectLimit.of R ι G f i) g ⊗ₜ[R] m) = (Module.DirectLimit.of R ι (fun (x : ι) => TensorProduct R (G x) M) (fun (i j : ι) (h : i j) => LinearMap.rTensor M (f i j h)) i) (g ⊗ₜ[R] m)
      noncomputable def TensorProduct.directLimitLeft {R : Type u_1} [CommRing R] {ι : Type u_2} [DecidableEq ι] [Preorder ι] {G : ιType u_3} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) (M : Type u_4) [AddCommGroup M] [Module R M] [IsDirected ι fun (x x_1 : ι) => x x_1] :
      TensorProduct R (Module.DirectLimit G f) M ≃ₗ[R] Module.DirectLimit (fun (x : ι) => TensorProduct R (G x) M) fun (i j : ι) (h : i j) => LinearMap.rTensor M (f i j h)

      limᵢ (Gᵢ ⊗ M) and (limᵢ Gᵢ) ⊗ M are isomorphic as modules

      Equations
      Instances For
        @[simp]
        theorem TensorProduct.directLimitLeft_tmul_of {R : Type u_1} [CommRing R] {ι : Type u_2} [DecidableEq ι] [Preorder ι] {G : ιType u_3} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) (M : Type u_4) [AddCommGroup M] [Module R M] [IsDirected ι fun (x x_1 : ι) => x x_1] {i : ι} (g : G i) (m : M) :
        (TensorProduct.directLimitLeft f M) ((Module.DirectLimit.of R ι G f i) g ⊗ₜ[R] m) = (Module.DirectLimit.of R ι (fun (i : ι) => TensorProduct R (G i) M) (fun (i j : ι) (h : i j) => LinearMap.rTensor M (f i j h)) i) (g ⊗ₜ[R] m)
        @[simp]
        theorem TensorProduct.directLimitLeft_symm_of_tmul {R : Type u_1} [CommRing R] {ι : Type u_2} [DecidableEq ι] [Preorder ι] {G : ιType u_3} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) (M : Type u_4) [AddCommGroup M] [Module R M] [IsDirected ι fun (x x_1 : ι) => x x_1] {i : ι} (g : G i) (m : M) :
        (TensorProduct.directLimitLeft f M).symm ((Module.DirectLimit.of R ι (fun (x : ι) => TensorProduct R (G x) M) (fun (i j : ι) (h : i j) => LinearMap.rTensor M (f i j h)) i) (g ⊗ₜ[R] m)) = (Module.DirectLimit.of R ι G f i) g ⊗ₜ[R] m
        noncomputable def TensorProduct.directLimitRight {R : Type u_1} [CommRing R] {ι : Type u_2} [DecidableEq ι] [Preorder ι] {G : ιType u_3} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) (M : Type u_4) [AddCommGroup M] [Module R M] [IsDirected ι fun (x x_1 : ι) => x x_1] :
        TensorProduct R M (Module.DirectLimit G f) ≃ₗ[R] Module.DirectLimit (fun (x : ι) => TensorProduct R M (G x)) fun (i j : ι) (h : i j) => LinearMap.lTensor M (f i j h)

        M ⊗ (limᵢ Gᵢ) and limᵢ (M ⊗ Gᵢ) are isomorphic as modules

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem TensorProduct.directLimitRight_tmul_of {R : Type u_1} [CommRing R] {ι : Type u_2} [DecidableEq ι] [Preorder ι] {G : ιType u_3} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) (M : Type u_4) [AddCommGroup M] [Module R M] [IsDirected ι fun (x x_1 : ι) => x x_1] {i : ι} (m : M) (g : G i) :
          (TensorProduct.directLimitRight f M) (m ⊗ₜ[R] (Module.DirectLimit.of R ι G f i) g) = (Module.DirectLimit.of R ι (fun (x : ι) => TensorProduct R M (G x)) (fun (i j : ι) (h : i j) => LinearMap.lTensor M (f i j h)) i) (m ⊗ₜ[R] g)
          @[simp]
          theorem TensorProduct.directLimitRight_symm_of_tmul {R : Type u_1} [CommRing R] {ι : Type u_2} [DecidableEq ι] [Preorder ι] {G : ιType u_3} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) (M : Type u_4) [AddCommGroup M] [Module R M] [IsDirected ι fun (x x_1 : ι) => x x_1] {i : ι} (m : M) (g : G i) :
          (TensorProduct.directLimitRight f M).symm ((Module.DirectLimit.of R ι (fun (x : ι) => TensorProduct R M (G x)) (fun (i j : ι) (h : i j) => LinearMap.lTensor M (f i j h)) i) (m ⊗ₜ[R] g)) = m ⊗ₜ[R] (Module.DirectLimit.of R ι G f i) g