Documentation

Mathlib.LinearAlgebra.TensorAlgebra.Basic

Tensor Algebras #

Given a commutative semiring R, and an R-module M, we construct the tensor algebra of M. This is the free R-algebra generated (R-linearly) by the module M.

Notation #

  1. TensorAlgebra R M is the tensor algebra itself. It is endowed with an R-algebra structure.
  2. TensorAlgebra.ι R is the canonical R-linear map M → TensorAlgebra R M.
  3. Given a linear map f : M → A to an R-algebra A, lift R f is the lift of f to an R-algebra morphism TensorAlgebra R M → A.

Theorems #

  1. ι_comp_lift states that the composition (lift R f) ∘ (ι R) is identical to f.
  2. lift_unique states that whenever an R-algebra morphism g : TensorAlgebra R M → A is given whose composition with ι R is f, then one has g = lift R f.
  3. hom_ext is a variant of lift_unique in the form of an extensionality theorem.
  4. lift_comp_ι is a combination of ι_comp_lift and lift_unique. It states that the lift of the composition of an algebra morphism with ι is the algebra morphism itself.

Implementation details #

As noted above, the tensor algebra of M is constructed as the free R-algebra generated by M, modulo the additional relations making the inclusion of M into an R-linear map.

inductive TensorAlgebra.Rel (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] :
FreeAlgebra R MFreeAlgebra R MProp

An inductively defined relation on Pre R M used to force the initial algebra structure on the associated quotient.

