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} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {a b : M} : Rel R M (FreeAlgebra.ι R (a + b)) (FreeAlgebra.ι R a + FreeAlgebra.ι R b)
• smul {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {r : R} {a : M} : 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.

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

instance instSemiringTensorAlgebra (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] : Semiring (TensorAlgebra 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)

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)

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)

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

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

theorem TensorAlgebra.ι_def (R : Type u_3) [CommSemiring R] {M : Type u_4} [AddCommMonoid M] [Module R M] : ι R = { toFun := fun (m : M) => (RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m), map_add' := ⋯, map_smul' := ⋯ }

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 (Rel R M)) (FreeAlgebra.ι R m) = (ι R) m

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.

@[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) : (lift R).symm F = F.toLinearMap ∘ₗ ι 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) : ((lift R) f).toLinearMap ∘ₗ ι 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) : ((lift R) f) ((ι 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 ∘ₗ ι R = f ↔ g = (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) : (lift R) (g.toLinearMap ∘ₗ ι 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 ∘ₗ ι R = g.toLinearMap ∘ₗ ι R) : f = g

See note [partially-applied ext lemmas].

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

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 ((algebraMap R (TensorAlgebra R M)) r)) (ι : ∀ (x : M), C ((ι 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.

@[simp]

theorem TensorAlgebra.adjoin_range_ι {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] : Algebra.adjoin R (Set.range ⇑(ι R)) = ⊤

@[simp]

theorem TensorAlgebra.range_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) : ((lift R) f).range = Algebra.adjoin R (Set.range ⇑f)

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.

theorem TensorAlgebra.algebraMap_leftInverse {R : Type u_1} [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] : Function.LeftInverse ⇑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

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.

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.

@[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] : toTrivSqZeroExt ((ι 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.

theorem TensorAlgebra.ι_leftInverse {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] : Function.LeftInverse ⇑ιInv ⇑(ι R)

@[simp]

theorem TensorAlgebra.ι_inj (R : Type u_1) [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (x y : M) : (ι R) x = (ι 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) : (ι 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) : (ι 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) : (ι 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 (ι 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.

@[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) : (tprod R M n) x = (List.ofFn fun (i : Fin n) => (ι 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.

@[simp]

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