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 M → FreeAlgebra R M → Prop

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)

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

• TensorAlgebra R M = RingQuot (TensorAlgebra.Rel R M)

instance instInhabitedTensorAlgebra (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] : Inhabited (TensorAlgebra R M)

Equations

• instInhabitedTensorAlgebra R M = RingQuot.instInhabited (TensorAlgebra.Rel R M)

instance instSemiringTensorAlgebra (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] : Semiring (TensorAlgebra R M)

Equations

• instSemiringTensorAlgebra R M = RingQuot.instSemiring (TensorAlgebra.Rel R M)

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] : Algebra R (TensorAlgebra A M)

Equations

• instAlgebra = RingQuot.instAlgebra (TensorAlgebra.Rel A M)

instance 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] : SMulCommClass R S (TensorAlgebra A M)

Equations

• ⋯ = ⋯

instance 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] : IsScalarTower R S (TensorAlgebra A M)

Equations

• ⋯ = ⋯

instance TensorAlgebra.instRing (M : Type u_2) [AddCommMonoid M] {S : Type u_3} [CommRing S] [Module S M] : Ring (TensorAlgebra S M)

Equations

• TensorAlgebra.instRing M = RingQuot.instRing (TensorAlgebra.Rel S M)

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] : M →ₗ[R] TensorAlgebra R M

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

Equations

• TensorAlgebra.ι = TensorAlgebra.wrapped✝.1

theorem TensorAlgebra.ringQuot_mkAlgHom_freeAlgebra_ι_eq_ι (R : Type u_1) [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (m : M) : (RingQuot.mkAlgHom R (TensorAlgebra.Rel R M)) (FreeAlgebra.ι R m) = (TensorAlgebra.ι R) m

@[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

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] : (M →ₗ[R] A) ≃ (TensorAlgebra R M →ₐ[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.

@[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) : ((TensorAlgebra.lift R) f) ((TensorAlgebra.ι R) x) = f x

@[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_iff {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} {g : TensorAlgebra R M →ₐ[R] A} : f = g ↔ f.toLinearMap ∘ₗ TensorAlgebra.ι R = g.toLinearMap ∘ₗ TensorAlgebra.ι R

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 : TensorAlgebra R M →ₐ[R] A} {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 M → Prop} (algebraMap : ∀ (r : R), C ((_root_.algebraMap R (TensorAlgebra R M)) r)) (ι : ∀ (x : M), C ((TensorAlgebra.ι R) x)) (mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)) (add : ∀ (a b : TensorAlgebra R M), C a → C b → C (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.

def TensorAlgebra.algebraMapInv {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] : TensorAlgebra R M →ₐ[R] R

The left-inverse of algebraMap.

Equations

• TensorAlgebra.algebraMapInv = (TensorAlgebra.lift R) 0

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 : R) (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

instance TensorAlgebra.instNontrivial {R : Type u_1} [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] [Nontrivial R] : Nontrivial (TensorAlgebra R M)

A TensorAlgebra over a nontrivial semiring is nontrivial.

Equations

• ⋯ = ⋯

def TensorAlgebra.toTrivSqZeroExt {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] : TensorAlgebra R M →ₐ[R] TrivSqZeroExt R M

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)

@[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] : TensorAlgebra R M →ₗ[R] M

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

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 : M) (y : M) : (TensorAlgebra.ι R) x = (TensorAlgebra.ι R) y ↔ x = y

@[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) : (TensorAlgebra.ι R) x ≠ 1

theorem TensorAlgebra.ι_range_disjoint_one {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] : Disjoint (LinearMap.range (TensorAlgebra.ι R)) 1

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

• TensorAlgebra.tprod R M n = (MultilinearMap.mkPiAlgebraFin R n (TensorAlgebra R M)).compLinearMap fun (x : Fin n) => TensorAlgebra.ι R

@[simp]

theorem TensorAlgebra.tprod_apply (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) : (TensorAlgebra.tprod R M n) x = (List.ofFn fun (i : Fin n) => (TensorAlgebra.ι R) (x i)).prod

def FreeAlgebra.toTensor {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] : FreeAlgebra R M →ₐ[R] TensorAlgebra R M

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)

@[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