HepLean Documentation

Mathlib.LinearAlgebra.TensorProduct.Basis

Bases and dimensionality of tensor products of modules #

These can not go into LinearAlgebra.TensorProduct since they depend on LinearAlgebra.FinsuppVectorSpace which in turn imports LinearAlgebra.TensorProduct.

source
def Basis.tensorProduct {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] (b : Basis ι S M) (c : Basis κ R N) :
Basis (ι × κ) S (TensorProduct R M N)

If b : ι → M and c : κ → N are bases then so is fun i ↦ b i.1 ⊗ₜ c i.2 : ι × κ → M ⊗ N.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Basis.tensorProduct_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] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] (b : Basis ι S M) (c : Basis κ R N) (i : ι) (j : κ) :
    (b.tensorProduct c) (i, j) = b i ⊗ₜ[R] c j
    source
    theorem Basis.tensorProduct_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] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] (b : Basis ι S M) (c : Basis κ R N) (i : ι × κ) :
    (b.tensorProduct c) i = b i.1 ⊗ₜ[R] c i.2
    source
    @[simp]
    theorem Basis.tensorProduct_repr_tmul_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] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] (b : Basis ι S M) (c : Basis κ R N) (m : M) (n : N) (i : ι) (j : κ) :
    ((b.tensorProduct c).repr (m ⊗ₜ[R] n)) (i, j) = (c.repr n) j • (b.repr m) i
    source
    noncomputable def Basis.baseChange {R : Type u_1} {M : Type u_3} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_7) [Semiring S] [Algebra R S] (b : Basis ι R M) :
    Basis ι S (TensorProduct R S M)

    The lift of an R-basis of M to an S-basis of the base change S ⊗[R] M.

    Equations
    Instances For
      source
      @[simp]
      theorem Basis.baseChange_repr_tmul {R : Type u_1} {M : Type u_3} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_7) [Semiring S] [Algebra R S] (b : Basis ι R M) (x : S) (y : M) (i : ι) :
      ((Basis.baseChange S b).repr (x ⊗ₜ[R] y)) i = (b.repr y) i • x
      source
      @[simp]
      theorem Basis.baseChange_apply {R : Type u_1} {M : Type u_3} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_7) [Semiring S] [Algebra R S] (b : Basis ι R M) (i : ι) :
      (Basis.baseChange S b) i = 1 ⊗ₜ[R] b i
      source
      def TensorProduct.equivFinsuppOfBasisRight {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq κ] (𝒞 : Basis κ R N) :
      TensorProduct R M N ≃ₗ[R] κ →₀ M

      If {𝒞ᵢ} is a basis for the module N, then every elements of x ∈ M ⊗ N can be uniquely written as ∑ᵢ mᵢ ⊗ 𝒞ᵢ for some mᵢ ∈ M.

      Equations
      Instances For
        source
        @[simp]
        theorem TensorProduct.equivFinsuppOfBasisRight_apply_tmul {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq κ] (𝒞 : Basis κ R N) (m : M) (n : N) :
        (TensorProduct.equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ[R] n) = Finsupp.mapRange (fun (x : R) => x • m) ⋯ (𝒞.repr n)
        source
        theorem TensorProduct.equivFinsuppOfBasisRight_apply_tmul_apply {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq κ] (𝒞 : Basis κ R N) (m : M) (n : N) (i : κ) :
        ((TensorProduct.equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ[R] n)) i = (𝒞.repr n) i • m
        source
        theorem TensorProduct.equivFinsuppOfBasisRight_symm {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq κ] (𝒞 : Basis κ R N) :
        ↑(TensorProduct.equivFinsuppOfBasisRight 𝒞).symm = (Finsupp.lsum R) fun (i : κ) => (TensorProduct.mk R M N).flip (𝒞 i)
        source
        @[simp]
        theorem TensorProduct.equivFinsuppOfBasisRight_symm_apply {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq κ] (𝒞 : Basis κ R N) (b : κ →₀ M) :
        (TensorProduct.equivFinsuppOfBasisRight 𝒞).symm b = b.sum fun (i : κ) (m : M) => m ⊗ₜ[R] 𝒞 i
        source
        theorem TensorProduct.sum_tmul_basis_right_injective {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq κ] (𝒞 : Basis κ R N) :
        Function.Injective ⇑((Finsupp.lsum R) fun (i : κ) => (TensorProduct.mk R M N).flip (𝒞 i))
        source
        theorem TensorProduct.sum_tmul_basis_right_eq_zero {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq κ] (𝒞 : Basis κ R N) (b : κ →₀ M) (h : (b.sum fun (i : κ) (m : M) => m ⊗ₜ[R] 𝒞 i) = 0) :
        b = 0
        source
        def TensorProduct.equivFinsuppOfBasisLeft {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq ι] (ℬ : Basis ι R M) :
        TensorProduct R M N ≃ₗ[R] ι →₀ N

        If {ℬᵢ} is a basis for the module M, then every elements of x ∈ M ⊗ N can be uniquely written as ∑ᵢ ℬᵢ ⊗ nᵢ for some nᵢ ∈ N.

        Equations
        Instances For
          source
          @[simp]
          theorem TensorProduct.equivFinsuppOfBasisLeft_apply_tmul {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq ι] (ℬ : Basis ι R M) (m : M) (n : N) :
          (TensorProduct.equivFinsuppOfBasisLeft ℬ) (m ⊗ₜ[R] n) = Finsupp.mapRange (fun (x : R) => x • n) ⋯ (ℬ.repr m)
          source
          theorem TensorProduct.equivFinsuppOfBasisLeft_apply_tmul_apply {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq ι] (ℬ : Basis ι R M) (m : M) (n : N) (i : ι) :
          ((TensorProduct.equivFinsuppOfBasisLeft ℬ) (m ⊗ₜ[R] n)) i = (ℬ.repr m) i • n
          source
          theorem TensorProduct.equivFinsuppOfBasisLeft_symm {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq ι] (ℬ : Basis ι R M) :
          ↑(TensorProduct.equivFinsuppOfBasisLeft ℬ).symm = (Finsupp.lsum R) fun (i : ι) => (TensorProduct.mk R M N) (ℬ i)
          source
          @[simp]
          theorem TensorProduct.equivFinsuppOfBasisLeft_symm_apply {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq ι] (ℬ : Basis ι R M) (b : ι →₀ N) :
          (TensorProduct.equivFinsuppOfBasisLeft ℬ).symm b = b.sum fun (i : ι) (n : N) => ℬ i ⊗ₜ[R] n
          source
          theorem TensorProduct.eq_repr_basis_right {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq κ] (𝒞 : Basis κ R N) (x : TensorProduct R M N) :
          ∃ (b : κ →₀ M), (b.sum fun (i : κ) (m : M) => m ⊗ₜ[R] 𝒞 i) = x

          Elements in M ⊗ N can be represented by sum of elements in M tensor elements of basis of N.

          source
          theorem TensorProduct.eq_repr_basis_left {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq ι] (ℬ : Basis ι R M) (x : TensorProduct R M N) :
          ∃ (c : ι →₀ N), (c.sum fun (i : ι) (n : N) => ℬ i ⊗ₜ[R] n) = x

          Elements in M ⊗ N can be represented by sum of elements of basis of M tensor elements of N.

          source
          theorem TensorProduct.sum_tmul_basis_left_injective {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq ι] (ℬ : Basis ι R M) :
          Function.Injective ⇑((Finsupp.lsum R) fun (i : ι) => (TensorProduct.mk R M N) (ℬ i))
          source
          theorem TensorProduct.sum_tmul_basis_left_eq_zero {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq ι] (ℬ : Basis ι R M) (b : ι →₀ N) (h : (b.sum fun (i : ι) (n : N) => ℬ i ⊗ₜ[R] n) = 0) :
          b = 0