Results on finitely supported functions.

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

def finsuppTensorFinsupp (R : Type u_1) (M : Type u_2) (N : Type u_3) (ι : Type u_4) (κ : Type u_5) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid 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) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (i : ι) (m : M) (k : κ) (n : N) : (finsuppTensorFinsupp R M N ι κ) (Finsupp.single i m ⊗ₜ[R] Finsupp.single k n) = Finsupp.single (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) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid 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) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (i : ι × κ) (m : M) (n : N) : (LinearEquiv.symm (finsuppTensorFinsupp R M N ι κ)) (Finsupp.single i (m ⊗ₜ[R] n)) = Finsupp.single i.1 m ⊗ₜ[R] Finsupp.single i.2 n

def finsuppTensorFinsuppLid (R : Type u_1) (N : Type u_3) (ι : Type u_4) (κ : Type u_5) [CommSemiring R] [AddCommMonoid N] [Module R N] : TensorProduct R (ι →₀ R) (κ →₀ N) ≃ₗ[R] ι × κ →₀ N

A variant of finsuppTensorFinsupp where the first module is the ground ring.

Equations

• finsuppTensorFinsuppLid R N ι κ = LinearEquiv.trans (finsuppTensorFinsupp R R N ι κ) (Finsupp.lcongr (Equiv.refl (ι × κ)) (TensorProduct.lid R N))

@[simp]

theorem finsuppTensorFinsuppLid_apply_apply (R : Type u_1) (N : Type u_3) (ι : Type u_4) (κ : Type u_5) [CommSemiring R] [AddCommMonoid N] [Module R N] (f : ι →₀ R) (g : κ →₀ N) (a : ι) (b : κ) : ((finsuppTensorFinsuppLid R N ι κ) (f ⊗ₜ[R] g)) (a, b) = f a • g b

@[simp]

theorem finsuppTensorFinsuppLid_single_tmul_single (R : Type u_1) (N : Type u_3) (ι : Type u_4) (κ : Type u_5) [CommSemiring R] [AddCommMonoid N] [Module R N] (a : ι) (b : κ) (r : R) (n : N) : (finsuppTensorFinsuppLid R N ι κ) (Finsupp.single a r ⊗ₜ[R] Finsupp.single b n) = Finsupp.single (a, b) (r • n)

@[simp]

theorem finsuppTensorFinsuppLid_symm_single_smul (R : Type u_1) (N : Type u_3) (ι : Type u_4) (κ : Type u_5) [CommSemiring R] [AddCommMonoid N] [Module R N] (i : ι × κ) (r : R) (n : N) : (LinearEquiv.symm (finsuppTensorFinsuppLid R N ι κ)) (Finsupp.single i (r • n)) = Finsupp.single i.1 r ⊗ₜ[R] Finsupp.single i.2 n

def finsuppTensorFinsuppRid (R : Type u_1) (M : Type u_2) (ι : Type u_4) (κ : Type u_5) [CommSemiring R] [AddCommMonoid M] [Module R M] : TensorProduct R (ι →₀ M) (κ →₀ R) ≃ₗ[R] ι × κ →₀ M

A variant of finsuppTensorFinsupp where the second module is the ground ring.

Equations

• finsuppTensorFinsuppRid R M ι κ = LinearEquiv.trans (finsuppTensorFinsupp R M R ι κ) (Finsupp.lcongr (Equiv.refl (ι × κ)) (TensorProduct.rid R M))

@[simp]

theorem finsuppTensorFinsuppRid_apply_apply (R : Type u_1) (M : Type u_2) (ι : Type u_4) (κ : Type u_5) [CommSemiring R] [AddCommMonoid M] [Module R M] (f : ι →₀ M) (g : κ →₀ R) (a : ι) (b : κ) : ((finsuppTensorFinsuppRid R M ι κ) (f ⊗ₜ[R] g)) (a, b) = g b • f a

@[simp]

