Documentation

Mathlib.LinearAlgebra.DirectSum.Finsupp

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] :

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.
Instances For
    @[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) :
    @[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) :
    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
    Instances For
      @[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₂)