Coproduct actions on tensor products of modules

For a bialgebra H over a commutative semiring R, its coproduct acts on the tensor product of two H-modules. BialgebraModule.Tensor is a type synonym of the native R-tensor product, with this coproduct action. A synonym is necessary because the native tensor product's left-factor scalar action would otherwise compete with the coproduct action. The original factor R-module structures are retained; tensorEquiv identifies the base action with the native tensor action.

tensorEquiv identifies the underlying R-module with the native tensor product; tmul constructs pure tensors. tensorMap tensors native H-linear intertwiners.

The coproduct action restricts tensorPairAction along Bialgebra.comulAlgHom.

BialgebraModule.Trivial is the base semiring with H acting through its counit. The associativity equivalence assoc (with its naturality tensorMap_tensorMap_assoc and pentagon coherence assoc_pentagon) and the unit equivalences lid and rid are the native tensor-product equivalences, which are H-linear by coassociativity and the two counit laws. Together with the trivial module these are the data of the monoidal structure on modules over a bialgebra; see C. Kassel, Quantum Groups, Chapter III.

def TauCeti.BialgebraModule.Tensor (R : Type u_1) (_H : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : Type (max u_3 u_4)

The tensor product over R, with a separate carrier for the coproduct action of H.

The synonym separates that action from the native tensor product's left-factor action. The module structures reuse the native tensor structures locally; the action itself is characterized by tensorEquiv_smul. Its base action agrees with the native tensor action under tensorEquiv.

@[instance_reducible]

instance TauCeti.BialgebraModule.instAddCommMonoidTensor (R : Type u_1) (H : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : AddCommMonoid (Tensor R H M N)

@[instance_reducible]

instance TauCeti.BialgebraModule.instAddCommGroupTensor (R : Type u_5) (H : Type u_6) (M : Type u_7) (N : Type u_8) [CommSemiring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : AddCommGroup (Tensor R H M N)

noncomputable def TauCeti.BialgebraModule.tensorAction (R : Type u_1) (H : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] : H →ₐ[R] Module.End R (TensorProduct R M N)

The representation of H on the native tensor product obtained from its coproduct.

theorem TauCeti.BialgebraModule.tensorAction_apply (R : Type u_1) (H : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] (h : H) (x : TensorProduct R M N) : ((tensorAction R H M N) h) x = ((tensorPairAction R M N) (CoalgebraStruct.comul h)) x

The coproduct action is the pair action applied to the coproduct.

@[instance_reducible]

noncomputable instance TauCeti.BialgebraModule.instModuleTensor (R : Type u_1) (H : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] : Module H (Tensor R H M N)

The coproduct module structure on the tensor carrier.

@[instance_reducible, instance 1100]

noncomputable instance TauCeti.BialgebraModule.instModuleTensor_1 (R : Type u_1) (H : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] : Module R (Tensor R H M N)

The base action is restriction of the coproduct action along the algebra map.

For the canonical algebra structure when H = R, this presentation also aligns the two scalar actions. The underlying equivalence below identifies it with the original native tensor action. The priority keeps this presentation ahead of generic natural and integer scalar actions.

instance TauCeti.BialgebraModule.instIsScalarTowerTensor (R : Type u_1) (H : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] : IsScalarTower R H (Tensor R H M N)

The coproduct module is compatible with the caller's base scalar action.

noncomputable def TauCeti.BialgebraModule.tensorEquiv (R : Type u_1) (H : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] : Tensor R H M N ≃ₗ[R] TensorProduct R M N

The underlying R-linear identification with the native tensor product.

instance TauCeti.BialgebraModule.instFiniteTensor (R : Type u_1) (H : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] [Module.Finite R M] [Module.Finite R N] : Module.Finite R (Tensor R H M N)

Finite base modules have a finite tensor product with the coproduct action.

noncomputable def TauCeti.BialgebraModule.tmul (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] (m : M) (n : N) : Tensor R H M N

A pure tensor in the carrier with the coproduct action.

@[simp]

theorem TauCeti.BialgebraModule.tensorEquiv_tmul (R : Type u_1) (H : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] (m : M) (n : N) : (tensorEquiv R H M N) (tmul R H m n) = m ⊗ₜ[R] n

The underlying equivalence sends a pure tensor to the native pure tensor.

@[simp]

theorem TauCeti.BialgebraModule.tensorEquiv_symm_tmul (R : Type u_1) (H : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] (m : M) (n : N) : (tensorEquiv R H M N).symm (m ⊗ₜ[R] n) = tmul R H m n

The inverse underlying equivalence constructs pure tensors.

@[simp]

theorem TauCeti.BialgebraModule.add_tmul (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] (m m' : M) (n : N) : tmul R H (m + m') n = tmul R H m n + tmul R H m' n

Pure tensors are additive in the first factor.

@[simp]

theorem TauCeti.BialgebraModule.tmul_add (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] (m : M) (n n' : N) : tmul R H m (n + n') = tmul R H m n + tmul R H m n'

Pure tensors are additive in the second factor.

@[simp]

theorem TauCeti.BialgebraModule.zero_tmul (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] (n : N) : tmul R H 0 n = 0

A zero first factor gives the zero tensor.

@[simp]

theorem TauCeti.BialgebraModule.tmul_zero (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] (m : M) : tmul R H m 0 = 0

A zero second factor gives the zero tensor.

theorem TauCeti.BialgebraModule.sum_tmul (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {ι : Type u_5} (s : Finset ι) (m : ι → M) (n : N) : tmul R H (∑ i ∈ s, m i) n = ∑ i ∈ s, tmul R H (m i) n

Pure tensors distribute over finite sums in the first factor.

theorem TauCeti.BialgebraModule.tmul_sum (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {ι : Type u_5} (s : Finset ι) (m : M) (n : ι → N) : tmul R H m (∑ i ∈ s, n i) = ∑ i ∈ s, tmul R H m (n i)

Pure tensors distribute over finite sums in the second factor.

theorem TauCeti.BialgebraModule.smul_tmul' (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] (r : R) (m : M) (n : N) : r • tmul R H m n = tmul R H (r • m) n

Base scalars may be applied to the first factor.

@[simp]

theorem TauCeti.BialgebraModule.tmul_smul (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] (r : R) (m : M) (n : N) : tmul R H m (r • n) = r • tmul R H m n

Base scalars may be applied to the second factor.

@[simp]

theorem TauCeti.BialgebraModule.neg_tmul (R : Type u_1) (H : Type u_2) [CommSemiring R] [Semiring H] [Bialgebra R H] {M : Type u_5} {N : Type u_6} [AddCommGroup M] [Module R M] [Module H M] [IsScalarTower R H M] [AddCommGroup N] [Module R N] [Module H N] [IsScalarTower R H N] (m : M) (n : N) : tmul R H (-m) n = -tmul R H m n

Negating the first factor negates the pure tensor.

@[simp]

theorem TauCeti.BialgebraModule.tmul_neg (R : Type u_1) (H : Type u_2) [CommSemiring R] [Semiring H] [Bialgebra R H] {M : Type u_5} {N : Type u_6} [AddCommGroup M] [Module R M] [Module H M] [IsScalarTower R H M] [AddCommGroup N] [Module R N] [Module H N] [IsScalarTower R H N] (m : M) (n : N) : tmul R H m (-n) = -tmul R H m n

Negating the second factor negates the pure tensor.

theorem TauCeti.BialgebraModule.Tensor.inductionOn {R : Type u_1} {H : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {P : Tensor R H M N → Prop} (x : Tensor R H M N) (htmul : ∀ (m : M) (n : N), P (tmul R H m n)) (hadd : ∀ (x y : Tensor R H M N), P x → P y → P (x + y)) : P x

Prove a proposition about coproduct tensors by pure tensors and addition.

theorem TauCeti.BialgebraModule.Tensor.ext {R : Type u_1} {H : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {P : Type u_5} [AddCommMonoid P] [Module H P] {f g : Tensor R H M N →ₗ[H] P} (h : ∀ (m : M) (n : N), f (tmul R H m n) = g (tmul R H m n)) : f = g

Two H-linear maps from the coproduct tensor carrier agree if they agree on pure tensors.

theorem TauCeti.BialgebraModule.Tensor.ext_iff {R : Type u_1} {H : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {P : Type u_5} [AddCommMonoid P] [Module H P] {f g : Tensor R H M N →ₗ[H] P} : f = g ↔ ∀ (m : M) (n : N), f (tmul R H m n) = g (tmul R H m n)

@[simp]

theorem TauCeti.BialgebraModule.tensorEquiv_smul (R : Type u_1) (H : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] (h : H) (x : Tensor R H M N) : (tensorEquiv R H M N) (h • x) = ((tensorAction R H M N) h) ((tensorEquiv R H M N) x)

The underlying equivalence expresses the action through the coproduct representation.

theorem TauCeti.BialgebraModule.tensorEquiv_smul_of_comul_eq_tmul {R : Type u_1} {H : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {a : H} (ha : CoalgebraStruct.comul a = a ⊗ₜ[R] a) (x : Tensor R H M N) : (tensorEquiv R H M N) (a • x) = (TensorProduct.map ((Algebra.lsmul R R M) a) ((Algebra.lsmul R R N) a)) ((tensorEquiv R H M N) x)

An element with coproduct a ⊗ a acts on the coproduct tensor product as the tensor product of its actions on the two factors.

noncomputable def TauCeti.BialgebraModule.tensorMap (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {M' : Type u_5} {N' : Type u_6} [AddCommMonoid M'] [Module R M'] [Module H M'] [IsScalarTower R H M'] [AddCommMonoid N'] [Module R N'] [Module H N'] [IsScalarTower R H N'] (f : M →ₗ[H] M') (g : N →ₗ[H] N') : Tensor R H M N →ₗ[H] Tensor R H M' N'

The tensor product of native H-linear intertwiners, for the coproduct actions.

@[simp]

theorem TauCeti.BialgebraModule.tensorEquiv_tensorMap (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {M' : Type u_5} {N' : Type u_6} [AddCommMonoid M'] [Module R M'] [Module H M'] [IsScalarTower R H M'] [AddCommMonoid N'] [Module R N'] [Module H N'] [IsScalarTower R H N'] (f : M →ₗ[H] M') (g : N →ₗ[H] N') (x : Tensor R H M N) : (tensorEquiv R H M' N') ((tensorMap R H f g) x) = (TensorProduct.map (↑R f) (↑R g)) ((tensorEquiv R H M N) x)

The underlying map of a tensor intertwiner is the native tensor product of maps.

@[simp]

theorem TauCeti.BialgebraModule.tensorMap_tmul (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {M' : Type u_5} {N' : Type u_6} [AddCommMonoid M'] [Module R M'] [Module H M'] [IsScalarTower R H M'] [AddCommMonoid N'] [Module R N'] [Module H N'] [IsScalarTower R H N'] (f : M →ₗ[H] M') (g : N →ₗ[H] N') (m : M) (n : N) : (tensorMap R H f g) (tmul R H m n) = tmul R H (f m) (g n)

A tensor intertwiner acts on pure tensors by its two component maps.

@[simp]

theorem TauCeti.BialgebraModule.tensorMap_id (R : Type u_1) (H : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] : tensorMap R H LinearMap.id LinearMap.id = LinearMap.id

Tensoring the identity intertwiners gives the identity.

@[simp]

theorem TauCeti.BialgebraModule.tensorMap_zero_left (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {M' : Type u_5} {N' : Type u_6} [AddCommMonoid M'] [Module R M'] [Module H M'] [IsScalarTower R H M'] [AddCommMonoid N'] [Module R N'] [Module H N'] [IsScalarTower R H N'] (g : N →ₗ[H] N') : tensorMap R H 0 g = 0

Tensoring with the zero intertwiner on the left gives zero.

@[simp]

theorem TauCeti.BialgebraModule.tensorMap_zero_right (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {M' : Type u_5} {N' : Type u_6} [AddCommMonoid M'] [Module R M'] [Module H M'] [IsScalarTower R H M'] [AddCommMonoid N'] [Module R N'] [Module H N'] [IsScalarTower R H N'] (f : M →ₗ[H] M') : tensorMap R H f 0 = 0

Tensoring with the zero intertwiner on the right gives zero.

@[simp]

theorem TauCeti.BialgebraModule.tensorMap_add_left (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {M' : Type u_5} {N' : Type u_6} [AddCommMonoid M'] [Module R M'] [Module H M'] [IsScalarTower R H M'] [AddCommMonoid N'] [Module R N'] [Module H N'] [IsScalarTower R H N'] (f₁ f₂ : M →ₗ[H] M') (g : N →ₗ[H] N') : tensorMap R H (f₁ + f₂) g = tensorMap R H f₁ g + tensorMap R H f₂ g

tensorMap is additive in its left intertwiner argument.

@[simp]

theorem TauCeti.BialgebraModule.tensorMap_add_right (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {M' : Type u_5} {N' : Type u_6} [AddCommMonoid M'] [Module R M'] [Module H M'] [IsScalarTower R H M'] [AddCommMonoid N'] [Module R N'] [Module H N'] [IsScalarTower R H N'] (f : M →ₗ[H] M') (g₁ g₂ : N →ₗ[H] N') : tensorMap R H f (g₁ + g₂) = tensorMap R H f g₁ + tensorMap R H f g₂

tensorMap is additive in its right intertwiner argument.

theorem TauCeti.BialgebraModule.tensorMap_sum_left (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {M' : Type u_5} {N' : Type u_6} [AddCommMonoid M'] [Module R M'] [Module H M'] [IsScalarTower R H M'] [AddCommMonoid N'] [Module R N'] [Module H N'] [IsScalarTower R H N'] {ι : Type u_7} (s : Finset ι) (f : ι → M →ₗ[H] M') (g : N →ₗ[H] N') : tensorMap R H (∑ i ∈ s, f i) g = ∑ i ∈ s, tensorMap R H (f i) g

tensorMap commutes with finite sums in its left intertwiner argument.

theorem TauCeti.BialgebraModule.tensorMap_sum_right (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {M' : Type u_5} {N' : Type u_6} [AddCommMonoid M'] [Module R M'] [Module H M'] [IsScalarTower R H M'] [AddCommMonoid N'] [Module R N'] [Module H N'] [IsScalarTower R H N'] {ι : Type u_7} (s : Finset ι) (f : M →ₗ[H] M') (g : ι → N →ₗ[H] N') : tensorMap R H f (∑ i ∈ s, g i) = ∑ i ∈ s, tensorMap R H f (g i)

tensorMap commutes with finite sums in its right intertwiner argument.

@[simp]

theorem TauCeti.BialgebraModule.tensorMap_comp (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {M' : Type u_5} {N' : Type u_6} [AddCommMonoid M'] [Module R M'] [Module H M'] [IsScalarTower R H M'] [AddCommMonoid N'] [Module R N'] [Module H N'] [IsScalarTower R H N'] {M'' : Type u_7} {N'' : Type u_8} [AddCommMonoid M''] [Module R M''] [Module H M''] [IsScalarTower R H M''] [AddCommMonoid N''] [Module R N''] [Module H N''] [IsScalarTower R H N''] (f : M →ₗ[H] M') (f' : M' →ₗ[H] M'') (g : N →ₗ[H] N') (g' : N' →ₗ[H] N'') : tensorMap R H (f' ∘ₗ f) (g' ∘ₗ g) = tensorMap R H f' g' ∘ₗ tensorMap R H f g

Tensor products of intertwiners preserve composition.

noncomputable def TauCeti.BialgebraModule.tensorCongr (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {M' : Type u_5} {N' : Type u_6} [AddCommMonoid M'] [Module R M'] [Module H M'] [IsScalarTower R H M'] [AddCommMonoid N'] [Module R N'] [Module H N'] [IsScalarTower R H N'] (f : M ≃ₗ[H] M') (g : N ≃ₗ[H] N') : Tensor R H M N ≃ₗ[H] Tensor R H M' N'

Tensor products of module isomorphisms, for the coproduct actions.

@[simp]

theorem TauCeti.BialgebraModule.toLinearMap_tensorCongr (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {M' : Type u_5} {N' : Type u_6} [AddCommMonoid M'] [Module R M'] [Module H M'] [IsScalarTower R H M'] [AddCommMonoid N'] [Module R N'] [Module H N'] [IsScalarTower R H N'] (f : M ≃ₗ[H] M') (g : N ≃ₗ[H] N') : ↑(tensorCongr R H f g) = tensorMap R H ↑f ↑g

The underlying linear map of a tensor isomorphism is the tensor product of the maps.

@[simp]

theorem TauCeti.BialgebraModule.tensorCongr_symm (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {M' : Type u_5} {N' : Type u_6} [AddCommMonoid M'] [Module R M'] [Module H M'] [IsScalarTower R H M'] [AddCommMonoid N'] [Module R N'] [Module H N'] [IsScalarTower R H N'] (f : M ≃ₗ[H] M') (g : N ≃ₗ[H] N') : (tensorCongr R H f g).symm = tensorCongr R H f.symm g.symm

Inverting a tensor isomorphism tensors the inverse isomorphisms.

@[simp]

theorem TauCeti.BialgebraModule.tensorCongr_refl (R : Type u_1) (H : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] : tensorCongr R H (LinearEquiv.refl H M) (LinearEquiv.refl H N) = LinearEquiv.refl H (Tensor R H M N)

Tensoring identity isomorphisms gives the identity isomorphism.

theorem TauCeti.BialgebraModule.tensorCongr_trans (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {M' : Type u_5} {N' : Type u_6} [AddCommMonoid M'] [Module R M'] [Module H M'] [IsScalarTower R H M'] [AddCommMonoid N'] [Module R N'] [Module H N'] [IsScalarTower R H N'] {M'' : Type u_7} {N'' : Type u_8} [AddCommMonoid M''] [Module R M''] [Module H M''] [IsScalarTower R H M''] [AddCommMonoid N''] [Module R N''] [Module H N''] [IsScalarTower R H N''] (f : M ≃ₗ[H] M') (f' : M' ≃ₗ[H] M'') (g : N ≃ₗ[H] N') (g' : N' ≃ₗ[H] N'') : tensorCongr R H (f ≪≫ₗ f') (g ≪≫ₗ g') = tensorCongr R H f g ≪≫ₗ tensorCongr R H f' g'

Tensor products of module isomorphisms preserve composition.

theorem TauCeti.BialgebraModule.tensorCongr_apply (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {M' : Type u_5} {N' : Type u_6} [AddCommMonoid M'] [Module R M'] [Module H M'] [IsScalarTower R H M'] [AddCommMonoid N'] [Module R N'] [Module H N'] [IsScalarTower R H N'] (f : M ≃ₗ[H] M') (g : N ≃ₗ[H] N') (x : Tensor R H M N) : (tensorCongr R H f g) x = (tensorMap R H ↑f ↑g) x

The tensor isomorphism has underlying map the tensor product of the two maps.

@[simp]

theorem TauCeti.BialgebraModule.tensorCongr_tmul (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {M' : Type u_5} {N' : Type u_6} [AddCommMonoid M'] [Module R M'] [Module H M'] [IsScalarTower R H M'] [AddCommMonoid N'] [Module R N'] [Module H N'] [IsScalarTower R H N'] (f : M ≃ₗ[H] M') (g : N ≃ₗ[H] N') (m : M) (n : N) : (tensorCongr R H f g) (tmul R H m n) = tmul R H (f m) (g n)

Tensor products of isomorphisms act componentwise on pure tensors.

noncomputable def TauCeti.BialgebraModule.assoc (R : Type u_1) (H : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] (P : Type u_5) [AddCommMonoid P] [Module R P] [Module H P] [IsScalarTower R H P] : Tensor R H (Tensor R H M N) P ≃ₗ[H] Tensor R H M (Tensor R H N P)

The associativity equivalence of coproduct tensor products. It is H-linear because the coproduct is coassociative.

theorem TauCeti.BialgebraModule.tensorEquiv_assoc (R : Type u_1) (H : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] (P : Type u_5) [AddCommMonoid P] [Module R P] [Module H P] [IsScalarTower R H P] (x : Tensor R H (Tensor R H M N) P) : (tensorEquiv R H M (Tensor R H N P)) ((assoc R H M N P) x) = (TensorProduct.map LinearMap.id ↑(tensorEquiv R H N P).symm) ((TensorProduct.assoc R M N P) ((TensorProduct.map (↑(tensorEquiv R H M N)) LinearMap.id) ((tensorEquiv R H (Tensor R H M N) P) x)))

Underneath, the associativity equivalence is the associativity equivalence of native tensor products.

@[simp]

theorem TauCeti.BialgebraModule.assoc_tmul (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {P : Type u_5} [AddCommMonoid P] [Module R P] [Module H P] [IsScalarTower R H P] (m : M) (n : N) (p : P) : (assoc R H M N P) (tmul R H (tmul R H m n) p) = tmul R H m (tmul R H n p)

The associativity equivalence reassociates pure tensors.

@[simp]

theorem TauCeti.BialgebraModule.assoc_symm_tmul (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {P : Type u_5} [AddCommMonoid P] [Module R P] [Module H P] [IsScalarTower R H P] (m : M) (n : N) (p : P) : (assoc R H M N P).symm (tmul R H m (tmul R H n p)) = tmul R H (tmul R H m n) p

The inverse associativity equivalence reassociates pure tensors.

theorem TauCeti.BialgebraModule.tensorMap_tensorMap_comp_assoc (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {P : Type u_5} [AddCommMonoid P] [Module R P] [Module H P] [IsScalarTower R H P] {M' : Type u_6} {N' : Type u_7} {P' : Type u_8} [AddCommMonoid M'] [Module R M'] [Module H M'] [IsScalarTower R H M'] [AddCommMonoid N'] [Module R N'] [Module H N'] [IsScalarTower R H N'] [AddCommMonoid P'] [Module R P'] [Module H P'] [IsScalarTower R H P'] (f : M →ₗ[H] M') (g : N →ₗ[H] N') (h : P →ₗ[H] P') : tensorMap R H f (tensorMap R H g h) ∘ₗ ↑(assoc R H M N P) = ↑(assoc R H M' N' P') ∘ₗ tensorMap R H (tensorMap R H f g) h

The associativity equivalence is natural in all three module factors.

theorem TauCeti.BialgebraModule.tensorMap_tensorMap_assoc (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {P : Type u_5} [AddCommMonoid P] [Module R P] [Module H P] [IsScalarTower R H P] {M' : Type u_6} {N' : Type u_7} {P' : Type u_8} [AddCommMonoid M'] [Module R M'] [Module H M'] [IsScalarTower R H M'] [AddCommMonoid N'] [Module R N'] [Module H N'] [IsScalarTower R H N'] [AddCommMonoid P'] [Module R P'] [Module H P'] [IsScalarTower R H P'] (f : M →ₗ[H] M') (g : N →ₗ[H] N') (h : P →ₗ[H] P') (x : Tensor R H (Tensor R H M N) P) : (tensorMap R H f (tensorMap R H g h)) ((assoc R H M N P) x) = (assoc R H M' N' P') ((tensorMap R H (tensorMap R H f g) h) x)

Pointwise naturality of the associativity equivalence with respect to tensorMap.

theorem TauCeti.BialgebraModule.tensorMap_tensorMap_comp_assoc_symm (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {P : Type u_5} [AddCommMonoid P] [Module R P] [Module H P] [IsScalarTower R H P] {M' : Type u_6} {N' : Type u_7} {P' : Type u_8} [AddCommMonoid M'] [Module R M'] [Module H M'] [IsScalarTower R H M'] [AddCommMonoid N'] [Module R N'] [Module H N'] [IsScalarTower R H N'] [AddCommMonoid P'] [Module R P'] [Module H P'] [IsScalarTower R H P'] (f : M →ₗ[H] M') (g : N →ₗ[H] N') (h : P →ₗ[H] P') : tensorMap R H (tensorMap R H f g) h ∘ₗ ↑(assoc R H M N P).symm = ↑(assoc R H M' N' P').symm ∘ₗ tensorMap R H f (tensorMap R H g h)

The inverse associativity equivalence is natural in all three module factors.

theorem TauCeti.BialgebraModule.tensorMap_tensorMap_assoc_symm (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {P : Type u_5} [AddCommMonoid P] [Module R P] [Module H P] [IsScalarTower R H P] {M' : Type u_6} {N' : Type u_7} {P' : Type u_8} [AddCommMonoid M'] [Module R M'] [Module H M'] [IsScalarTower R H M'] [AddCommMonoid N'] [Module R N'] [Module H N'] [IsScalarTower R H N'] [AddCommMonoid P'] [Module R P'] [Module H P'] [IsScalarTower R H P'] (f : M →ₗ[H] M') (g : N →ₗ[H] N') (h : P →ₗ[H] P') (x : Tensor R H M (Tensor R H N P)) : (tensorMap R H (tensorMap R H f g) h) ((assoc R H M N P).symm x) = (assoc R H M' N' P').symm ((tensorMap R H f (tensorMap R H g h)) x)

Pointwise naturality of the inverse associativity equivalence with respect to tensorMap.

theorem TauCeti.BialgebraModule.assoc_pentagon (R : Type u_1) (H : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] (P : Type u_5) [AddCommMonoid P] [Module R P] [Module H P] [IsScalarTower R H P] (Q : Type u_6) [AddCommMonoid Q] [Module R Q] [Module H Q] [IsScalarTower R H Q] : assoc R H (Tensor R H M N) P Q ≪≫ₗ assoc R H M N (Tensor R H P Q) = tensorCongr R H (assoc R H M N P) (LinearEquiv.refl H Q) ≪≫ₗ assoc R H M (Tensor R H N P) Q ≪≫ₗ tensorCongr R H (LinearEquiv.refl H M) (assoc R H N P Q)

Mac Lane's pentagon identity for the coproduct tensor associativity equivalence: the two ways of reassociating ((M ⊗ N) ⊗ P) ⊗ Q into M ⊗ (N ⊗ (P ⊗ Q)) agree.

theorem TauCeti.BialgebraModule.assoc_pentagon_apply (R : Type u_1) (H : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] [Module H N] [IsScalarTower R H N] {P : Type u_5} [AddCommMonoid P] [Module R P] [Module H P] [IsScalarTower R H P] {Q : Type u_6} [AddCommMonoid Q] [Module R Q] [Module H Q] [IsScalarTower R H Q] (x : Tensor R H (Tensor R H (Tensor R H M N) P) Q) : (assoc R H M N (Tensor R H P Q)) ((assoc R H (Tensor R H M N) P Q) x) = (tensorMap R H LinearMap.id ↑(assoc R H N P Q)) ((assoc R H M (Tensor R H N P) Q) ((tensorMap R H (↑(assoc R H M N P)) LinearMap.id) x))

Pointwise form of Mac Lane's pentagon identity for BialgebraModule.assoc.

def TauCeti.BialgebraModule.Trivial (R : Type u_5) (_H : Type u_6) : Type u_5

The base semiring R, with a separate carrier for the action of H through its counit.

This trivial module is the unit for the coproduct tensor product. As for Tensor, the base action is restriction of the H-action along the algebra map, and trivialEquiv identifies it with the native action of R on itself.

@[instance_reducible]

noncomputable instance TauCeti.BialgebraModule.instAddCommMonoidTrivial (R : Type u_1) (H : Type u_2) [CommSemiring R] : AddCommMonoid (Trivial R H)

@[instance_reducible]

noncomputable instance TauCeti.BialgebraModule.instAddCommGroupTrivialOfCommRing (R : Type u_5) (H : Type u_6) [CommRing R] : AddCommGroup (Trivial R H)

@[instance_reducible]

noncomputable instance TauCeti.BialgebraModule.instModuleTrivial (R : Type u_1) (H : Type u_2) [CommSemiring R] [Semiring H] [Bialgebra R H] : Module H (Trivial R H)

The action of H on the trivial module, through the counit.

@[instance_reducible, instance 1100]

noncomputable instance TauCeti.BialgebraModule.instModuleTrivial_1 (R : Type u_1) (H : Type u_2) [CommSemiring R] [Semiring H] [Bialgebra R H] : Module R (Trivial R H)

The base action on the trivial module is restriction of the counit action along the algebra map.

instance TauCeti.BialgebraModule.instIsScalarTowerTrivial (R : Type u_1) (H : Type u_2) [CommSemiring R] [Semiring H] [Bialgebra R H] : IsScalarTower R H (Trivial R H)

The counit module is compatible with its base scalar action.

noncomputable def TauCeti.BialgebraModule.trivialEquiv (R : Type u_1) (H : Type u_2) [CommSemiring R] [Semiring H] [Bialgebra R H] : Trivial R H ≃ₗ[R] R

The underlying R-linear identification of the trivial module with R.

@[simp]

theorem TauCeti.BialgebraModule.trivialEquiv_smul (R : Type u_1) (H : Type u_2) [CommSemiring R] [Semiring H] [Bialgebra R H] (h : H) (x : Trivial R H) : (trivialEquiv R H) (h • x) = CoalgebraStruct.counit h * (trivialEquiv R H) x

An element of H acts on the trivial module by multiplication by its counit.

instance TauCeti.BialgebraModule.instFiniteTrivial (R : Type u_1) (H : Type u_2) [CommSemiring R] [Semiring H] [Bialgebra R H] : Module.Finite R (Trivial R H)

The trivial module is finite over the base.

noncomputable def TauCeti.BialgebraModule.lid (R : Type u_1) (H : Type u_2) (M : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] : Tensor R H (Trivial R H) M ≃ₗ[H] M

The left unit equivalence of the coproduct tensor product. It is H-linear by the left counit law.

theorem TauCeti.BialgebraModule.lid_apply (R : Type u_1) (H : Type u_2) (M : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] (x : Tensor R H (Trivial R H) M) : (lid R H M) x = (TensorProduct.lid R M) ((TensorProduct.map (↑(trivialEquiv R H)) LinearMap.id) ((tensorEquiv R H (Trivial R H) M) x))

Underneath, the left unit equivalence is the native left unit equivalence.

@[simp]

theorem TauCeti.BialgebraModule.lid_tmul (R : Type u_1) (H : Type u_2) {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] (r : Trivial R H) (m : M) : (lid R H M) (tmul R H r m) = (trivialEquiv R H) r • m

The left unit equivalence scales by the trivial factor.

@[simp]

theorem TauCeti.BialgebraModule.lid_symm_apply (R : Type u_1) (H : Type u_2) {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] (m : M) : (lid R H M).symm m = tmul R H ((trivialEquiv R H).symm 1) m

The inverse left unit equivalence inserts the unit of the trivial module.

noncomputable def TauCeti.BialgebraModule.rid (R : Type u_1) (H : Type u_2) (M : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] : Tensor R H M (Trivial R H) ≃ₗ[H] M

The right unit equivalence of the coproduct tensor product. It is H-linear by the right counit law.

theorem TauCeti.BialgebraModule.rid_apply (R : Type u_1) (H : Type u_2) (M : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] (x : Tensor R H M (Trivial R H)) : (rid R H M) x = (TensorProduct.rid R M) ((TensorProduct.map LinearMap.id ↑(trivialEquiv R H)) ((tensorEquiv R H M (Trivial R H)) x))

Underneath, the right unit equivalence is the native right unit equivalence.

@[simp]

theorem TauCeti.BialgebraModule.rid_tmul (R : Type u_1) (H : Type u_2) {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] (m : M) (r : Trivial R H) : (rid R H M) (tmul R H m r) = (trivialEquiv R H) r • m

The right unit equivalence scales by the trivial factor.

@[simp]

theorem TauCeti.BialgebraModule.rid_symm_apply (R : Type u_1) (H : Type u_2) {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring H] [Bialgebra R H] [Module H M] [IsScalarTower R H M] (m : M) : (rid R H M).symm m = tmul R H m ((trivialEquiv R H).symm 1)

The inverse right unit equivalence inserts the unit of the trivial module.