feat: comultiplication as a bialgebra hom

From toric

Author: YaelDillies

Mathlib/RingTheory/Bialgebra/TensorProduct.lean

@@ -20,14 +20,17 @@ instance on a tensor product of bialgebras, and the tensor product of two `Bialg
 
 @[expose] public section
 
+open Coalgebra
 open scoped TensorProduct
 
 namespace Bialgebra.TensorProduct
 
 open Coalgebra.TensorProduct
 
-variable (R S A B C D : Type*) [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B]
-  [Bialgebra S A] [Bialgebra R B] [Algebra R A] [Algebra R S] [IsScalarTower R S A]
+variable {R S A B C D : Type*} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B]
+
+section Heterogeneous
+variable (R S A B) [Bialgebra S A] [Bialgebra R B] [Algebra R A] [Algebra R S] [IsScalarTower R S A]
 
 lemma counit_eq_algHom_toLinearMap :
     Coalgebra.counit (R := S) (A := A ⊗[R] B) =
@@ -60,7 +63,7 @@ lemma comulAlgHom_def :
         (Algebra.TensorProduct.map (Bialgebra.comulAlgHom S A)
         (Bialgebra.comulAlgHom R B)) := rfl
 
-variable {R S A B C D}
+variable {R S A B}
 
 variable [Semiring C] [Semiring D] [Bialgebra S C]
   [Bialgebra R D] [Algebra R C] [IsScalarTower R S C]
@@ -161,7 +164,23 @@ theorem rid_tmul (r : R) (a : A) : Bialgebra.TensorProduct.rid R S A (a ⊗ₜ r
 @[simp]
 theorem rid_symm_apply (a : A) : (Bialgebra.TensorProduct.rid R S A).symm a = a ⊗ₜ 1 := rfl
 
+end Heterogeneous
+
+section Homogeneous
+variable (R S A B) [Bialgebra R A] [Bialgebra R B]
+
+/-- The tensor product of `R`-bialgebras is commutative, up to bialgebra isomorphism. -/
+def comm : A ⊗[R] B ≃ₐc[R] B ⊗[R] A :=
+  .ofAlgEquiv (Algebra.TensorProduct.comm R A B) (by ext <;> simp) <| by
+    ext a <;>
+    · dsimp
+      rw [← (ℛ R a).eq]
+      simp [TensorProduct.tmul_sum, TensorProduct.sum_tmul]
+      rfl
+
+end Homogeneous
 end Bialgebra.TensorProduct
+
 namespace BialgHom
 
 variable {R A B C : Type*} [CommRing R] [Ring A] [Ring B] [Ring C]
@@ -178,3 +197,17 @@ noncomputable abbrev rTensor (f : B →ₐc[R] C) : B ⊗[R] A →ₐc[R] C ⊗[
   Bialgebra.TensorProduct.map f (BialgHom.id R A)
 
 end BialgHom
+
+namespace Bialgebra
+variable (R A : Type*) [CommSemiring R] [Semiring A] [Bialgebra R A]
+
+/-- Comultiplication as a bialgebra hom. -/
+def comulBialgHom [IsCocomm R A] : A →ₐc[R] A ⊗[R] A where
+  __ := comulAlgHom R A
+  __ := comulCoalgHom R A
+
+lemma comm_comp_comulBialgHom [IsCocomm R A] :
+    (TensorProduct.comm R A A).toBialgHom.comp (comulBialgHom R A) = comulBialgHom R A := by
+  ext; exact comm_comul _ _
+
+end Bialgebra

Mathlib/RingTheory/Coalgebra/TensorProduct.lean

@@ -8,6 +8,10 @@ module
 public import Mathlib.LinearAlgebra.TensorProduct.Tower
 public import Mathlib.RingTheory.Coalgebra.Equiv
 
+meta import Mathlib.RingTheory.Coalgebra.CoassocSimps
+
+import Mathlib.Algebra.Algebra.Bilinear
+
 /-!
 # Tensor products of coalgebras
 
@@ -295,3 +299,28 @@ noncomputable abbrev rTensor (f : N →ₗc[R] P) : N ⊗[R] M →ₗc[R] P ⊗[
   Coalgebra.TensorProduct.map f (CoalgHom.id R M)
 
 end CoalgHom
+
+namespace Coalgebra
+variable {R C : Type*} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C]
+  [IsCocomm R C]
+
+local notation3 "ε" => counit (R := R) (A := C)
+local notation3 "μ" => LinearMap.mul' R R
+local notation3 "δ" => comul (R := R)
+local infix:90 " ◁ " => LinearMap.lTensor
+local notation3:90 f:90 " ▷ " X:90 => LinearMap.rTensor X f
+local infix:70 " ⊗ₘ " => _root_.TensorProduct.map
+
+variable (R C) in
+/-- Comultiplication as a coalgebra hom. -/
+noncomputable def comulCoalgHom : C →ₗc[R] C ⊗[R] C where
+  __ := δ
+  counit_comp := by
+    simp only [counit_def, AlgebraTensorModule.rid_eq_rid, ← lid_eq_rid]
+    calc
+        (μ ∘ₗ (ε ⊗ₘ ε)) ∘ₗ δ
+    _ = (μ ∘ₗ ε ▷ R) ∘ₗ (C ◁ ε ∘ₗ δ) := by simp [coassoc_simps]
+    _ = ε := by ext; simp
+  map_comp_comul := by simp [comul_def, coassoc_simps]
+
+end Coalgebra