Results on finitely supported functions.

The tensor product of ι →₀ M and κ →₀ N is linearly equivalent to (ι × κ) →₀ (M ⊗ N).

noncomputable def finsuppTensorFinsupp (R : Type u_1) (M : Type u_2) (N : Type u_3) (ι : Type u_4) (κ : Type u_5) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : TensorProduct R (ι →₀ M) (κ →₀ N) ≃ₗ[R] ι × κ →₀ TensorProduct R M N

The tensor product of ι →₀ M and κ →₀ N is linearly equivalent to (ι × κ) →₀ (M ⊗ N).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem finsuppTensorFinsupp_single (R : Type u_1) (M : Type u_2) (N : Type u_3) (ι : Type u_4) (κ : Type u_5) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (i : ι) (m : M) (k : κ) (n : N) : ↑(finsuppTensorFinsupp R M N ι κ) ((fun₀ | i => m) ⊗ₜ[R] fun₀ | k => n) = fun₀ | (i, k) => m ⊗ₜ[R] n

@[simp]

theorem finsuppTensorFinsupp_apply (R : Type u_1) (M : Type u_2) (N : Type u_3) (ι : Type u_4) (κ : Type u_5) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : ι →₀ M) (g : κ →₀ N) (i : ι) (k : κ) : ↑(↑(finsuppTensorFinsupp R M N ι κ) (f ⊗ₜ[R] g)) (i, k) = ↑f i ⊗ₜ[R] ↑g k

@[simp]

theorem finsuppTensorFinsupp_symm_single (R : Type u_1) (M : Type u_2) (N : Type u_3) (ι : Type u_4) (κ : Type u_5) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (i : ι × κ) (m : M) (n : N) : (↑(LinearEquiv.symm (finsuppTensorFinsupp R M N ι κ)) fun₀ | i => m ⊗ₜ[R] n) = (fun₀ | i.fst => m) ⊗ₜ[R] fun₀ | i.snd => n

def finsuppTensorFinsupp' (S : Type u_1) [CommRing S] (α : Type u_2) (β : Type u_3) : TensorProduct S (α →₀ S) (β →₀ S) ≃ₗ[S] α × β →₀ S

A variant of finsuppTensorFinsupp where both modules are the ground ring.

Equations

• finsuppTensorFinsupp' S α β = LinearEquiv.trans (finsuppTensorFinsupp S S S α β) (Finsupp.lcongr (Equiv.refl (α × β)) (TensorProduct.lid S S))

@[simp]

theorem finsuppTensorFinsupp'_apply_apply (S : Type u_1) [CommRing S] (α : Type u_2) (β : Type u_3) (f : α →₀ S) (g : β →₀ S) (a : α) (b : β) : ↑(↑(finsuppTensorFinsupp' S α β) (f ⊗ₜ[S] g)) (a, b) = ↑f a * ↑g b

@[simp]

theorem finsuppTensorFinsupp'_single_tmul_single (S : Type u_1) [CommRing S] (α : Type u_2) (β : Type u_3) (a : α) (b : β) (r₁ : S) (r₂ : S) : ↑(finsuppTensorFinsupp' S α β) ((fun₀ | a => r₁) ⊗ₜ[S] fun₀ | b => r₂) = fun₀ | (a, b) => r₁ * r₂