feat: comultiplication as a bialgebra hom

Mathlib/RingTheory/Bialgebra/TensorProduct.lean

@@ -18,16 +18,19 @@ instance on a tensor product of bialgebras, and the tensor product of two `Bialg
 
 -/
 
-@[expose] public section
+public noncomputable 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,14 +63,13 @@ 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]
 
 /-- The tensor product of two bialgebra morphisms as a bialgebra morphism. -/
-noncomputable def map (f : A →ₐc[S] C) (g : B →ₐc[R] D) :
-    A ⊗[R] B →ₐc[S] C ⊗[R] D :=
+@[expose] def map (f : A →ₐc[S] C) (g : B →ₐc[R] D) : A ⊗[R] B →ₐc[S] C ⊗[R] D :=
   { Coalgebra.TensorProduct.map (f : A →ₗc[S] C) (g : B →ₗc[R] D),
     Algebra.TensorProduct.map (f : A →ₐ[S] C) (g : B →ₐ[R] D) with }
 
@@ -88,8 +90,7 @@ theorem map_toAlgHom (f : A →ₐc[S] C) (g : B →ₐc[R] D) :
 
 variable (R S A C D) in
 /-- The associator for tensor products of R-bialgebras, as a bialgebra equivalence. -/
-protected noncomputable def assoc :
-    (A ⊗[S] C) ⊗[R] D ≃ₐc[S] A ⊗[S] (C ⊗[R] D) :=
+@[expose] protected def assoc : (A ⊗[S] C) ⊗[R] D ≃ₐc[S] A ⊗[S] (C ⊗[R] D) :=
   { Coalgebra.TensorProduct.assoc R S A C D, Algebra.TensorProduct.assoc R S S A C D with }
 
 @[simp]
@@ -115,7 +116,7 @@ theorem assoc_toAlgEquiv :
 variable (R B) in
 /-- The base ring is a left identity for the tensor product of bialgebras, up to
 bialgebra equivalence. -/
-protected noncomputable def lid : R ⊗[R] B ≃ₐc[R] B :=
+@[expose] protected def lid : R ⊗[R] B ≃ₐc[R] B :=
   { Coalgebra.TensorProduct.lid R B, Algebra.TensorProduct.lid R B with }
 
 @[simp]
@@ -138,7 +139,7 @@ theorem coalgebra_rid_eq_algebra_rid_apply (x : A ⊗[R] R) :
 variable (R S A) in
 /-- The base ring is a right identity for the tensor product of bialgebras, up to
 bialgebra equivalence. -/
-protected noncomputable def rid : A ⊗[R] R ≃ₐc[S] A where
+@[expose] protected def rid : A ⊗[R] R ≃ₐc[S] A where
   toCoalgEquiv := Coalgebra.TensorProduct.rid R S A
   map_mul' x y := by
     simp only [CoalgEquiv.toCoalgHom_eq_coe, CoalgHom.toLinearMap_eq_coe, AddHom.toFun_eq_coe,
@@ -161,7 +162,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. -/
+@[expose] 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]
@@ -170,11 +187,25 @@ variable {R A B C : Type*} [CommRing R] [Ring A] [Ring B] [Ring C]
 variable (A)
 
 /-- `lTensor A f : A ⊗ B →ₐc A ⊗ C` is the natural bialgebra morphism induced by `f : B →ₐc C`. -/
-noncomputable abbrev lTensor (f : B →ₐc[R] C) : A ⊗[R] B →ₐc[R] A ⊗[R] C :=
+abbrev lTensor (f : B →ₐc[R] C) : A ⊗[R] B →ₐc[R] A ⊗[R] C :=
   Bialgebra.TensorProduct.map (BialgHom.id R A) f
 
 /-- `rTensor A f : B ⊗ A →ₐc C ⊗ A` is the natural bialgebra morphism induced by `f : B →ₐc C`. -/
-noncomputable abbrev rTensor (f : B →ₐc[R] C) : B ⊗[R] A →ₐc[R] C ⊗[R] A :=
+abbrev rTensor (f : B →ₐc[R] C) : B ⊗[R] A →ₐc[R] C ⊗[R] A :=
   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. -/
+@[expose] 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