Tensor Algebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
tensor_algebra R Mis the tensor algebra itself. It is endowed with an R-algebra structure.tensor_algebra.ι Ris the canonical R-linear mapM → tensor_algebra R M.- Given a linear map
f : M → Ato an R-algebraA,lift R fis the lift offto anR-algebra morphismtensor_algebra R M → A.
Theorems #
ι_comp_liftstates that the composition(lift R f) ∘ (ι R)is identical tof.lift_uniquestates that whenever an R-algebra morphismg : tensor_algebra R M → Ais given whose composition withι Risf, then one hasg = lift R f.hom_extis a variant oflift_uniquein the form of an extensionality theorem.lift_comp_ιis a combination ofι_comp_liftandlift_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
tensor_algebra.rel
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_monoid M]
[module R M] :
free_algebra R M → free_algebra R M → Prop
- add : ∀ {R : Type u_1} [_inst_1 : comm_semiring R] {M : Type u_2} [_inst_2 : add_comm_monoid M] [_inst_3 : module R M] {a b : M}, tensor_algebra.rel R M (free_algebra.ι R (a + b)) (free_algebra.ι R a + free_algebra.ι R b)
- smul : ∀ {R : Type u_1} [_inst_1 : comm_semiring R] {M : Type u_2} [_inst_2 : add_comm_monoid M] [_inst_3 : module R M] {r : R} {a : M}, tensor_algebra.rel R M (free_algebra.ι R (r • a)) (⇑(algebra_map R (free_algebra R M)) r * free_algebra.ι R a)
An inductively defined relation on pre R M used to force the initial algebra structure on
the associated quotient.
@[protected, instance]
def
tensor_algebra.inhabited
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_monoid M]
[module R M] :
inhabited (tensor_algebra R M)
def
tensor_algebra
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_monoid M]
[module R M] :
Type (max u_1 u_2)
The tensor algebra of the module M over the commutative semiring R.
Equations
- tensor_algebra R M = ring_quot (tensor_algebra.rel R M)
@[protected, instance]
def
tensor_algebra.semiring
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_monoid M]
[module R M] :
semiring (tensor_algebra R M)
@[protected, instance]
def
tensor_algebra.algebra
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_monoid M]
[module R M] :
algebra R (tensor_algebra R M)
@[protected, instance]
def
tensor_algebra.ring
(M : Type u_2)
[add_comm_monoid M]
{S : Type u_1}
[comm_ring S]
[module S M] :
ring (tensor_algebra S M)
Equations
@[irreducible]
def
tensor_algebra.ι
(R : Type u_1)
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M] :
M →ₗ[R] tensor_algebra R M
The canonical linear map M →ₗ[R] tensor_algebra R M.
Equations
- tensor_algebra.ι R = {to_fun := λ (m : M), ⇑(ring_quot.mk_alg_hom R (tensor_algebra.rel R M)) (free_algebra.ι R m), map_add' := _, map_smul' := _}
theorem
tensor_algebra.ring_quot_mk_alg_hom_free_algebra_ι_eq_ι
(R : Type u_1)
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
(m : M) :
⇑(ring_quot.mk_alg_hom R (tensor_algebra.rel R M)) (free_algebra.ι R m) = ⇑(tensor_algebra.ι R) m
@[simp]
theorem
tensor_algebra.lift_symm_apply
(R : Type u_1)
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{A : Type u_3}
[semiring A]
[algebra R A]
(F : tensor_algebra R M →ₐ[R] A) :
⇑((tensor_algebra.lift R).symm) F = F.to_linear_map.comp (tensor_algebra.ι R)
@[irreducible]
def
tensor_algebra.lift
(R : Type u_1)
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid 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 tensor_algebra R M → A.
Equations
- tensor_algebra.lift R = {to_fun := ⇑(ring_quot.lift_alg_hom R) ∘ λ (f : M →ₗ[R] A), ⟨⇑(free_algebra.lift R) ⇑f, _⟩, inv_fun := λ (F : tensor_algebra R M →ₐ[R] A), F.to_linear_map.comp (tensor_algebra.ι R), left_inv := _, right_inv := _}
@[simp]
theorem
tensor_algebra.ι_comp_lift
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{A : Type u_3}
[semiring A]
[algebra R A]
(f : M →ₗ[R] A) :
(⇑(tensor_algebra.lift R) f).to_linear_map.comp (tensor_algebra.ι R) = f
@[simp]
theorem
tensor_algebra.lift_ι_apply
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{A : Type u_3}
[semiring A]
[algebra R A]
(f : M →ₗ[R] A)
(x : M) :
⇑(⇑(tensor_algebra.lift R) f) (⇑(tensor_algebra.ι R) x) = ⇑f x
@[simp]
theorem
tensor_algebra.lift_unique
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{A : Type u_3}
[semiring A]
[algebra R A]
(f : M →ₗ[R] A)
(g : tensor_algebra R M →ₐ[R] A) :
g.to_linear_map.comp (tensor_algebra.ι R) = f ↔ g = ⇑(tensor_algebra.lift R) f
@[simp]
theorem
tensor_algebra.lift_comp_ι
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{A : Type u_3}
[semiring A]
[algebra R A]
(g : tensor_algebra R M →ₐ[R] A) :
⇑(tensor_algebra.lift R) (g.to_linear_map.comp (tensor_algebra.ι R)) = g
@[ext]
theorem
tensor_algebra.hom_ext
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{A : Type u_3}
[semiring A]
[algebra R A]
{f g : tensor_algebra R M →ₐ[R] A}
(w : f.to_linear_map.comp (tensor_algebra.ι R) = g.to_linear_map.comp (tensor_algebra.ι R)) :
f = g
theorem
tensor_algebra.induction
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{C : tensor_algebra R M → Prop}
(h_grade0 : ∀ (r : R), C (⇑(algebra_map R (tensor_algebra R M)) r))
(h_grade1 : ∀ (x : M), C (⇑(tensor_algebra.ι R) x))
(h_mul : ∀ (a b : tensor_algebra R M), C a → C b → C (a * b))
(h_add : ∀ (a b : tensor_algebra R M), C a → C b → C (a + b))
(a : tensor_algebra R M) :
C a
If C holds for the algebra_map of r : R into tensor_algebra R M, the ι of x : M,
and is preserved under addition and muliplication, then it holds for all of tensor_algebra R M.
def
tensor_algebra.algebra_map_inv
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M] :
tensor_algebra R M →ₐ[R] R
The left-inverse of algebra_map.
Equations
theorem
tensor_algebra.algebra_map_left_inverse
{R : Type u_1}
[comm_semiring R]
(M : Type u_2)
[add_comm_monoid M]
[module R M] :
@[simp]
theorem
tensor_algebra.algebra_map_inj
{R : Type u_1}
[comm_semiring R]
(M : Type u_2)
[add_comm_monoid M]
[module R M]
(x y : R) :
⇑(algebra_map R (tensor_algebra R M)) x = ⇑(algebra_map R (tensor_algebra R M)) y ↔ x = y
@[simp]
theorem
tensor_algebra.algebra_map_eq_zero_iff
{R : Type u_1}
[comm_semiring R]
(M : Type u_2)
[add_comm_monoid M]
[module R M]
(x : R) :
⇑(algebra_map R (tensor_algebra R M)) x = 0 ↔ x = 0
@[simp]
theorem
tensor_algebra.algebra_map_eq_one_iff
{R : Type u_1}
[comm_semiring R]
(M : Type u_2)
[add_comm_monoid M]
[module R M]
(x : R) :
⇑(algebra_map R (tensor_algebra R M)) x = 1 ↔ x = 1
def
tensor_algebra.to_triv_sq_zero_ext
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
[module Rᵐᵒᵖ M]
[is_central_scalar R M] :
tensor_algebra R M →ₐ[R] triv_sq_zero_ext R M
The canonical map from tensor_algebra R M into triv_sq_zero_ext R M that sends
tensor_algebra.ι to triv_sq_zero_ext.inr.
Equations
@[simp]
theorem
tensor_algebra.to_triv_sq_zero_ext_ι
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
(x : M)
[module Rᵐᵒᵖ M]
[is_central_scalar R M] :
def
tensor_algebra.ι_inv
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M] :
tensor_algebra R M →ₗ[R] M
The left-inverse of ι.
As an implementation detail, we implement this using triv_sq_zero_ext which has a suitable
algebra structure.
Equations
- tensor_algebra.ι_inv = let _inst : module Rᵐᵒᵖ M := module.comp_hom M ((ring_hom.id R).from_opposite tensor_algebra.ι_inv._proof_1) in (triv_sq_zero_ext.snd_hom R M).comp tensor_algebra.to_triv_sq_zero_ext.to_linear_map
theorem
tensor_algebra.ι_left_inverse
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M] :
@[simp]
theorem
tensor_algebra.ι_inj
(R : Type u_1)
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
(x y : M) :
⇑(tensor_algebra.ι R) x = ⇑(tensor_algebra.ι R) y ↔ x = y
@[simp]
theorem
tensor_algebra.ι_eq_zero_iff
(R : Type u_1)
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
(x : M) :
⇑(tensor_algebra.ι R) x = 0 ↔ x = 0
@[simp]
theorem
tensor_algebra.ι_eq_algebra_map_iff
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
(x : M)
(r : R) :
⇑(tensor_algebra.ι R) x = ⇑(algebra_map R (tensor_algebra R M)) r ↔ x = 0 ∧ r = 0
@[simp]
theorem
tensor_algebra.ι_ne_one
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
[nontrivial R]
(x : M) :
⇑(tensor_algebra.ι R) x ≠ 1
theorem
tensor_algebra.ι_range_disjoint_one
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M] :
disjoint (linear_map.range (tensor_algebra.ι R)) 1
The generators of the tensor algebra are disjoint from its scalars.
def
tensor_algebra.tprod
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_monoid M]
[module R M]
(n : ℕ) :
multilinear_map R (λ (i : fin n), M) (tensor_algebra R M)
Construct a product of n elements of the module within the tensor algebra.
See also pi_tensor_product.tprod.
Equations
- tensor_algebra.tprod R M n = (multilinear_map.mk_pi_algebra_fin R n (tensor_algebra R M)).comp_linear_map (λ (_x : fin n), tensor_algebra.ι R)
@[simp]
theorem
tensor_algebra.tprod_apply
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_monoid M]
[module R M]
{n : ℕ}
(x : fin n → M) :
⇑(tensor_algebra.tprod R M n) x = (list.of_fn (λ (i : fin n), ⇑(tensor_algebra.ι R) (x i))).prod
def
free_algebra.to_tensor
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M] :
free_algebra R M →ₐ[R] tensor_algebra R M
The canonical image of the free_algebra in the tensor_algebra, which maps
free_algebra.ι R x to tensor_algebra.ι R x.
Equations
@[simp]
theorem
free_algebra.to_tensor_ι
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
(m : M) :
⇑free_algebra.to_tensor (free_algebra.ι R m) = ⇑(tensor_algebra.ι R) m