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:

• TensorProduct.directLimitLeft : DirectLimit G f ⊗[R] M ≃ₗ[R] DirectLimit (G · ⊗[R] M) (f ▷ M)
• TensorProduct.directLimitRight : M ⊗[R] DirectLimit G f ≃ₗ[R] DirectLimit (M ⊗[R] G ·) (M ◁ f)

noncomputable def TensorProduct.fromDirectLimit {R : Type u_1} [CommSemiring R] {ι : Type u_2} [DecidableEq ι] [Preorder ι] {G : ι → Type u_3} [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) (M : Type u_4) [AddCommMonoid 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.

@[simp]

theorem TensorProduct.fromDirectLimit_of_tmul {R : Type u_1} [CommSemiring R] {ι : Type u_2} [DecidableEq ι] [Preorder ι] {G : ι → Type u_3} [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) {M : Type u_4} [AddCommMonoid M] [Module R M] {i : ι} (g : G i) (m : M) : (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} [CommSemiring R] {ι : Type u_2} [DecidableEq ι] [Preorder ι] {G : ι → Type u_3} [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) (M : Type u_4) [AddCommMonoid 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.

@[simp]

theorem TensorProduct.toDirectLimit_tmul_of {R : Type u_1} [CommSemiring R] {ι : Type u_2} [DecidableEq ι] [Preorder ι] {G : ι → Type u_3} [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) {M : Type u_4} [AddCommMonoid M] [Module R M] {i : ι} (g : G i) (m : M) : (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} [CommSemiring R] {ι : Type u_2} [DecidableEq ι] [Preorder ι] {G : ι → Type u_3} [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) (M : Type u_4) [AddCommMonoid 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)

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

Equations

• TensorProduct.directLimitLeft f M = LinearEquiv.ofLinear (TensorProduct.toDirectLimit f M) (TensorProduct.fromDirectLimit f M) ⋯ ⋯

@[simp]

theorem TensorProduct.directLimitLeft_tmul_of {R : Type u_1} [CommSemiring R] {ι : Type u_2} [DecidableEq ι] [Preorder ι] {G : ι → Type u_3} [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) (M : Type u_4) [AddCommMonoid M] [Module R M] {i : ι} (g : G i) (m : M) : (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} [CommSemiring R] {ι : Type u_2} [DecidableEq ι] [Preorder ι] {G : ι → Type u_3} [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) (M : Type u_4) [AddCommMonoid M] [Module R M] {i : ι} (g : G i) (m : M) : (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

theorem TensorProduct.directLimitLeft_rTensor_of {R : Type u_1} [CommSemiring R] {ι : Type u_2} [DecidableEq ι] [Preorder ι] {G : ι → Type u_3} [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) (M : Type u_4) [AddCommMonoid M] [Module R M] {i : ι} (x : TensorProduct R (G i) M) : (directLimitLeft f M) ((LinearMap.rTensor M (Module.DirectLimit.of R ι G f i)) x) = (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) x

noncomputable def TensorProduct.directLimitRight {R : Type u_1} [CommSemiring R] {ι : Type u_2} [DecidableEq ι] [Preorder ι] {G : ι → Type u_3} [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) (M : Type u_4) [AddCommMonoid M] [Module R M] : 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.

@[simp]

theorem TensorProduct.directLimitRight_tmul_of {R : Type u_1} [CommSemiring R] {ι : Type u_2} [DecidableEq ι] [Preorder ι] {G : ι → Type u_3} [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) (M : Type u_4) [AddCommMonoid M] [Module R M] {i : ι} (m : M) (g : G i) : (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} [CommSemiring R] {ι : Type u_2} [DecidableEq ι] [Preorder ι] {G : ι → Type u_3} [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) (M : Type u_4) [AddCommMonoid M] [Module R M] {i : ι} (m : M) (g : G i) : (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

instance TensorProduct.instDirectedSystemCoeLinearMapIdRTensor {R : Type u_1} [CommSemiring R] {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) (M : Type u_4) [AddCommMonoid M] [Module R M] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] : DirectedSystem (fun (x : ι) => TensorProduct R (G x) M) fun (i j : ι) (h : i ≤ j) => ⇑(LinearMap.rTensor M (f i j h))

instance TensorProduct.instDirectedSystemCoeLinearMapIdLTensor {R : Type u_1} [CommSemiring R] {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) (M : Type u_4) [AddCommMonoid M] [Module R M] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] : DirectedSystem (fun (x : ι) => TensorProduct R M (G x)) fun (i j : ι) (h : i ≤ j) => ⇑(LinearMap.lTensor M (f i j h))