Instances For
    def TensorAlgebra (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] :
    Type (max u_1 u_2)

    The tensor algebra of the module M over the commutative semiring R.

    Equations
    Instances For
      instance instAlgebra {R : Type u_3} {A : Type u_4} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [CommSemiring A] [Algebra R A] [Module R M] [Module A M] [IsScalarTower R A M] :
      Equations
      theorem instSMulCommClassTensorAlgebra {R : Type u_3} {S : Type u_4} {A : Type u_5} {M : Type u_6} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [CommSemiring A] [Algebra R A] [Algebra S A] [Module R M] [Module S M] [Module A M] [IsScalarTower R A M] [IsScalarTower S A M] :
      theorem instIsScalarTowerTensorAlgebra {R : Type u_3} {S : Type u_4} {A : Type u_5} {M : Type u_6} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [CommSemiring A] [SMul R S] [Algebra R A] [Algebra S A] [Module R M] [Module S M] [Module A M] [IsScalarTower R A M] [IsScalarTower S A M] [IsScalarTower R S A] :
      theorem TensorAlgebra.ι_def (R : Type u_3) [CommSemiring R] {M : Type u_4} [AddCommMonoid M] [Module R M] :
      TensorAlgebra.ι R = { toFun := fun (m : M) => (RingQuot.mkAlgHom R (TensorAlgebra.Rel R M)) (FreeAlgebra.ι R m), map_add' := , map_smul' := }
      @[irreducible]
      def TensorAlgebra.ι (R : Type u_3) [CommSemiring R] {M : Type u_4} [AddCommMonoid M] [Module R M] :

      The canonical linear map M →ₗ[R] TensorAlgebra R M.

      Equations
      Instances For
        def TensorAlgebra.lift (R : Type u_1) [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {A : Type u_3} [Semiring A] [Algebra R A] :

        Given a linear map f : M → A where A is an R-algebra, lift R f is the unique lift of f to a morphism of R-algebras TensorAlgebra R M → A.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem TensorAlgebra.lift_symm_apply (R : Type u_1) [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {A : Type u_3} [Semiring A] [Algebra R A] (F : TensorAlgebra R M →ₐ[R] A) :
          (TensorAlgebra.lift R).symm F = F.toLinearMap ∘ₗ TensorAlgebra.ι R
          @[simp]
          theorem TensorAlgebra.ι_comp_lift {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {A : Type u_3} [Semiring A] [Algebra R A] (f : M →ₗ[R] A) :
          ((TensorAlgebra.lift R) f).toLinearMap ∘ₗ TensorAlgebra.ι R = f
          @[simp]
          theorem TensorAlgebra.lift_ι_apply {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {A : Type u_3} [Semiring A] [Algebra R A] (f : M →ₗ[R] A) (x : M) :
          @[simp]
          theorem TensorAlgebra.lift_unique {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {A : Type u_3} [Semiring A] [Algebra R A] (f : M →ₗ[R] A) (g : TensorAlgebra R M →ₐ[R] A) :
          g.toLinearMap ∘ₗ TensorAlgebra.ι R = f g = (TensorAlgebra.lift R) f
          @[simp]
          theorem TensorAlgebra.lift_comp_ι {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {A : Type u_3} [Semiring A] [Algebra R A] (g : TensorAlgebra R M →ₐ[R] A) :
          (TensorAlgebra.lift R) (g.toLinearMap ∘ₗ TensorAlgebra.ι R) = g
          theorem TensorAlgebra.hom_ext {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {A : Type u_3} [Semiring A] [Algebra R A] {f g : TensorAlgebra R M →ₐ[R] A} (w : f.toLinearMap ∘ₗ TensorAlgebra.ι R = g.toLinearMap ∘ₗ TensorAlgebra.ι R) :
          f = g

          See note [partially-applied ext lemmas].

          theorem TensorAlgebra.induction {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {C : TensorAlgebra R MProp} (algebraMap : ∀ (r : R), C ((algebraMap R (TensorAlgebra R M)) r)) (ι : ∀ (x : M), C ((TensorAlgebra.ι R) x)) (mul : ∀ (a b : TensorAlgebra R M), C aC bC (a * b)) (add : ∀ (a b : TensorAlgebra R M), C aC bC (a + b)) (a : TensorAlgebra R M) :
          C a

          If C holds for the algebraMap of r : R into TensorAlgebra R M, the ι of x : M, and is preserved under addition and multiplication, then it holds for all of TensorAlgebra R M.

          The left-inverse of algebraMap.

          Equations
          Instances For
            theorem TensorAlgebra.algebraMap_leftInverse {R : Type u_1} [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] :
            Function.LeftInverse TensorAlgebra.algebraMapInv (algebraMap R (TensorAlgebra R M))
            @[simp]
            theorem TensorAlgebra.algebraMap_inj {R : Type u_1} [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (x y : R) :
            (algebraMap R (TensorAlgebra R M)) x = (algebraMap R (TensorAlgebra R M)) y x = y
            @[simp]
            theorem TensorAlgebra.algebraMap_eq_zero_iff {R : Type u_1} [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (x : R) :
            (algebraMap R (TensorAlgebra R M)) x = 0 x = 0
            @[simp]
            theorem TensorAlgebra.algebraMap_eq_one_iff {R : Type u_1} [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (x : R) :
            (algebraMap R (TensorAlgebra R M)) x = 1 x = 1

            A TensorAlgebra over a nontrivial semiring is nontrivial.

            The canonical map from TensorAlgebra R M into TrivSqZeroExt R M that sends TensorAlgebra.ι to TrivSqZeroExt.inr.

            Equations
            Instances For
              @[simp]
              theorem TensorAlgebra.toTrivSqZeroExt_ι {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (x : M) [Module Rᵐᵒᵖ M] [IsCentralScalar R M] :
              TensorAlgebra.toTrivSqZeroExt ((TensorAlgebra.ι R) x) = TrivSqZeroExt.inr x
              def TensorAlgebra.ιInv {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] :

              The left-inverse of ι.

              As an implementation detail, we implement this using TrivSqZeroExt which has a suitable algebra structure.

              Equations
              Instances For
                theorem TensorAlgebra.ι_leftInverse {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] :
                Function.LeftInverse TensorAlgebra.ιInv (TensorAlgebra.ι R)
                @[simp]
                theorem TensorAlgebra.ι_inj (R : Type u_1) [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (x y : M) :
                @[simp]
                theorem TensorAlgebra.ι_eq_zero_iff (R : Type u_1) [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (x : M) :
                (TensorAlgebra.ι R) x = 0 x = 0
                @[simp]
                theorem TensorAlgebra.ι_eq_algebraMap_iff {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (x : M) (r : R) :
                (TensorAlgebra.ι R) x = (algebraMap R (TensorAlgebra R M)) r x = 0 r = 0
                @[simp]
                theorem TensorAlgebra.ι_ne_one {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] [Nontrivial R] (x : M) :

                The generators of the tensor algebra are disjoint from its scalars.

                def TensorAlgebra.tprod (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (n : ) :
                MultilinearMap R (fun (x : Fin n) => M) (TensorAlgebra R M)

                Construct a product of n elements of the module within the tensor algebra.

                See also PiTensorProduct.tprod.

                Equations
                Instances For
                  @[simp]
                  theorem TensorAlgebra.tprod_apply (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] {n : } (x : Fin nM) :
                  (TensorAlgebra.tprod R M n) x = (List.ofFn fun (i : Fin n) => (TensorAlgebra.ι R) (x i)).prod

                  The canonical image of the FreeAlgebra in the TensorAlgebra, which maps FreeAlgebra.ι R x to TensorAlgebra.ι R x.

                  Equations
                  Instances For
                    @[simp]
                    theorem FreeAlgebra.toTensor_ι {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (m : M) :
                    FreeAlgebra.toTensor (FreeAlgebra.ι R m) = (TensorAlgebra.ι R) m