Coproduct tensors and finite products

Tensoring a finite product of modules over a bialgebra distributes over that product. The underlying equivalences are Mathlib's TensorProduct.piLeft and TensorProduct.piRight; the component maps are tensor products of module projections. These equivalences let one iterate finite module decompositions without losing the coproduct action.

noncomputable def TauCeti.BialgebraModule.piLeft (R : Type u_1) (H : Type u_2) [CommSemiring R] [Semiring H] [Bialgebra R H] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (M : ι → Type u_4) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → Module H (M i)] [∀ (i : ι), IsScalarTower R H (M i)] (N : Type u_5) [AddCommMonoid N] [Module R N] [Module H N] [IsScalarTower R H N] : Tensor R H ((i : ι) → M i) N ≃ₗ[H] (i : ι) → Tensor R H (M i) N

Coproduct tensor products distribute over finite products in their left factor.

theorem TauCeti.BialgebraModule.piLeft_apply (R : Type u_1) (H : Type u_2) [CommSemiring R] [Semiring H] [Bialgebra R H] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (M : ι → Type u_4) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → Module H (M i)] [∀ (i : ι), IsScalarTower R H (M i)] (N : Type u_5) [AddCommMonoid N] [Module R N] [Module H N] [IsScalarTower R H N] (x : Tensor R H ((i : ι) → M i) N) (i : ι) : (piLeft R H M N) x i = (tensorMap R H (LinearMap.proj i) LinearMap.id) x

Each component of piLeft is the tensor product of the corresponding projection with the identity.

@[simp]

theorem TauCeti.BialgebraModule.piLeft_tmul (R : Type u_1) (H : Type u_2) [CommSemiring R] [Semiring H] [Bialgebra R H] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (M : ι → Type u_4) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → Module H (M i)] [∀ (i : ι), IsScalarTower R H (M i)] (N : Type u_5) [AddCommMonoid N] [Module R N] [Module H N] [IsScalarTower R H N] (m : (i : ι) → M i) (n : N) (i : ι) : (piLeft R H M N) (tmul R H m n) i = tmul R H (m i) n

The finite-product comparison evaluates pure tensors componentwise.

@[simp]

theorem TauCeti.BialgebraModule.piLeft_symm_single_tmul (R : Type u_1) (H : Type u_2) [CommSemiring R] [Semiring H] [Bialgebra R H] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (M : ι → Type u_4) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → Module H (M i)] [∀ (i : ι), IsScalarTower R H (M i)] (N : Type u_5) [AddCommMonoid N] [Module R N] [Module H N] [IsScalarTower R H N] (i : ι) (m : M i) (n : N) : (piLeft R H M N).symm (Pi.single i (tmul R H m n)) = tmul R H (Pi.single i m) n

The inverse comparison inserts a pure tensor into one product component.

theorem TauCeti.BialgebraModule.piLeft_symm_single (R : Type u_1) (H : Type u_2) [CommSemiring R] [Semiring H] [Bialgebra R H] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (M : ι → Type u_4) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → Module H (M i)] [∀ (i : ι), IsScalarTower R H (M i)] (N : Type u_5) [AddCommMonoid N] [Module R N] [Module H N] [IsScalarTower R H N] (i : ι) (x : Tensor R H (M i) N) : (piLeft R H M N).symm (Pi.single i x) = (tensorMap R H (LinearMap.single H M i) LinearMap.id) x

The inverse left comparison inserts an arbitrary tensor into one component.

noncomputable def TauCeti.BialgebraModule.piRight (R : Type u_1) (H : Type u_2) [CommSemiring R] [Semiring H] [Bialgebra R H] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (M : ι → Type u_4) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → Module H (M i)] [∀ (i : ι), IsScalarTower R H (M i)] (N : Type u_5) [AddCommMonoid N] [Module R N] [Module H N] [IsScalarTower R H N] : Tensor R H N ((i : ι) → M i) ≃ₗ[H] (i : ι) → Tensor R H N (M i)

Coproduct tensor products distribute over finite products in their right factor.

theorem TauCeti.BialgebraModule.piRight_apply (R : Type u_1) (H : Type u_2) [CommSemiring R] [Semiring H] [Bialgebra R H] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (M : ι → Type u_4) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → Module H (M i)] [∀ (i : ι), IsScalarTower R H (M i)] (N : Type u_5) [AddCommMonoid N] [Module R N] [Module H N] [IsScalarTower R H N] (x : Tensor R H N ((i : ι) → M i)) (i : ι) : (piRight R H M N) x i = (tensorMap R H LinearMap.id (LinearMap.proj i)) x

Each component of piRight is the tensor product of the identity with the corresponding projection.

@[simp]

theorem TauCeti.BialgebraModule.piRight_tmul (R : Type u_1) (H : Type u_2) [CommSemiring R] [Semiring H] [Bialgebra R H] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (M : ι → Type u_4) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → Module H (M i)] [∀ (i : ι), IsScalarTower R H (M i)] (N : Type u_5) [AddCommMonoid N] [Module R N] [Module H N] [IsScalarTower R H N] (n : N) (m : (i : ι) → M i) (i : ι) : (piRight R H M N) (tmul R H n m) i = tmul R H n (m i)

The finite-product comparison evaluates pure tensors componentwise.

@[simp]

theorem TauCeti.BialgebraModule.piRight_symm_single_tmul (R : Type u_1) (H : Type u_2) [CommSemiring R] [Semiring H] [Bialgebra R H] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (M : ι → Type u_4) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → Module H (M i)] [∀ (i : ι), IsScalarTower R H (M i)] (N : Type u_5) [AddCommMonoid N] [Module R N] [Module H N] [IsScalarTower R H N] (i : ι) (n : N) (m : M i) : (piRight R H M N).symm (Pi.single i (tmul R H n m)) = tmul R H n (Pi.single i m)

The inverse comparison inserts a pure tensor into one product component.

theorem TauCeti.BialgebraModule.piRight_symm_single (R : Type u_1) (H : Type u_2) [CommSemiring R] [Semiring H] [Bialgebra R H] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (M : ι → Type u_4) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → Module H (M i)] [∀ (i : ι), IsScalarTower R H (M i)] (N : Type u_5) [AddCommMonoid N] [Module R N] [Module H N] [IsScalarTower R H N] (i : ι) (x : Tensor R H N (M i)) : (piRight R H M N).symm (Pi.single i x) = (tensorMap R H LinearMap.id (LinearMap.single H M i)) x

The inverse right comparison inserts an arbitrary tensor into one component.