Modules over tensor-product algebras

A module over A ⊗[k] B has commuting actions of A and B, obtained by restricting along Algebra.TensorProduct.includeLeft and Algebra.TensorProduct.includeRight. These actions are explicit definitions, since an existing action of a factor may be different. For B = Aᵐᵒᵖ, they are the left and right actions of an ordinary bimodule. The factor-action identities are explicit rewrite rules: their tensor-product parameters are carried by the chosen scalar instance, so global simp would try to infer hidden factors for unrelated scalar actions.

The factor actions agree with the ground-ring action. This supplies the restriction needed for balanced tensor products of enveloping-algebra modules; it uses Mathlib's scalar restriction without a new bimodule type.

A ground-linear map equivariant for the two factor inclusions is linear over the whole tensor-product algebra. linearMapOfFactors packages this criterion, so constructions with commuting outer actions can reuse the same extension of linearity.

BialgebraModule.tensorPairAction assembles the actions of A on M and of B on N into an action of A ⊗[R] B on M ⊗[R] N, using Mathlib's Algebra.lsmul, Algebra.TensorProduct.map, and Module.endTensorEndAlgHom. This construction requires only algebras, without a coproduct.

@[reducible, inline]

abbrev TauCeti.Algebra.TensorProduct.moduleLeft {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring k] [Semiring A] [Semiring B] [Algebra k A] [Algebra k B] (M : Type u_4) [AddCommMonoid M] [Module (TensorProduct k A B) M] : Module A M

Restrict a tensor-product algebra module to the first factor.

@[reducible, inline]

abbrev TauCeti.Algebra.TensorProduct.moduleRight {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring k] [Semiring A] [Semiring B] [Algebra k A] [Algebra k B] (M : Type u_4) [AddCommMonoid M] [Module (TensorProduct k A B) M] : Module B M

Restrict a tensor-product algebra module to the second factor.

theorem TauCeti.Algebra.TensorProduct.smul_moduleLeft {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring k] [Semiring A] [Semiring B] [Algebra k A] [Algebra k B] (M : Type u_4) [AddCommMonoid M] [Module (TensorProduct k A B) M] (a : A) (m : M) : a • m = a ⊗ₜ[k] 1 • m

The first-factor action is the action of a ⊗ 1.

theorem TauCeti.Algebra.TensorProduct.smul_moduleRight {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring k] [Semiring A] [Semiring B] [Algebra k A] [Algebra k B] (M : Type u_4) [AddCommMonoid M] [Module (TensorProduct k A B) M] (b : B) (m : M) : b • m = 1 ⊗ₜ[k] b • m

The second-factor action is the action of 1 ⊗ b.

theorem TauCeti.Algebra.TensorProduct.moduleSMulCommClass {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring k] [Semiring A] [Semiring B] [Algebra k A] [Algebra k B] (M : Type u_4) [AddCommMonoid M] [Module (TensorProduct k A B) M] : SMulCommClass A B M

The restricted factor actions commute.

theorem TauCeti.Algebra.TensorProduct.moduleLeftIsScalarTower {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring k] [Semiring A] [Semiring B] [Algebra k A] [Algebra k B] (M : Type u_4) [AddCommMonoid M] [Module (TensorProduct k A B) M] [Module k M] [IsScalarTower k (TensorProduct k A B) M] : IsScalarTower k A M

Restricting to the first factor respects the ground-ring action.

theorem TauCeti.Algebra.TensorProduct.moduleRightIsScalarTower {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring k] [Semiring A] [Semiring B] [Algebra k A] [Algebra k B] (M : Type u_4) [AddCommMonoid M] [Module (TensorProduct k A B) M] [Module k M] [IsScalarTower k (TensorProduct k A B) M] : IsScalarTower k B M

Restricting to the second factor respects the ground-ring action.

