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 #
TensorAlgebra R M
is the tensor algebra itself. It is endowed with an R-algebra structure.TensorAlgebra.ι R
is the canonical R-linear mapM → TensorAlgebra R M
.- Given a linear map
f : M → A
to an R-algebraA
,lift R f
is the lift off
to anR
-algebra morphismTensorAlgebra R M → A
.
Theorems #
ι_comp_lift
states that the composition(lift R f) ∘ (ι R)
is identical tof
.lift_unique
states that whenever an R-algebra morphismg : TensorAlgebra R M → A
is given whose composition withι R
isf
, then one hasg = lift R f
.hom_ext
is a variant oflift_unique
in the form of an extensionality theorem.lift_comp_ι
is a combination ofι_comp_lift
andlift_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.
An inductively defined relation on Pre R M
used to force the initial algebra structure on
the associated quotient.
- add: ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {a b : M}, TensorAlgebra.Rel R M (FreeAlgebra.ι R (a + b)) (FreeAlgebra.ι R a + FreeAlgebra.ι R b)
- smul: ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R} {a : M}, TensorAlgebra.Rel R M (FreeAlgebra.ι R (r • a)) ((algebraMap R (FreeAlgebra R M)) r * FreeAlgebra.ι R a)
Instances For
The tensor algebra of the module M
over the commutative semiring R
.
Equations
- TensorAlgebra R M = RingQuot (TensorAlgebra.Rel R M)
Instances For
Equations
Equations
Equations
- instAlgebra = RingQuot.instAlgebra (TensorAlgebra.Rel A M)
Equations
The canonical linear map M →ₗ[R] TensorAlgebra R M
.
Equations
Instances For
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
See note [partially-applied ext lemmas].
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
- TensorAlgebra.algebraMapInv = (TensorAlgebra.lift R) 0
Instances For
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
- TensorAlgebra.toTrivSqZeroExt = (TensorAlgebra.lift R) (TrivSqZeroExt.inrHom R M)
Instances For
The left-inverse of ι
.
As an implementation detail, we implement this using TrivSqZeroExt
which has a suitable
algebra structure.
Equations
- TensorAlgebra.ιInv = TrivSqZeroExt.sndHom R M ∘ₗ TensorAlgebra.toTrivSqZeroExt.toLinearMap
Instances For
The generators of the tensor algebra are disjoint from its scalars.
Construct a product of n
elements of the module within the tensor algebra.
See also PiTensorProduct.tprod
.
Equations
- TensorAlgebra.tprod R M n = (MultilinearMap.mkPiAlgebraFin R n (TensorAlgebra R M)).compLinearMap fun (x : Fin n) => TensorAlgebra.ι R
Instances For
The canonical image of the FreeAlgebra
in the TensorAlgebra
, which maps
FreeAlgebra.ι R x
to TensorAlgebra.ι R x
.
Equations
- FreeAlgebra.toTensor = (FreeAlgebra.lift R) ⇑(TensorAlgebra.ι R)