Documentation

TauCeti.Algebra.AlgebraicGroup.Representation.Comodule.TensorProduct

Tensor products of point representations #

This file synchronizes tensor-product operations across the fixed-object correspondence between point representations of an affine group and comodules over its commutative Hopf algebra.

Two point representations on V and W have a tensor representation on V ⊗ W: at a value algebra A, its action is the tensor product of the two component automorphisms, transported across the canonical equivalence

A ⊗[R] (V ⊗[R] W) ≃ (A ⊗[R] V) ⊗[A] (A ⊗[R] W).

This construction agrees with the point representation induced by the diagonal tensor-product comodule. No finiteness, freeness, projectivity, flatness, or nontriviality hypothesis is used.

Main declarations #

References #

source
noncomputable def TauCeti.HopfAlgebra.PointRepresentation.tensor {R : Type u} {H : Type v} {V W : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module R W] (Theta : PointRepresentation) (Psi : PointRepresentation) :
PointRepresentation

The tensor product of two point representations. At each value algebra, the tensor product of the component automorphisms is transported across scalar-extension distributivity.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.HopfAlgebra.PointRepresentation.tensor_action_tmul {R : Type u} {H : Type v} {V W : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module R W] (Theta : PointRepresentation) (Psi : PointRepresentation) (A : CommAlgCat R) (x : ↑(points A)) (a : ↑A) (v : V) (w : W) :
    ↑((CategoryTheory.ConcreteCategory.hom ((Theta.tensor Psi).action A)) x) (a ⊗ₜ[R] (v ⊗ₜ[R] w)) = (TensorProduct.AlgebraTensorModule.distribBaseChange R (↑A) V W).symm (↑((CategoryTheory.ConcreteCategory.hom (Theta.action A)) x) (a ⊗ₜ[R] v) ⊗ₜ[↑A] ↑((CategoryTheory.ConcreteCategory.hom (Psi.action A)) x) (1 ⊗ₜ[R] w))

    On a pure tensor, the tensor point action applies the two component actions diagonally and transports the result back through scalar-extension distributivity.

    source
    theorem TauCeti.HopfAlgebra.PointRepresentation.tensor_action_apply {R : Type u} {H : Type v} {V W : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module R W] (Theta : PointRepresentation) (Psi : PointRepresentation) (A : CommAlgCat R) (x : ↑(points A)) (z : TensorProduct R (↑A) (TensorProduct R V W)) :
    ↑((CategoryTheory.ConcreteCategory.hom ((Theta.tensor Psi).action A)) x) z = (TensorProduct.AlgebraTensorModule.distribBaseChange R (↑A) V W).symm ((TensorProduct.map ↑((CategoryTheory.ConcreteCategory.hom (Theta.action A)) x) ↑((CategoryTheory.ConcreteCategory.hom (Psi.action A)) x)) ((TensorProduct.AlgebraTensorModule.distribBaseChange R (↑A) V W) z))

    The tensor point action, expressed by conjugating the tensor of the two component linear maps through scalar-extension distributivity.

    source
    @[simp]
    theorem TauCeti.HopfAlgebra.PointRepresentation.ofComodule_tensor {R : Type u} {H : Type v} {V W : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module R W] (rhoV : Comodule R H V) (rhoW : Comodule R H W) :
    ofComodule (Comodule.tensor R H V W) = (ofComodule rhoV).tensor (ofComodule rhoW)

    The point representation induced by the tensor product of two comodules is the tensor product of their induced point representations.

    source
    @[simp]
    theorem TauCeti.HopfAlgebra.PointRepresentation.toComodule_tensor {R : Type u} {H : Type v} {V W : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module R W] (Theta : PointRepresentation) (Psi : PointRepresentation) :
    (Theta.tensor Psi).toComodule = Comodule.tensor R H V W

    Recovering the comodule of a tensor-product point representation gives the tensor product of the recovered comodules.