Documentation

Mathlib.LinearAlgebra.TensorPower

Tensor power of a semimodule over a commutative semiring #

We define the nth tensor power of M as the n-ary tensor product indexed by Fin n of M, ⨂[R] (i : Fin n), M. This is a special case of PiTensorProduct.

This file introduces the notation ⨂[R]^n M for TensorPower R n M, which in turn is an abbreviation for ⨂[R] i : Fin n, M.

Main definitions: #

Implementation notes #

In this file we use ₜ1 and ₜ* as local notation for the graded multiplicative structure on tensor powers. Elsewhere, using 1 and * on GradedMonoid should be preferred.

@[reducible, inline]
noncomputable abbrev TensorPower (R : Type u_1) (n : ) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] :
Type (max u_2 u_1)

Homogenous tensor powers $M^{\otimes n}$. ⨂[R]^n M is a shorthand for ⨂[R] (i : Fin n), M.

Equations
Instances For

    Homogenous tensor powers $M^{\otimes n}$. ⨂[R]^n M is a shorthand for ⨂[R] (i : Fin n), M.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem PiTensorProduct.gradedMonoid_eq_of_reindex_cast {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ιι : Type u_3} {ι : ιιType u_4} {a : GradedMonoid fun (ii : ιι) => PiTensorProduct R fun (x : ι ii) => M} {b : GradedMonoid fun (ii : ιι) => PiTensorProduct R fun (x : ι ii) => M} (h : a.fst = b.fst) :
      (PiTensorProduct.reindex R (fun (x : ι a.fst) => M) (Equiv.cast )) a.snd = b.snda = b

      Two dependent pairs of tensor products are equal if their index is equal and the contents are equal after a canonical reindexing.

      noncomputable instance TensorPower.gOne {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :
      GradedMonoid.GOne fun (i : ) => TensorPower R i M

      As a graded monoid, ⨂[R]^i M has a 1 : ⨂[R]^0 M.

      Equations
      theorem TensorPower.gOne_def {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :
      GradedMonoid.GOne.one = (PiTensorProduct.tprod R) Fin.elim0
      noncomputable def TensorPower.mulEquiv {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : } {m : } :

      A variant of PiTensorProduct.tmulEquiv with the result indexed by Fin (n + m).

      Equations
      Instances For
        noncomputable instance TensorPower.gMul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :
        GradedMonoid.GMul fun (i : ) => TensorPower R i M

        As a graded monoid, ⨂[R]^i M has a (*) : ⨂[R]^i M → ⨂[R]^j M → ⨂[R]^(i + j) M.

        Equations
        • One or more equations did not get rendered due to their size.
        theorem TensorPower.gMul_def {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {i : } {j : } (a : TensorPower R i M) (b : TensorPower R j M) :
        GradedMonoid.GMul.mul a b = TensorPower.mulEquiv (a ⊗ₜ[R] b)
        theorem TensorPower.gMul_eq_coe_linearMap {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {i : } {j : } (a : TensorPower R i M) (b : TensorPower R j M) :
        GradedMonoid.GMul.mul a b = (((TensorProduct.mk R (TensorPower R i M) (TensorPower R j M)).compr₂ TensorPower.mulEquiv) a) b
        noncomputable def TensorPower.cast (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] {i : } {j : } (h : i = j) :

        Cast between "equal" tensor powers.

        Equations
        Instances For
          theorem TensorPower.cast_tprod (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] {i : } {j : } (h : i = j) (a : Fin iM) :
          @[simp]
          theorem TensorPower.cast_refl (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] {i : } (h : i = i) :
          @[simp]
          theorem TensorPower.cast_symm (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] {i : } {j : } (h : i = j) :
          (TensorPower.cast R M h).symm = TensorPower.cast R M
          @[simp]
          theorem TensorPower.cast_trans (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] {i : } {j : } {k : } (h : i = j) (h' : j = k) :
          TensorPower.cast R M h ≪≫ₗ TensorPower.cast R M h' = TensorPower.cast R M
          @[simp]
          theorem TensorPower.cast_cast {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {i : } {j : } {k : } (h : i = j) (h' : j = k) (a : TensorPower R i M) :
          (TensorPower.cast R M h') ((TensorPower.cast R M h) a) = (TensorPower.cast R M ) a
          theorem TensorPower.gradedMonoid_eq_of_cast {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {a : GradedMonoid fun (n : ) => PiTensorProduct R fun (x : Fin n) => M} {b : GradedMonoid fun (n : ) => PiTensorProduct R fun (x : Fin n) => M} (h : a.fst = b.fst) (h2 : (TensorPower.cast R M h) a.snd = b.snd) :
          a = b
          theorem TensorPower.cast_eq_cast {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {i : } {j : } (h : i = j) :
          (TensorPower.cast R M h) = cast
          theorem TensorPower.tprod_mul_tprod (R : Type u_1) {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {na : } {nb : } (a : Fin naM) (b : Fin nbM) :
          theorem TensorPower.one_mul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : } (a : TensorPower R n M) :
          (TensorPower.cast R M ) (GradedMonoid.GMul.mul GradedMonoid.GOne.one a) = a
          theorem TensorPower.mul_one {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : } (a : TensorPower R n M) :
          (TensorPower.cast R M ) (GradedMonoid.GMul.mul a GradedMonoid.GOne.one) = a
          theorem TensorPower.mul_assoc {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {na : } {nb : } {nc : } (a : TensorPower R na M) (b : TensorPower R nb M) (c : TensorPower R nc M) :
          noncomputable instance TensorPower.gmonoid {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :
          Equations
          • TensorPower.gmonoid = let __src := TensorPower.gMul; let __src_1 := TensorPower.gOne; GradedMonoid.GMonoid.mk GradedMonoid.GMonoid.gnpowRec
          noncomputable def TensorPower.algebraMap₀ {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :

          The canonical map from R to ⨂[R]^0 M corresponding to the algebraMap of the tensor algebra.

          Equations
          Instances For
            theorem TensorPower.algebraMap₀_eq_smul_one {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (r : R) :
            TensorPower.algebraMap₀ r = r GradedMonoid.GOne.one
            theorem TensorPower.algebraMap₀_one {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :
            TensorPower.algebraMap₀ 1 = GradedMonoid.GOne.one
            theorem TensorPower.algebraMap₀_mul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : } (r : R) (a : TensorPower R n M) :
            (TensorPower.cast R M ) (GradedMonoid.GMul.mul (TensorPower.algebraMap₀ r) a) = r a
            theorem TensorPower.mul_algebraMap₀ {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : } (r : R) (a : TensorPower R n M) :
            (TensorPower.cast R M ) (GradedMonoid.GMul.mul a (TensorPower.algebraMap₀ r)) = r a
            theorem TensorPower.algebraMap₀_mul_algebraMap₀ {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (r : R) (s : R) :
            (TensorPower.cast R M ) (GradedMonoid.GMul.mul (TensorPower.algebraMap₀ r) (TensorPower.algebraMap₀ s)) = TensorPower.algebraMap₀ (r * s)
            noncomputable instance TensorPower.gsemiring {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :
            Equations
            • TensorPower.gsemiring = let __src := TensorPower.gmonoid; DirectSum.GSemiring.mk GradedMonoid.GMonoid.gnpow (fun (n : ) => TensorPower.algebraMap₀ n)
            noncomputable instance TensorPower.galgebra {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :
            DirectSum.GAlgebra R fun (i : ) => TensorPower R i M

            The tensor powers form a graded algebra.

            Note that this instance implies Algebra R (⨁ n : ℕ, ⨂[R]^n M) via DirectSum.Algebra.

            Equations
            • TensorPower.galgebra = { toFun := (TensorPower.algebraMap₀).toAddMonoidHom, map_one := , map_mul := , commutes := , smul_def := }
            theorem TensorPower.galgebra_toFun_def {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (r : R) :
            DirectSum.GAlgebra.toFun r = TensorPower.algebraMap₀ r