theorem finsuppTensorFinsuppRid_single_tmul_single (R : Type u_1) (M : Type u_2) (ι : Type u_4) (κ : Type u_5) [CommSemiring R] [AddCommMonoid M] [Module R M] (a : ι) (b : κ) (m : M) (r : R) : (finsuppTensorFinsuppRid R M ι κ) (Finsupp.single a m ⊗ₜ[R] Finsupp.single b r) = Finsupp.single (a, b) (r • m)

@[simp]

theorem finsuppTensorFinsuppRid_symm_single_smul (R : Type u_1) (M : Type u_2) (ι : Type u_4) (κ : Type u_5) [CommSemiring R] [AddCommMonoid M] [Module R M] (i : ι × κ) (m : M) (r : R) : (LinearEquiv.symm (finsuppTensorFinsuppRid R M ι κ)) (Finsupp.single i (r • m)) = Finsupp.single i.1 m ⊗ₜ[R] Finsupp.single i.2 r

def finsuppTensorFinsupp' (R : Type u_1) (ι : Type u_4) (κ : Type u_5) [CommSemiring R] : TensorProduct R (ι →₀ R) (κ →₀ R) ≃ₗ[R] ι × κ →₀ R

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

Equations

• finsuppTensorFinsupp' R ι κ = finsuppTensorFinsuppLid R R ι κ

@[simp]

theorem finsuppTensorFinsupp'_apply_apply (R : Type u_1) (ι : Type u_4) (κ : Type u_5) [CommSemiring R] (f : ι →₀ R) (g : κ →₀ R) (a : ι) (b : κ) : ((finsuppTensorFinsupp' R ι κ) (f ⊗ₜ[R] g)) (a, b) = f a * g b

@[simp]

theorem finsuppTensorFinsupp'_single_tmul_single (R : Type u_1) (ι : Type u_4) (κ : Type u_5) [CommSemiring R] (a : ι) (b : κ) (r₁ : R) (r₂ : R) : (finsuppTensorFinsupp' R ι κ) (Finsupp.single a r₁ ⊗ₜ[R] Finsupp.single b r₂) = Finsupp.single (a, b) (r₁ * r₂)

theorem finsuppTensorFinsupp'_symm_single_mul (R : Type u_1) (ι : Type u_4) (κ : Type u_5) [CommSemiring R] (i : ι × κ) (r₁ : R) (r₂ : R) : (LinearEquiv.symm (finsuppTensorFinsupp' R ι κ)) (Finsupp.single i (r₁ * r₂)) = Finsupp.single i.1 r₁ ⊗ₜ[R] Finsupp.single i.2 r₂

theorem finsuppTensorFinsupp'_symm_single_eq_single_one_tmul (R : Type u_1) (ι : Type u_4) (κ : Type u_5) [CommSemiring R] (i : ι × κ) (r : R) : (LinearEquiv.symm (finsuppTensorFinsupp' R ι κ)) (Finsupp.single i r) = Finsupp.single i.1 1 ⊗ₜ[R] Finsupp.single i.2 r

theorem finsuppTensorFinsupp'_symm_single_eq_tmul_single_one (R : Type u_1) (ι : Type u_4) (κ : Type u_5) [CommSemiring R] (i : ι × κ) (r : R) : (LinearEquiv.symm (finsuppTensorFinsupp' R ι κ)) (Finsupp.single i r) = Finsupp.single i.1 r ⊗ₜ[R] Finsupp.single i.2 1

theorem finsuppTensorFinsuppLid_self (R : Type u_1) (ι : Type u_4) (κ : Type u_5) [CommSemiring R] : finsuppTensorFinsuppLid R R ι κ = finsuppTensorFinsupp' R ι κ

theorem finsuppTensorFinsuppRid_self (R : Type u_1) (ι : Type u_4) (κ : Type u_5) [CommSemiring R] : finsuppTensorFinsuppRid R R ι κ = finsuppTensorFinsupp' R ι κ