Documentation

Mathlib.LinearAlgebra.DirectSum.Finsupp

Results on finitely supported functions. #

Case of MvPolynomial #

These functions apply to MvPolynomial, one can define

noncomputable def MvPolynomial.rTensor' :
    MvPolynomial σ S ⊗[R] N ≃ₗ[S] (σ →₀ ℕ) →₀ (S ⊗[R] N) :=
  TensorProduct.finsuppLeft'

noncomputable def MvPolynomial.rTensor :
    MvPolynomial σ R ⊗[R] N ≃ₗ[R] (σ →₀ ℕ) →₀ N :=
  TensorProduct.finsuppScalarLeft

However, to be actually usable, these definitions need lemmas to be given in companion PR.

Case of Polynomial #

Polynomial is a structure containing a Finsupp, so these functions can't be applied directly to Polynomial.

Some linear equivs need to be added to mathlib for that. This belongs to a companion PR.

TODO #

noncomputable def TensorProduct.finsuppLeft (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (N : Type u_3) [AddCommMonoid N] [Module R N] (ι : Type u_4) [DecidableEq ι] :

The tensor product of ι →₀ M and N is linearly equivalent to ι →₀ M ⊗[R] N

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem TensorProduct.finsuppLeft_apply_tmul {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (p : ι →₀ M) (n : N) :
    (TensorProduct.finsuppLeft R M N ι) (p ⊗ₜ[R] n) = p.sum fun (i : ι) (m : M) => Finsupp.single i (m ⊗ₜ[R] n)
    @[simp]
    theorem TensorProduct.finsuppLeft_apply_tmul_apply {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (p : ι →₀ M) (n : N) (i : ι) :
    ((TensorProduct.finsuppLeft R M N ι) (p ⊗ₜ[R] n)) i = p i ⊗ₜ[R] n
    theorem TensorProduct.finsuppLeft_apply {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (t : TensorProduct R (ι →₀ M) N) (i : ι) :
    @[simp]
    theorem TensorProduct.finsuppLeft_symm_apply_single {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (i : ι) (m : M) (n : N) :
    noncomputable def TensorProduct.finsuppRight (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (N : Type u_3) [AddCommMonoid N] [Module R N] (ι : Type u_4) [DecidableEq ι] :

    The tensor product of M and ι →₀ N is linearly equivalent to ι →₀ M ⊗[R] N

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem TensorProduct.finsuppRight_apply_tmul {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (m : M) (p : ι →₀ N) :
      (TensorProduct.finsuppRight R M N ι) (m ⊗ₜ[R] p) = p.sum fun (i : ι) (n : N) => Finsupp.single i (m ⊗ₜ[R] n)
      @[simp]
      theorem TensorProduct.finsuppRight_apply_tmul_apply {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (m : M) (p : ι →₀ N) (i : ι) :
      ((TensorProduct.finsuppRight R M N ι) (m ⊗ₜ[R] p)) i = m ⊗ₜ[R] p i
      theorem TensorProduct.finsuppRight_apply {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (t : TensorProduct R M (ι →₀ N)) (i : ι) :
      @[simp]
      theorem TensorProduct.finsuppRight_symm_apply_single {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (i : ι) (m : M) (n : N) :
      theorem TensorProduct.finsuppLeft_smul' {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] {S : Type u_5} [CommSemiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] (s : S) (t : TensorProduct R (ι →₀ M) N) :
      noncomputable def TensorProduct.finsuppLeft' (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (N : Type u_3) [AddCommMonoid N] [Module R N] (ι : Type u_4) [DecidableEq ι] (S : Type u_5) [CommSemiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] :

      When M is also an S-module, then TensorProduct.finsuppLeft R M N`` is an S`-linear equiv

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem TensorProduct.finsuppLeft'_apply {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] {S : Type u_5} [CommSemiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] (x : TensorProduct R (ι →₀ M) N) :
        noncomputable def TensorProduct.finsuppScalarLeft (R : Type u_1) [CommSemiring R] (N : Type u_3) [AddCommMonoid N] [Module R N] (ι : Type u_4) [DecidableEq ι] :

        The tensor product of ι →₀ R and N is linearly equivalent to ι →₀ N

        Equations
        Instances For
          @[simp]
          theorem TensorProduct.finsuppScalarLeft_apply_tmul_apply {R : Type u_1} [CommSemiring R] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (p : ι →₀ R) (n : N) (i : ι) :
          ((TensorProduct.finsuppScalarLeft R N ι) (p ⊗ₜ[R] n)) i = p i n
          theorem TensorProduct.finsuppScalarLeft_apply_tmul {R : Type u_1} [CommSemiring R] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (p : ι →₀ R) (n : N) :
          (TensorProduct.finsuppScalarLeft R N ι) (p ⊗ₜ[R] n) = p.sum fun (i : ι) (m : R) => Finsupp.single i (m n)
          theorem TensorProduct.finsuppScalarLeft_apply {R : Type u_1} [CommSemiring R] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (pn : TensorProduct R (ι →₀ R) N) (i : ι) :
          @[simp]
          theorem TensorProduct.finsuppScalarLeft_symm_apply_single {R : Type u_1} [CommSemiring R] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (i : ι) (n : N) :
          noncomputable def TensorProduct.finsuppScalarRight (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (ι : Type u_4) [DecidableEq ι] :

          The tensor product of M and ι →₀ R is linearly equivalent to ι →₀ N

          Equations
          Instances For
            @[simp]
            theorem TensorProduct.finsuppScalarRight_apply_tmul_apply {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {ι : Type u_4} [DecidableEq ι] (m : M) (p : ι →₀ R) (i : ι) :
            theorem TensorProduct.finsuppScalarRight_apply_tmul {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {ι : Type u_4} [DecidableEq ι] (m : M) (p : ι →₀ R) :
            (TensorProduct.finsuppScalarRight R M ι) (m ⊗ₜ[R] p) = p.sum fun (i : ι) (n : R) => Finsupp.single i (n m)
            theorem TensorProduct.finsuppScalarRight_apply {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {ι : Type u_4} [DecidableEq ι] (t : TensorProduct R M (ι →₀ R)) (i : ι) :
            @[simp]
            def finsuppTensorFinsupp (R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] :

            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) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] (i : ι) (m : M) (k : κ) (n : N) :
              @[simp]
              theorem finsuppTensorFinsupp_apply (R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] (f : ι →₀ M) (g : κ →₀ N) (i : ι) (k : κ) :
              ((finsuppTensorFinsupp R S M N ι κ) (f ⊗ₜ[R] g)) (i, k) = f i ⊗ₜ[R] g k
              @[simp]
              theorem finsuppTensorFinsupp_symm_single (R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] (i : ι × κ) (m : M) (n : N) :
              def finsuppTensorFinsuppLid (R : Type u_1) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [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
              Instances For
                @[simp]
                theorem finsuppTensorFinsuppLid_apply_apply (R : Type u_1) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [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_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid N] [Module R N] (a : ι) (b : κ) (r : R) (n : N) :
                @[simp]
                theorem finsuppTensorFinsuppLid_symm_single_smul (R : Type u_1) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid N] [Module R N] (i : ι × κ) (r : R) (n : N) :
                def finsuppTensorFinsuppRid (R : Type u_1) (M : Type u_3) (ι : Type u_5) (κ : Type u_6) [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
                Instances For
                  @[simp]
                  theorem finsuppTensorFinsuppRid_apply_apply (R : Type u_1) (M : Type u_3) (ι : Type u_5) (κ : Type u_6) [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_3) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] (a : ι) (b : κ) (m : M) (r : R) :
                  @[simp]
                  theorem finsuppTensorFinsuppRid_symm_single_smul (R : Type u_1) (M : Type u_3) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] (i : ι × κ) (m : M) (r : R) :
                  def finsuppTensorFinsupp' (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [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_5) (κ : Type u_6) [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_5) (κ : Type u_6) [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_5) (κ : Type u_6) [CommSemiring R] (i : ι × κ) (r₁ : R) (r₂ : R) :
                    (finsuppTensorFinsupp' R ι κ).symm (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_5) (κ : Type u_6) [CommSemiring R] (i : ι × κ) (r : R) :
                    theorem finsuppTensorFinsupp'_symm_single_eq_tmul_single_one (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] (i : ι × κ) (r : R) :
                    theorem finsuppTensorFinsuppLid_self (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] :
                    theorem finsuppTensorFinsuppRid_self (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] :