Tensor products in the general linear group

This file packages the tensor product of two linear automorphisms as an automorphism and records its compatibility with multiplication, inverses, and pure tensors.

Main declarations

• LinearMap.GeneralLinearGroup.tensorProduct: the tensor product of two linear automorphisms.
• LinearMap.GeneralLinearGroup.tensorProduct_tmul: its action on a pure tensor.

def LinearMap.GeneralLinearGroup.tensorProduct {K : Type u} {V : Type v} {W : Type w} [CommSemiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid W] [Module K W] (g : GeneralLinearGroup K V) (h : GeneralLinearGroup K W) : GeneralLinearGroup K (TensorProduct K V W)

The tensor product of two linear automorphisms.

Equations

• g.tensorProduct h = LinearMap.GeneralLinearGroup.ofLinearEquiv (TensorProduct.congr g.toLinearEquiv h.toLinearEquiv)

theorem LinearMap.GeneralLinearGroup.coe_tensorProduct {K : Type u} {V : Type v} {W : Type w} [CommSemiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid W] [Module K W] (g : GeneralLinearGroup K V) (h : GeneralLinearGroup K W) : ↑(g.tensorProduct h) = TensorProduct.map ↑g ↑h

The endomorphism underlying a tensor-product automorphism is TensorProduct.map.

@[simp]

theorem LinearMap.GeneralLinearGroup.tensorProduct_tmul {K : Type u} {V : Type v} {W : Type w} [CommSemiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid W] [Module K W] (g : GeneralLinearGroup K V) (h : GeneralLinearGroup K W) (v : V) (w : W) : ↑(g.tensorProduct h) (v ⊗ₜ[K] w) = ↑g v ⊗ₜ[K] ↑h w

A tensor-product automorphism acts factorwise on pure tensors.

@[simp]

theorem LinearMap.GeneralLinearGroup.tensorProduct_mul {K : Type u} {V : Type v} {W : Type w} [CommSemiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid W] [Module K W] (g₁ g₂ : GeneralLinearGroup K V) (h₁ h₂ : GeneralLinearGroup K W) : (g₁ * g₂).tensorProduct (h₁ * h₂) = g₁.tensorProduct h₁ * g₂.tensorProduct h₂

Tensor products preserve multiplication.

@[simp]

theorem LinearMap.GeneralLinearGroup.tensorProduct_one {K : Type u} {V : Type v} {W : Type w} [CommSemiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid W] [Module K W] : tensorProduct 1 1 = 1

The tensor product of two identity automorphisms is the identity.

@[simp]

theorem LinearMap.GeneralLinearGroup.tensorProduct_inv {K : Type u} {V : Type v} {W : Type w} [CommSemiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid W] [Module K W] (g : GeneralLinearGroup K V) (h : GeneralLinearGroup K W) : g⁻¹.tensorProduct h⁻¹ = (g.tensorProduct h)⁻¹

Tensor products preserve inverses.