def TauCeti.Algebra.TensorProduct.linearMapOfFactors {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring k] [Semiring A] [Semiring B] [Algebra k A] [Algebra k B] (M : Type u_4) [AddCommMonoid M] [Module (TensorProduct k A B) M] [Module k M] {N : Type u_5} [AddCommMonoid N] [Module k N] [Module (TensorProduct k A B) N] (f : M →ₗ[k] N) (hleft : ∀ (a : A) (m : M), f (a ⊗ₜ[k] 1 • m) = a ⊗ₜ[k] 1 • f m) (hright : ∀ (b : B) (m : M), f (1 ⊗ₜ[k] b • m) = 1 ⊗ₜ[k] b • f m) : M →ₗ[TensorProduct k A B] N

A ground-linear map equivariant for both factor inclusions is tensor-algebra linear.

@[simp]

theorem TauCeti.Algebra.TensorProduct.linearMapOfFactors_apply {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring k] [Semiring A] [Semiring B] [Algebra k A] [Algebra k B] (M : Type u_4) [AddCommMonoid M] [Module (TensorProduct k A B) M] [Module k M] {N : Type u_5} [AddCommMonoid N] [Module k N] [Module (TensorProduct k A B) N] (f : M →ₗ[k] N) (hleft : ∀ (a : A) (m : M), f (a ⊗ₜ[k] 1 • m) = a ⊗ₜ[k] 1 • f m) (hright : ∀ (b : B) (m : M), f (1 ⊗ₜ[k] b • m) = 1 ⊗ₜ[k] b • f m) (m : M) : (linearMapOfFactors M f hleft hright) m = f m

Extending linearity preserves the underlying function.

@[simp]

theorem TauCeti.Algebra.TensorProduct.linearMapOfFactors_restrictScalars {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring k] [Semiring A] [Semiring B] [Algebra k A] [Algebra k B] (M : Type u_4) [AddCommMonoid M] [Module (TensorProduct k A B) M] [Module k M] {N : Type u_5} [AddCommMonoid N] [Module k N] [Module (TensorProduct k A B) N] [IsScalarTower k (TensorProduct k A B) M] [IsScalarTower k (TensorProduct k A B) N] (f : M →ₗ[k] N) (hleft : ∀ (a : A) (m : M), f (a ⊗ₜ[k] 1 • m) = a ⊗ₜ[k] 1 • f m) (hright : ∀ (b : B) (m : M), f (1 ⊗ₜ[k] b • m) = 1 ⊗ₜ[k] b • f m) : ↑k (linearMapOfFactors M f hleft hright) = f

Restricting the extended linear map returns the original ground-linear map.

noncomputable def TauCeti.BialgebraModule.tensorPairAction (R : Type u_1) {A : Type u_2} {B : Type u_3} (M : Type u_4) (N : Type u_5) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Module A M] [IsScalarTower R A M] [Module B N] [IsScalarTower R B N] : TensorProduct R A B →ₐ[R] Module.End R (TensorProduct R M N)

The action of A on M and the action of B on N assembled into an action of A ⊗[R] B on M ⊗[R] N.

@[simp]

theorem TauCeti.BialgebraModule.tensorPairAction_tmul (R : Type u_1) {A : Type u_2} {B : Type u_3} (M : Type u_4) (N : Type u_5) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Module A M] [IsScalarTower R A M] [Module B N] [IsScalarTower R B N] (a : A) (b : B) (m : M) (n : N) : ((tensorPairAction R M N) (a ⊗ₜ[R] b)) (m ⊗ₜ[R] n) = (a • m) ⊗ₜ[R] (b • n)

A pure tensor of algebra elements acts on the two factors separately.

theorem TauCeti.BialgebraModule.tensorPairAction_natural (R : Type u_1) {A : Type u_2} {B : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Module A M] [IsScalarTower R A M] [Module B N] [IsScalarTower R B N] {M' : Type u_6} {N' : Type u_7} [AddCommMonoid M'] [Module R M'] [Module A M'] [IsScalarTower R A M'] [AddCommMonoid N'] [Module R N'] [Module B N'] [IsScalarTower R B N'] (f : M →ₗ[A] M') (g : N →ₗ[B] N') (t : TensorProduct R A B) (x : TensorProduct R M N) : (TensorProduct.map (↑R f) (↑R g)) (((tensorPairAction R M N) t) x) = ((tensorPairAction R M' N') t) ((TensorProduct.map (↑R f) (↑R g)) x)

Tensor products of intertwiners commute with the separate factor actions.