From f6eef405fd61c49b3aac5e9373417ec62924d110 Mon Sep 17 00:00:00 2001
From: Nikolas Tapia <tapia@wias-berlin.de>
Date: Tue, 11 Nov 2025 12:46:35 -0300
Subject: [PATCH 01/23] feat(TensorAlgebra/Hopf): implement HopfAlgebraStruct
 for TensorAlgebra

---
 Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean | 99 +++++++++++++++++++
 1 file changed, 99 insertions(+)
 create mode 100644 Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean

diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
new file mode 100644
index 00000000000000..c2792bc7e2c36a
--- /dev/null
+++ b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
@@ -0,0 +1,99 @@
+import Mathlib.Algebra.Lie.OfAssociative
+import Mathlib.GroupTheory.MonoidLocalization.Basic
+import Mathlib.LinearAlgebra.TensorAlgebra.Basic
+import Mathlib.RingTheory.HopfAlgebra.Basic
+import Mathlib.Algebra.Algebra.Bilinear
+
+namespace TensorAlgebra
+open scoped TensorProduct
+
+variable (R : Type*) [CommRing R] {M : Type*} [AddCommMonoid M] [Module R M]
+
+local notation "T["M"]" => TensorAlgebra R M
+
+/-- Counit in `TensorAlgebra R M`. -/
+abbrev ε := @algebraMapInv R _ M _ _
+
+/-- Linear map inducing the comultiplication in `TensorAlgebra R M`. -/
+def comul' : M →ₗ[R] T[M] ⊗[R] T[M] :=
+  TensorProduct.map (ι R) (Algebra.linearMap R T[M]) ∘ₗ (TensorProduct.rid R M).symm +
+  TensorProduct.map (Algebra.linearMap R T[M]) (ι R) ∘ₗ (TensorProduct.lid R M).symm
+
+/-- Comultiplication in `TensorAlgebra R M` as an algebra map. -/
+def comul : T[M] →ₐ[R] T[M] ⊗[R] T[M] := lift R (comul' R)
+
+/-- Antipode in `TensorAlgebra R M` as an algebra map. -/
+def antipode : T[M] →ₗ[R] T[M] := (MulOpposite.opLinearEquiv R).symm.comp
+  (lift R ((MulOpposite.opLinearEquiv R).comp (-(ι R)))).toLinearMap
+
+@[simp]
+lemma comul_apply' (x : M) : comul' R x = ι R x ⊗ₜ[R] ↑1 + ↑1 ⊗ₜ[R] ι R x := by
+  unfold comul'
+  simp
+
+@[simp]
+lemma counit_ι_apply (x : M) : (ε R) ((ι R) x) = 0 := by
+  unfold ε 
+  rw [algebraMapInv]
+  simp
+
+@[simp]
+lemma counit_ι_eq_zero : (ε R).toLinearMap ∘ₗ (ι R) = (0 : M →ₗ[R] R) := by
+  ext x
+  simp
+
+theorem rTensor : (Algebra.TensorProduct.map (ε R) (AlgHom.id R T[M])).comp (comul R) =
+    (Algebra.TensorProduct.lid R T[M]).symm.toAlgHom := by
+  unfold ε comul comul'
+  ext x
+  rw [algebraMapInv]
+  simp
+
+theorem lTensor : (Algebra.TensorProduct.map (AlgHom.id R T[M]) (ε R)).comp (comul R) =
+    ↑(Algebra.TensorProduct.rid R R T[M]).symm := by
+  unfold ε comul comul'
+  ext x
+  rw [algebraMapInv]
+  simp
+
+@[simp]
+lemma antipode_ι_apply (x : M) : antipode R ((ι R) x) = -(ι R) x := by
+  unfold antipode
+  simp
+
+@[simp]
+lemma antipode_one (r : R) : antipode R (algebraMap R T[M] r) = algebraMap R T[M] r := by
+  unfold antipode
+  simp
+
+theorem coassoc : (Algebra.TensorProduct.assoc R R T[M] T[M] T[M]).toAlgHom.comp 
+    ((Algebra.TensorProduct.map (comul R) (AlgHom.id R T[M])).comp (comul R)) =
+    (Algebra.TensorProduct.map (AlgHom.id R T[M]) (comul R)).comp (comul R) := by
+  unfold comul comul'
+  ext
+  /- can be reduced maybe? -/
+  simp only [AlgHom.comp_toLinearMap, LinearMap.coe_comp, AlgHom.coe_toLinearMap,
+  Function.comp_apply, lift_ι_apply, LinearMap.add_apply, LinearEquiv.coe_coe,
+  TensorProduct.rid_symm_apply, TensorProduct.map_tmul, Algebra.linearMap_apply, map_one,
+  TensorProduct.lid_symm_apply, map_add, Algebra.TensorProduct.map_tmul, TensorProduct.tmul_add]
+  abel
+
+instance instBialgebra : Bialgebra R T[M] :=
+  Bialgebra.ofAlgHom (comul R) (ε R) (coassoc R) (rTensor R) (lTensor R)
+
+instance : HopfAlgebraStruct R T[M] where
+  antipode := antipode R
+
+@[simp]
+theorem antipode_antihom_apply (x y : T[M]) : antipode R (x * y) = antipode R y * antipode R x := by
+  unfold antipode
+  simp
+
+@[simp]
+theorem antipode_antihom : antipode R ∘ₗ LinearMap.mul' R T[M] =
+    LinearMap.mul' R T[M] ∘ₗ TensorProduct.comm R T[M] T[M] ∘ₗ TensorProduct.map (antipode R)
+    (antipode R) := by
+  ext x y
+  simp
+
+end TensorAlgebra

From a1a3d1d1d8d2ddf2d816721246c84c25a9332dbd Mon Sep 17 00:00:00 2001
From: Nikolas Tapia <tapia@wias-berlin.de>
Date: Tue, 11 Nov 2025 13:06:32 -0300
Subject: [PATCH 02/23] add new file header

---
 Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
index c2792bc7e2c36a..e52d7b7aab2a59 100644
--- a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
+++ b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
@@ -1,9 +1,24 @@
+/-
+Copyright (c) 2025 Nikolas Tapia. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nikolas Tapia
+-/
 import Mathlib.Algebra.Lie.OfAssociative
 import Mathlib.GroupTheory.MonoidLocalization.Basic
 import Mathlib.LinearAlgebra.TensorAlgebra.Basic
 import Mathlib.RingTheory.HopfAlgebra.Basic
 import Mathlib.Algebra.Algebra.Bilinear
 
+/-!
+# Hopf algebra structure on `TensorAlgebra R M`
+
+In this file we implement the natura Hopf algebra structure on `TensorAlgebra R M`.
+The comultiplication is the unique algebra map satisfying `comul ((ι R) x) = (ι R) x ⊗ 1 + 1 ⊗ (ι R)
+x` for all `x : M`.
+`algebraMapInv` acts as the counit, and the antipode is the unique algebra map `antipode :
+TensorAlgebra R M → (TensorAlgebra R M)ᵐᵒᵖ` induced by `fun x => op -(ι R) x`.
+-/
+
 namespace TensorAlgebra
 open scoped TensorProduct
 
@@ -25,6 +40,7 @@ def comul : T[M] →ₐ[R] T[M] ⊗[R] T[M] := lift R (comul' R)
 /-- Antipode in `TensorAlgebra R M` as an algebra map. -/
 def antipode : T[M] →ₗ[R] T[M] := (MulOpposite.opLinearEquiv R).symm.comp
   (lift R ((MulOpposite.opLinearEquiv R).comp (-(ι R)))).toLinearMap
+def antipode : T[M] →ₗ[R] T[M] := (MulOpposite.opLinearEquiv R).symm.comp (lift R ((MulOpposite.opLinearEquiv R).comp (-(ι R)))).toLinearMap
 
 @[simp]
 lemma comul_apply' (x : M) : comul' R x = ι R x ⊗ₜ[R] ↑1 + ↑1 ⊗ₜ[R] ι R x := by

From aad3c860b2a53879c35d713abd601ddd8e4baf2d Mon Sep 17 00:00:00 2001
From: Nikolas Tapia <tapia@wias-berlin.de>
Date: Tue, 11 Nov 2025 13:01:25 -0300
Subject: [PATCH 03/23] update files

---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index d216b7d5af7b9f..374feca342f08a 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -4559,6 +4559,7 @@ import Mathlib.LinearAlgebra.SymplecticGroup
 import Mathlib.LinearAlgebra.TensorAlgebra.Basic
 import Mathlib.LinearAlgebra.TensorAlgebra.Basis
 import Mathlib.LinearAlgebra.TensorAlgebra.Grading
+import Mathlib.LinearAlgebra.TensorAlgebra.Hopf
 import Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
 import Mathlib.LinearAlgebra.TensorPower.Basic
 import Mathlib.LinearAlgebra.TensorPower.Pairing

From 7099dbe2a3ffa1b972a693732ba12eaf6939a5af Mon Sep 17 00:00:00 2001
From: Nikolas Tapia <tapia@wias-berlin.de>
Date: Wed, 12 Nov 2025 18:32:09 -0300
Subject: [PATCH 04/23] remove trailing whitespace

---
 Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
index e52d7b7aab2a59..53d200f84bdb0c 100644
--- a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
+++ b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
@@ -49,7 +49,7 @@ lemma comul_apply' (x : M) : comul' R x = ι R x ⊗ₜ[R] ↑1 + ↑1 ⊗ₜ[R]
 
 @[simp]
 lemma counit_ι_apply (x : M) : (ε R) ((ι R) x) = 0 := by
-  unfold ε 
+  unfold ε
   rw [algebraMapInv]
   simp
 
@@ -82,7 +82,7 @@ lemma antipode_one (r : R) : antipode R (algebraMap R T[M] r) = algebraMap R T[M
   unfold antipode
   simp
 
-theorem coassoc : (Algebra.TensorProduct.assoc R R T[M] T[M] T[M]).toAlgHom.comp 
+theorem coassoc : (Algebra.TensorProduct.assoc R R T[M] T[M] T[M]).toAlgHom.comp
     ((Algebra.TensorProduct.map (comul R) (AlgHom.id R T[M])).comp (comul R)) =
     (Algebra.TensorProduct.map (AlgHom.id R T[M]) (comul R)).comp (comul R) := by
   unfold comul comul'

From b55afbcdf5acf95dbfbb7d1b27c3d11ca3c2013e Mon Sep 17 00:00:00 2001
From: Nikolas Tapia <tapia@wias-berlin.de>
Date: Wed, 12 Nov 2025 18:44:36 -0300
Subject: [PATCH 05/23] delete duplicate def

---
 Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
index 53d200f84bdb0c..4915cf2e31d77e 100644
--- a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
+++ b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
@@ -40,7 +40,6 @@ def comul : T[M] →ₐ[R] T[M] ⊗[R] T[M] := lift R (comul' R)
 /-- Antipode in `TensorAlgebra R M` as an algebra map. -/
 def antipode : T[M] →ₗ[R] T[M] := (MulOpposite.opLinearEquiv R).symm.comp
   (lift R ((MulOpposite.opLinearEquiv R).comp (-(ι R)))).toLinearMap
-def antipode : T[M] →ₗ[R] T[M] := (MulOpposite.opLinearEquiv R).symm.comp (lift R ((MulOpposite.opLinearEquiv R).comp (-(ι R)))).toLinearMap
 
 @[simp]
 lemma comul_apply' (x : M) : comul' R x = ι R x ⊗ₜ[R] ↑1 + ↑1 ⊗ₜ[R] ι R x := by

From 78371493c6cc9b2c72c4e5390729044aff5ac72f Mon Sep 17 00:00:00 2001
From: Nikolas Tapia <tapia@wias-berlin.de>
Date: Fri, 21 Nov 2025 15:07:10 +0100
Subject: [PATCH 06/23] =?UTF-8?q?change=20=CE=B5=20to=20algebraMapInv?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
index 4915cf2e31d77e..d0e93d1f288706 100644
--- a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
+++ b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
@@ -21,6 +21,8 @@ TensorAlgebra R M → (TensorAlgebra R M)ᵐᵒᵖ` induced by `fun x => op -(ι
 
 namespace TensorAlgebra
 open scoped TensorProduct
+open scoped TensorProduct RingTheory.LinearMap Coalgebra
+open LinearMap TensorProduct
 
 variable (R : Type*) [CommRing R] {M : Type*} [AddCommMonoid M] [Module R M]
 
@@ -49,24 +51,30 @@ lemma comul_apply' (x : M) : comul' R x = ι R x ⊗ₜ[R] ↑1 + ↑1 ⊗ₜ[R]
 @[simp]
 lemma counit_ι_apply (x : M) : (ε R) ((ι R) x) = 0 := by
   unfold ε
+lemma counit_ι_apply (x : M) : algebraMapInv ((ι R) x) = 0 := by
   rw [algebraMapInv]
   simp
 
 @[simp]
 lemma counit_ι_eq_zero : (ε R).toLinearMap ∘ₗ (ι R) = (0 : M →ₗ[R] R) := by
+lemma counit_ι_eq_zero : algebraMapInv.toLinearMap ∘ₗ (ι R) = (0 : M →ₗ[R] R) := by
   ext x
   simp
 
 theorem rTensor : (Algebra.TensorProduct.map (ε R) (AlgHom.id R T[M])).comp (comul R) =
+theorem rTensor : (Algebra.TensorProduct.map algebraMapInv (AlgHom.id R T[M])).comp (comul R) =
     (Algebra.TensorProduct.lid R T[M]).symm.toAlgHom := by
   unfold ε comul comul'
+  unfold comul comul'
   ext x
   rw [algebraMapInv]
   simp
 
 theorem lTensor : (Algebra.TensorProduct.map (AlgHom.id R T[M]) (ε R)).comp (comul R) =
+theorem lTensor : (Algebra.TensorProduct.map (AlgHom.id R T[M]) algebraMapInv).comp (comul R) =
     ↑(Algebra.TensorProduct.rid R R T[M]).symm := by
   unfold ε comul comul'
+  unfold comul comul'
   ext x
   rw [algebraMapInv]
   simp
@@ -93,11 +101,8 @@ theorem coassoc : (Algebra.TensorProduct.assoc R R T[M] T[M] T[M]).toAlgHom.comp
   TensorProduct.lid_symm_apply, map_add, Algebra.TensorProduct.map_tmul, TensorProduct.tmul_add]
   abel
 
-instance instBialgebra : Bialgebra R T[M] :=
-  Bialgebra.ofAlgHom (comul R) (ε R) (coassoc R) (rTensor R) (lTensor R)
-
-instance : HopfAlgebraStruct R T[M] where
-  antipode := antipode R
+instance instBialgebra : Bialgebra R T[M] := Bialgebra.ofAlgHom (comul R) algebraMapInv
+    (coassoc R) (rTensor R) (lTensor R)
 
 @[simp]
 theorem antipode_antihom_apply (x y : T[M]) : antipode R (x * y) = antipode R y * antipode R x := by

From b0791342b09c348309c8691d8fe3b00322fd9909 Mon Sep 17 00:00:00 2001
From: Nikolas Tapia <tapia@wias-berlin.de>
Date: Fri, 21 Nov 2025 15:08:53 +0100
Subject: [PATCH 07/23] use tensor notation for TensorProduct.map

---
 Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
index d0e93d1f288706..6cb263d6754b14 100644
--- a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
+++ b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
@@ -35,6 +35,8 @@ abbrev ε := @algebraMapInv R _ M _ _
 def comul' : M →ₗ[R] T[M] ⊗[R] T[M] :=
   TensorProduct.map (ι R) (Algebra.linearMap R T[M]) ∘ₗ (TensorProduct.rid R M).symm +
   TensorProduct.map (Algebra.linearMap R T[M]) (ι R) ∘ₗ (TensorProduct.lid R M).symm
+  ((ι R) ⊗ₘ (Algebra.linearMap R T[M])) ∘ₗ (TensorProduct.rid R M).symm +
+  ((Algebra.linearMap R T[M]) ⊗ₘ (ι R)) ∘ₗ (TensorProduct.lid R M).symm
 
 /-- Comultiplication in `TensorAlgebra R M` as an algebra map. -/
 def comul : T[M] →ₐ[R] T[M] ⊗[R] T[M] := lift R (comul' R)
@@ -110,9 +112,8 @@ theorem antipode_antihom_apply (x y : T[M]) : antipode R (x * y) = antipode R y
   simp
 
 @[simp]
-theorem antipode_antihom : antipode R ∘ₗ LinearMap.mul' R T[M] =
-    LinearMap.mul' R T[M] ∘ₗ TensorProduct.comm R T[M] T[M] ∘ₗ TensorProduct.map (antipode R)
-    (antipode R) := by
+theorem antipode_antihom : antipode R ∘ₗ mul' R T[M] =
+    mul' R T[M] ∘ₗ TensorProduct.comm R T[M] T[M] ∘ₗ ((antipode R) ⊗ₘ (antipode R)) := by
   ext x y
   simp
 

From 7f2fb474be2f52579e2881f1e896e4ea19973d51 Mon Sep 17 00:00:00 2001
From: Nikolas Tapia <tapia@wias-berlin.de>
Date: Fri, 21 Nov 2025 15:12:41 +0100
Subject: [PATCH 08/23] slightly change two lemmas

---
 Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
index 6cb263d6754b14..4fe1ae350e9591 100644
--- a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
+++ b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
@@ -46,8 +46,8 @@ def antipode : T[M] →ₗ[R] T[M] := (MulOpposite.opLinearEquiv R).symm.comp
   (lift R ((MulOpposite.opLinearEquiv R).comp (-(ι R)))).toLinearMap
 
 @[simp]
-lemma comul_apply' (x : M) : comul' R x = ι R x ⊗ₜ[R] ↑1 + ↑1 ⊗ₜ[R] ι R x := by
-  unfold comul'
+lemma comul_apply (x : M) : comul R (ι R x) = ι R x ⊗ₜ[R] ↑1 + ↑1 ⊗ₜ[R] ι R x := by
+  unfold comul comul'
   simp
 
 @[simp]
@@ -87,7 +87,8 @@ lemma antipode_ι_apply (x : M) : antipode R ((ι R) x) = -(ι R) x := by
   simp
 
 @[simp]
-lemma antipode_one (r : R) : antipode R (algebraMap R T[M] r) = algebraMap R T[M] r := by
+lemma antipode_algebraMap_apply (r : R) :
+    antipode R ((algebraMap R T[M]) r) = algebraMap R T[M] r := by
   unfold antipode
   simp
 
@@ -97,10 +98,10 @@ theorem coassoc : (Algebra.TensorProduct.assoc R R T[M] T[M] T[M]).toAlgHom.comp
   unfold comul comul'
   ext
   /- can be reduced maybe? -/
-  simp only [AlgHom.comp_toLinearMap, LinearMap.coe_comp, AlgHom.coe_toLinearMap,
-  Function.comp_apply, lift_ι_apply, LinearMap.add_apply, LinearEquiv.coe_coe,
-  TensorProduct.rid_symm_apply, TensorProduct.map_tmul, Algebra.linearMap_apply, map_one,
-  TensorProduct.lid_symm_apply, map_add, Algebra.TensorProduct.map_tmul, TensorProduct.tmul_add]
+  simp only [AlgHom.comp_toLinearMap, coe_comp, AlgHom.coe_toLinearMap,
+  Function.comp_apply, lift_ι_apply, add_apply, LinearEquiv.coe_coe,
+  rid_symm_apply, map_tmul, Algebra.linearMap_apply, map_one,
+  lid_symm_apply, map_add, Algebra.TensorProduct.map_tmul, tmul_add]
   abel
 
 instance instBialgebra : Bialgebra R T[M] := Bialgebra.ofAlgHom (comul R) algebraMapInv

From b34585f0362959840fe708171a0d920404a2491b Mon Sep 17 00:00:00 2001
From: Nikolas Tapia <tapia@wias-berlin.de>
Date: Sun, 16 Nov 2025 23:03:20 +0100
Subject: [PATCH 09/23] implement HopfAlgebra for TensorAlgebra

---
 Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean | 118 +++++++++++++++---
 1 file changed, 102 insertions(+), 16 deletions(-)

diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
index 4fe1ae350e9591..5bbb6c01787e10 100644
--- a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
+++ b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
@@ -3,11 +3,9 @@ Copyright (c) 2025 Nikolas Tapia. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nikolas Tapia
 -/
-import Mathlib.Algebra.Lie.OfAssociative
-import Mathlib.GroupTheory.MonoidLocalization.Basic
 import Mathlib.LinearAlgebra.TensorAlgebra.Basic
+import Mathlib.RingTheory.Coalgebra.Convolution
 import Mathlib.RingTheory.HopfAlgebra.Basic
-import Mathlib.Algebra.Algebra.Bilinear
 
 /-!
 # Hopf algebra structure on `TensorAlgebra R M`
@@ -20,7 +18,6 @@ TensorAlgebra R M → (TensorAlgebra R M)ᵐᵒᵖ` induced by `fun x => op -(ι
 -/
 
 namespace TensorAlgebra
-open scoped TensorProduct
 open scoped TensorProduct RingTheory.LinearMap Coalgebra
 open LinearMap TensorProduct
 
@@ -28,13 +25,8 @@ variable (R : Type*) [CommRing R] {M : Type*} [AddCommMonoid M] [Module R M]
 
 local notation "T["M"]" => TensorAlgebra R M
 
-/-- Counit in `TensorAlgebra R M`. -/
-abbrev ε := @algebraMapInv R _ M _ _
-
 /-- Linear map inducing the comultiplication in `TensorAlgebra R M`. -/
 def comul' : M →ₗ[R] T[M] ⊗[R] T[M] :=
-  TensorProduct.map (ι R) (Algebra.linearMap R T[M]) ∘ₗ (TensorProduct.rid R M).symm +
-  TensorProduct.map (Algebra.linearMap R T[M]) (ι R) ∘ₗ (TensorProduct.lid R M).symm
   ((ι R) ⊗ₘ (Algebra.linearMap R T[M])) ∘ₗ (TensorProduct.rid R M).symm +
   ((Algebra.linearMap R T[M]) ⊗ₘ (ι R)) ∘ₗ (TensorProduct.lid R M).symm
 
@@ -51,31 +43,24 @@ lemma comul_apply (x : M) : comul R (ι R x) = ι R x ⊗ₜ[R] ↑1 + ↑1 ⊗
   simp
 
 @[simp]
-lemma counit_ι_apply (x : M) : (ε R) ((ι R) x) = 0 := by
-  unfold ε
 lemma counit_ι_apply (x : M) : algebraMapInv ((ι R) x) = 0 := by
   rw [algebraMapInv]
   simp
 
 @[simp]
-lemma counit_ι_eq_zero : (ε R).toLinearMap ∘ₗ (ι R) = (0 : M →ₗ[R] R) := by
 lemma counit_ι_eq_zero : algebraMapInv.toLinearMap ∘ₗ (ι R) = (0 : M →ₗ[R] R) := by
   ext x
   simp
 
-theorem rTensor : (Algebra.TensorProduct.map (ε R) (AlgHom.id R T[M])).comp (comul R) =
 theorem rTensor : (Algebra.TensorProduct.map algebraMapInv (AlgHom.id R T[M])).comp (comul R) =
     (Algebra.TensorProduct.lid R T[M]).symm.toAlgHom := by
-  unfold ε comul comul'
   unfold comul comul'
   ext x
   rw [algebraMapInv]
   simp
 
-theorem lTensor : (Algebra.TensorProduct.map (AlgHom.id R T[M]) (ε R)).comp (comul R) =
 theorem lTensor : (Algebra.TensorProduct.map (AlgHom.id R T[M]) algebraMapInv).comp (comul R) =
     ↑(Algebra.TensorProduct.rid R R T[M]).symm := by
-  unfold ε comul comul'
   unfold comul comul'
   ext x
   rw [algebraMapInv]
@@ -118,4 +103,105 @@ theorem antipode_antihom : antipode R ∘ₗ mul' R T[M] =
   ext x y
   simp
 
+open Algebra Bialgebra Coalgebra in
+instance instHopfAlgebra : HopfAlgebra R T[M] where
+  antipode := antipode R
+  mul_antipode_rTensor_comul := by
+    rw [LinearMap.rTensor, ← LinearMap.convMul_def, ← convOne_def]
+    ext x
+    induction x using induction with
+    | algebraMap r => simp
+    | add u v hu hv => rw [map_add, hu, hv, ← map_add]
+    | ι u =>
+        conv =>
+          rhs
+          rw [convOne_def, comp_apply, CoalgebraStruct.counit, instBialgebra, toCoalgebraStruct,
+            toCoalgebra, ofAlgHom, mk', coe_coe, counit_ι_apply, map_zero]
+        conv =>
+          lhs
+          rw [convMul_apply, CoalgebraStruct.comul, toCoalgebraStruct, toCoalgebra]
+          unfold instBialgebra ofAlgHom mk'
+          simp only [coe_coe, comul_apply, map_add, map_tmul, antipode_ι_apply, id_coe, id_eq,
+            mul'_apply, mul_one, ← map_one (algebraMap R T[M]), antipode_algebraMap_apply]
+          simp only [map_one, mul_one, one_mul, neg_add_cancel]
+    | mul u v hu hv => 
+        conv =>
+          rhs
+          rw [convOne_apply, counit_mul, map_mul, ← convOne_apply, ← convOne_apply]
+        have assoc4 {Q} [Semiring Q] (a b c d : Q) : a * b * (c * d) = a * (b * c) * d := by
+          rw [← mul_assoc, mul_assoc a b c]
+        rw [convMul_apply, comul_mul, ← Coalgebra.Repr.eq (ℛ R u), ← Coalgebra.Repr.eq (ℛ R v),
+          Finset.sum_mul_sum, map_sum, map_sum] at *
+        simp only [TensorProduct.tmul_mul_tmul, map_sum, map_tmul, antipode_antihom_apply, id_coe,
+        id_eq, mul'_apply] at *
+        conv =>
+          lhs
+          conv =>
+            arg 2
+            intro i
+            conv =>
+              arg 2
+              intro j
+              rw [assoc4]
+        rw [Finset.sum_comm]
+        conv =>
+          lhs
+          conv =>
+            arg 2
+            intro i
+            rw [← Finset.sum_mul, ← Finset.mul_sum, hu, convOne_apply,
+            ← Algebra.commutes, mul_assoc]
+          rw [← Finset.mul_sum, hv, ← convOne_apply]
+  mul_antipode_lTensor_comul := by
+    rw [LinearMap.lTensor, ← LinearMap.convMul_def, ← convOne_def]
+    ext x
+    induction x using induction with
+    | algebraMap r => 
+        simp only [convMul_apply, comul_algebraMap, TensorProduct.algebraMap_apply, map_tmul,
+          id_coe, id_eq, mul'_apply, convOne_apply, counit_algebraMap, ← map_one (algebraMap R
+          T[M]), antipode_algebraMap_apply]
+        simp
+    | add u v hu hv => rw [map_add, hu, hv, ← map_add]
+    | ι u =>
+        conv =>
+          rhs
+          rw [convOne_def, comp_apply, CoalgebraStruct.counit, instBialgebra, toCoalgebraStruct,
+            toCoalgebra, ofAlgHom, mk', coe_coe, counit_ι_apply, map_zero]
+        conv =>
+          lhs
+          rw [convMul_apply, CoalgebraStruct.comul, toCoalgebraStruct, toCoalgebra]
+          unfold instBialgebra ofAlgHom mk'
+          simp only [coe_coe, comul_apply, map_add, map_tmul, antipode_ι_apply, id_coe, id_eq,
+            mul'_apply, mul_one, ← map_one (algebraMap R T[M]), antipode_algebraMap_apply]
+          simp only [map_one, mul_one, one_mul, neg_add_cancel]
+          abel_nf
+    | mul u v hu hv => 
+        conv =>
+          rhs
+          rw [convOne_apply, counit_mul, map_mul, Algebra.commutes, ← convOne_apply,
+            ← convOne_apply]
+        have assoc4 {Q} [Semiring Q] (a b c d : Q) : a * b * (c * d) = a * (b * c) * d := by
+          rw [← mul_assoc, mul_assoc a b c]
+        rw [convMul_apply, comul_mul, ← Coalgebra.Repr.eq (ℛ R u), ← Coalgebra.Repr.eq (ℛ R v),
+          Finset.sum_mul_sum, map_sum, map_sum] at *
+        simp only [TensorProduct.tmul_mul_tmul, map_sum, map_tmul, antipode_antihom_apply, id_coe,
+        id_eq, mul'_apply] at *
+        conv =>
+          lhs
+          conv =>
+            arg 2
+            intro i
+            conv =>
+              arg 2
+              intro j
+              rw [assoc4]
+        conv =>
+          lhs
+          conv =>
+            arg 2
+            intro i
+            rw [← Finset.sum_mul, ← Finset.mul_sum, hv, convOne_apply,
+            ← Algebra.commutes, mul_assoc]
+          rw [← Finset.mul_sum, hu, ← convOne_apply]
+
 end TensorAlgebra

From a16a19bc31ae6b5834ab5cfac310890625ac430a Mon Sep 17 00:00:00 2001
From: Nikolas Tapia <tapia@wias-berlin.de>
Date: Fri, 21 Nov 2025 15:23:02 +0100
Subject: [PATCH 10/23] remove trailing whitspace

---
 Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
index 5bbb6c01787e10..fddffa768415ee 100644
--- a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
+++ b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
@@ -124,7 +124,7 @@ instance instHopfAlgebra : HopfAlgebra R T[M] where
           simp only [coe_coe, comul_apply, map_add, map_tmul, antipode_ι_apply, id_coe, id_eq,
             mul'_apply, mul_one, ← map_one (algebraMap R T[M]), antipode_algebraMap_apply]
           simp only [map_one, mul_one, one_mul, neg_add_cancel]
-    | mul u v hu hv => 
+    | mul u v hu hv =>
         conv =>
           rhs
           rw [convOne_apply, counit_mul, map_mul, ← convOne_apply, ← convOne_apply]
@@ -156,7 +156,7 @@ instance instHopfAlgebra : HopfAlgebra R T[M] where
     rw [LinearMap.lTensor, ← LinearMap.convMul_def, ← convOne_def]
     ext x
     induction x using induction with
-    | algebraMap r => 
+    | algebraMap r =>
         simp only [convMul_apply, comul_algebraMap, TensorProduct.algebraMap_apply, map_tmul,
           id_coe, id_eq, mul'_apply, convOne_apply, counit_algebraMap, ← map_one (algebraMap R
           T[M]), antipode_algebraMap_apply]
@@ -175,7 +175,7 @@ instance instHopfAlgebra : HopfAlgebra R T[M] where
             mul'_apply, mul_one, ← map_one (algebraMap R T[M]), antipode_algebraMap_apply]
           simp only [map_one, mul_one, one_mul, neg_add_cancel]
           abel_nf
-    | mul u v hu hv => 
+    | mul u v hu hv =>
         conv =>
           rhs
           rw [convOne_apply, counit_mul, map_mul, Algebra.commutes, ← convOne_apply,

From 4cd2f5f6a883054e7fbbf0f903602f09797dfc63 Mon Sep 17 00:00:00 2001
From: Nikolas Tapia <tapia@wias-berlin.de>
Date: Fri, 21 Nov 2025 20:24:56 +0100
Subject: [PATCH 11/23] use module

---
 Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
index fddffa768415ee..c0ada4b5b69b4f 100644
--- a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
+++ b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
@@ -3,9 +3,11 @@ Copyright (c) 2025 Nikolas Tapia. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nikolas Tapia
 -/
-import Mathlib.LinearAlgebra.TensorAlgebra.Basic
-import Mathlib.RingTheory.Coalgebra.Convolution
-import Mathlib.RingTheory.HopfAlgebra.Basic
+module 
+
+public import Mathlib.LinearAlgebra.TensorAlgebra.Basic
+public import Mathlib.RingTheory.Coalgebra.Convolution
+public import Mathlib.RingTheory.HopfAlgebra.Basic
 
 /-!
 # Hopf algebra structure on `TensorAlgebra R M`
@@ -16,6 +18,7 @@ x` for all `x : M`.
 `algebraMapInv` acts as the counit, and the antipode is the unique algebra map `antipode :
 TensorAlgebra R M → (TensorAlgebra R M)ᵐᵒᵖ` induced by `fun x => op -(ι R) x`.
 -/
+@[expose] public section
 
 namespace TensorAlgebra
 open scoped TensorProduct RingTheory.LinearMap Coalgebra

From b10e530f6d66f8a9ec7e709a839658c15c84c028 Mon Sep 17 00:00:00 2001
From: "pre-commit-ci-lite[bot]"
 <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
Date: Fri, 21 Nov 2025 19:37:26 +0000
Subject: [PATCH 12/23] [pre-commit.ci lite] apply automatic fixes

---
 Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
index c0ada4b5b69b4f..7ec10cdde075a0 100644
--- a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
+++ b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
@@ -3,7 +3,7 @@ Copyright (c) 2025 Nikolas Tapia. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nikolas Tapia
 -/
-module 
+module
 
 public import Mathlib.LinearAlgebra.TensorAlgebra.Basic
 public import Mathlib.RingTheory.Coalgebra.Convolution
@@ -26,7 +26,7 @@ open LinearMap TensorProduct
 
 variable (R : Type*) [CommRing R] {M : Type*} [AddCommMonoid M] [Module R M]
 
-local notation "T["M"]" => TensorAlgebra R M
+local notation "T[" M "]" => TensorAlgebra R M
 
 /-- Linear map inducing the comultiplication in `TensorAlgebra R M`. -/
 def comul' : M →ₗ[R] T[M] ⊗[R] T[M] :=

From 24b59d6155f1fffda24cde7ad358d35bd6a29a09 Mon Sep 17 00:00:00 2001
From: Nikolas Tapia <tapia@wias-berlin.de>
Date: Sat, 22 Nov 2025 10:45:07 +0100
Subject: [PATCH 13/23] apply style fixes

---
 Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean | 98 ++++++++-----------
 1 file changed, 41 insertions(+), 57 deletions(-)

diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
index 7ec10cdde075a0..2aa8ed6b613327 100644
--- a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
+++ b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
@@ -24,88 +24,70 @@ namespace TensorAlgebra
 open scoped TensorProduct RingTheory.LinearMap Coalgebra
 open LinearMap TensorProduct
 
-variable (R : Type*) [CommRing R] {M : Type*} [AddCommMonoid M] [Module R M]
+section Bialgebra
+
+variable (R : Type*) [CommSemiring R] {M : Type*} [AddCommMonoid M] [Module R M]
 
 local notation "T[" M "]" => TensorAlgebra R M
 
-/-- Linear map inducing the comultiplication in `TensorAlgebra R M`. -/
-def comul' : M →ₗ[R] T[M] ⊗[R] T[M] :=
+/-- Comultiplication in `TensorAlgebra R M` as an algebra map.
+It is induced by the linear map sending `(m : M)` to `ι R m ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ι R m`.
+See `comul_apply`.
+-/
+def comul : T[M] →ₐ[R] T[M] ⊗[R] T[M] := lift R (
   ((ι R) ⊗ₘ (Algebra.linearMap R T[M])) ∘ₗ (TensorProduct.rid R M).symm +
   ((Algebra.linearMap R T[M]) ⊗ₘ (ι R)) ∘ₗ (TensorProduct.lid R M).symm
-
-/-- Comultiplication in `TensorAlgebra R M` as an algebra map. -/
-def comul : T[M] →ₐ[R] T[M] ⊗[R] T[M] := lift R (comul' R)
-
-/-- Antipode in `TensorAlgebra R M` as an algebra map. -/
-def antipode : T[M] →ₗ[R] T[M] := (MulOpposite.opLinearEquiv R).symm.comp
-  (lift R ((MulOpposite.opLinearEquiv R).comp (-(ι R)))).toLinearMap
+  )
 
 @[simp]
-lemma comul_apply (x : M) : comul R (ι R x) = ι R x ⊗ₜ[R] ↑1 + ↑1 ⊗ₜ[R] ι R x := by
-  unfold comul comul'
-  simp
+lemma comul_apply (m : M) : comul R (ι R m) = ι R m ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ι R m := by
+  simp [comul]
 
 @[simp]
-lemma counit_ι_apply (x : M) : algebraMapInv ((ι R) x) = 0 := by
-  rw [algebraMapInv]
-  simp
+lemma algebraMapInv_ι_apply (m : M) : algebraMapInv (ι R m) = 0 := by
+  simp [algebraMapInv]
 
 @[simp]
-lemma counit_ι_eq_zero : algebraMapInv.toLinearMap ∘ₗ (ι R) = (0 : M →ₗ[R] R) := by
-  ext x
+lemma algebraMapInv_ι_eq_zero : algebraMapInv.toLinearMap ∘ₗ (ι R) = (0 : M →ₗ[R] R) := by
+  ext
   simp
 
-theorem rTensor : (Algebra.TensorProduct.map algebraMapInv (AlgHom.id R T[M])).comp (comul R) =
-    (Algebra.TensorProduct.lid R T[M]).symm.toAlgHom := by
-  unfold comul comul'
-  ext x
-  rw [algebraMapInv]
-  simp
+instance instBialgebra : Bialgebra R T[M] := Bialgebra.ofAlgHom (comul R) algebraMapInv
+    (by ext; simpa [comul, Algebra.TensorProduct.one_def, add_tmul, tmul_add] using by abel)
+    (by ext; simp [comul, algebraMapInv])
+    (by ext; simp [comul, algebraMapInv])
 
-theorem lTensor : (Algebra.TensorProduct.map (AlgHom.id R T[M]) algebraMapInv).comp (comul R) =
-    ↑(Algebra.TensorProduct.rid R R T[M]).symm := by
-  unfold comul comul'
-  ext x
-  rw [algebraMapInv]
-  simp
+end Bialgebra
 
-@[simp]
-lemma antipode_ι_apply (x : M) : antipode R ((ι R) x) = -(ι R) x := by
-  unfold antipode
-  simp
+section HopfAlgebra
 
-@[simp]
-lemma antipode_algebraMap_apply (r : R) :
-    antipode R ((algebraMap R T[M]) r) = algebraMap R T[M] r := by
-  unfold antipode
-  simp
+variable (R : Type*) [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
 
-theorem coassoc : (Algebra.TensorProduct.assoc R R T[M] T[M] T[M]).toAlgHom.comp
-    ((Algebra.TensorProduct.map (comul R) (AlgHom.id R T[M])).comp (comul R)) =
-    (Algebra.TensorProduct.map (AlgHom.id R T[M]) (comul R)).comp (comul R) := by
-  unfold comul comul'
-  ext
-  /- can be reduced maybe? -/
-  simp only [AlgHom.comp_toLinearMap, coe_comp, AlgHom.coe_toLinearMap,
-  Function.comp_apply, lift_ι_apply, add_apply, LinearEquiv.coe_coe,
-  rid_symm_apply, map_tmul, Algebra.linearMap_apply, map_one,
-  lid_symm_apply, map_add, Algebra.TensorProduct.map_tmul, tmul_add]
-  abel
+local notation "T[" M "]" => TensorAlgebra R M
 
-instance instBialgebra : Bialgebra R T[M] := Bialgebra.ofAlgHom (comul R) algebraMapInv
-    (coassoc R) (rTensor R) (lTensor R)
+/-- Antipode in `TensorAlgebra R M` as an algebra map. -/
+def antipode : T[M] →ₗ[R] T[M] := (MulOpposite.opLinearEquiv R).symm.comp
+  (lift R ((MulOpposite.opLinearEquiv R).comp (-(ι R)))).toLinearMap
+
+@[simp]
+lemma antipode_ι_apply (x : M) : antipode R ((ι R) x) = -(ι R) x := by
+  simp [antipode]
 
 @[simp]
 theorem antipode_antihom_apply (x y : T[M]) : antipode R (x * y) = antipode R y * antipode R x := by
-  unfold antipode
-  simp
+  simp [antipode]
 
 @[simp]
 theorem antipode_antihom : antipode R ∘ₗ mul' R T[M] =
     mul' R T[M] ∘ₗ TensorProduct.comm R T[M] T[M] ∘ₗ ((antipode R) ⊗ₘ (antipode R)) := by
-  ext x y
+  ext
   simp
 
+@[simp]
+lemma antipode_algebraMap_apply (r : R) :
+    antipode R ((algebraMap R T[M]) r) = algebraMap R T[M] r := by
+  simp [antipode]
+
 open Algebra Bialgebra Coalgebra in
 instance instHopfAlgebra : HopfAlgebra R T[M] where
   antipode := antipode R
@@ -119,7 +101,7 @@ instance instHopfAlgebra : HopfAlgebra R T[M] where
         conv =>
           rhs
           rw [convOne_def, comp_apply, CoalgebraStruct.counit, instBialgebra, toCoalgebraStruct,
-            toCoalgebra, ofAlgHom, mk', coe_coe, counit_ι_apply, map_zero]
+            toCoalgebra, ofAlgHom, mk', coe_coe, algebraMapInv_ι_apply, map_zero]
         conv =>
           lhs
           rw [convMul_apply, CoalgebraStruct.comul, toCoalgebraStruct, toCoalgebra]
@@ -169,7 +151,7 @@ instance instHopfAlgebra : HopfAlgebra R T[M] where
         conv =>
           rhs
           rw [convOne_def, comp_apply, CoalgebraStruct.counit, instBialgebra, toCoalgebraStruct,
-            toCoalgebra, ofAlgHom, mk', coe_coe, counit_ι_apply, map_zero]
+            toCoalgebra, ofAlgHom, mk', coe_coe, algebraMapInv_ι_apply, map_zero]
         conv =>
           lhs
           rw [convMul_apply, CoalgebraStruct.comul, toCoalgebraStruct, toCoalgebra]
@@ -207,4 +189,6 @@ instance instHopfAlgebra : HopfAlgebra R T[M] where
             ← Algebra.commutes, mul_assoc]
           rw [← Finset.mul_sum, hu, ← convOne_apply]
 
+end HopfAlgebra
+
 end TensorAlgebra

From f00ee29e818fba4e499f5029517046881f8aaad6 Mon Sep 17 00:00:00 2001
From: Nikolas Tapia <tapia@wias-berlin.de>
Date: Sat, 22 Nov 2025 12:30:28 +0100
Subject: [PATCH 14/23] apply remainig fix

---
 Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
index 2aa8ed6b613327..eac1539fdfb2e4 100644
--- a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
+++ b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
@@ -35,8 +35,8 @@ It is induced by the linear map sending `(m : M)` to `ι R m ⊗ₜ[R] 1 + 1 ⊗
 See `comul_apply`.
 -/
 def comul : T[M] →ₐ[R] T[M] ⊗[R] T[M] := lift R (
-  ((ι R) ⊗ₘ (Algebra.linearMap R T[M])) ∘ₗ (TensorProduct.rid R M).symm +
-  ((Algebra.linearMap R T[M]) ⊗ₘ (ι R)) ∘ₗ (TensorProduct.lid R M).symm
+  (ι R ⊗ₘ Algebra.linearMap R T[M]) ∘ₗ (TensorProduct.rid R M).symm +
+  (Algebra.linearMap R T[M] ⊗ₘ ι R) ∘ₗ (TensorProduct.lid R M).symm
   )
 
 @[simp]
@@ -48,9 +48,8 @@ lemma algebraMapInv_ι_apply (m : M) : algebraMapInv (ι R m) = 0 := by
   simp [algebraMapInv]
 
 @[simp]
-lemma algebraMapInv_ι_eq_zero : algebraMapInv.toLinearMap ∘ₗ (ι R) = (0 : M →ₗ[R] R) := by
-  ext
-  simp
+lemma algebraMapInv_ι_eq_zero : algebraMapInv.toLinearMap ∘ₗ (ι R) = (0 : M →ₗ[R] R) :=
+  LinearMap.ext <| algebraMapInv_ι_apply _
 
 instance instBialgebra : Bialgebra R T[M] := Bialgebra.ofAlgHom (comul R) algebraMapInv
     (by ext; simpa [comul, Algebra.TensorProduct.one_def, add_tmul, tmul_add] using by abel)

From 19d9c1d60ea8d4a91b4b26f0dcd59942934af571 Mon Sep 17 00:00:00 2001
From: Nikolas Tapia <tapia@wias-berlin.de>
Date: Sat, 22 Nov 2025 12:58:47 +0100
Subject: [PATCH 15/23] missing fix

---
 Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
index eac1539fdfb2e4..37bf790a4873d8 100644
--- a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
+++ b/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
@@ -69,7 +69,7 @@ def antipode : T[M] →ₗ[R] T[M] := (MulOpposite.opLinearEquiv R).symm.comp
   (lift R ((MulOpposite.opLinearEquiv R).comp (-(ι R)))).toLinearMap
 
 @[simp]
-lemma antipode_ι_apply (x : M) : antipode R ((ι R) x) = -(ι R) x := by
+lemma antipode_ι_apply (x : M) : antipode R (ι R x) = -(ι R) x := by
   simp [antipode]
 
 @[simp]

From 40743ea28f03babcc5313c7ca6b11a75db2c4528 Mon Sep 17 00:00:00 2001
From: Nikolas Tapia <tapia@wias-berlin.de>
Date: Sat, 22 Nov 2025 13:03:04 +0100
Subject: [PATCH 16/23] move file

---
 Mathlib.lean                                                    | 2 +-
 .../Hopf.lean => RingTheory/HopfAlgebra/TensorAlgebra.lean}     | 0
 2 files changed, 1 insertion(+), 1 deletion(-)
 rename Mathlib/{LinearAlgebra/TensorAlgebra/Hopf.lean => RingTheory/HopfAlgebra/TensorAlgebra.lean} (100%)

diff --git a/Mathlib.lean b/Mathlib.lean
index 10047fc3bd06a4..6cf89a2562735e 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -4598,7 +4598,6 @@ public import Mathlib.LinearAlgebra.SymplecticGroup
 public import Mathlib.LinearAlgebra.TensorAlgebra.Basic
 public import Mathlib.LinearAlgebra.TensorAlgebra.Basis
 public import Mathlib.LinearAlgebra.TensorAlgebra.Grading
-public import Mathlib.LinearAlgebra.TensorAlgebra.Hopf
 public import Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
 public import Mathlib.LinearAlgebra.TensorPower.Basic
 public import Mathlib.LinearAlgebra.TensorPower.Pairing
@@ -5793,6 +5792,7 @@ public import Mathlib.RingTheory.Henselian
 public import Mathlib.RingTheory.HopfAlgebra.Basic
 public import Mathlib.RingTheory.HopfAlgebra.GroupLike
 public import Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
+public import Mathlib.RingTheory.HopfAlgebra.TensorAlgebra
 public import Mathlib.RingTheory.HopfAlgebra.TensorProduct
 public import Mathlib.RingTheory.HopkinsLevitzki
 public import Mathlib.RingTheory.Ideal.AssociatedPrime
diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean b/Mathlib/RingTheory/HopfAlgebra/TensorAlgebra.lean
similarity index 100%
rename from Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
rename to Mathlib/RingTheory/HopfAlgebra/TensorAlgebra.lean

From e37d201883150f1ede8a15b489331e2c080618ba Mon Sep 17 00:00:00 2001
From: Nikolas Tapia <tapia@wias-berlin.de>
Date: Sat, 22 Nov 2025 14:02:38 +0100
Subject: [PATCH 17/23] more style changes

---
 Mathlib/RingTheory/HopfAlgebra/TensorAlgebra.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/Mathlib/RingTheory/HopfAlgebra/TensorAlgebra.lean b/Mathlib/RingTheory/HopfAlgebra/TensorAlgebra.lean
index 37bf790a4873d8..02ba6501cc53fc 100644
--- a/Mathlib/RingTheory/HopfAlgebra/TensorAlgebra.lean
+++ b/Mathlib/RingTheory/HopfAlgebra/TensorAlgebra.lean
@@ -64,12 +64,12 @@ variable (R : Type*) [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
 
 local notation "T[" M "]" => TensorAlgebra R M
 
-/-- Antipode in `TensorAlgebra R M` as an algebra map. -/
+/-- Antipode in `TensorAlgebra R M` as a linear map. -/
 def antipode : T[M] →ₗ[R] T[M] := (MulOpposite.opLinearEquiv R).symm.comp
-  (lift R ((MulOpposite.opLinearEquiv R).comp (-(ι R)))).toLinearMap
+  (lift R <| (MulOpposite.opLinearEquiv R).comp <| -ι R).toLinearMap
 
 @[simp]
-lemma antipode_ι_apply (x : M) : antipode R (ι R x) = -(ι R) x := by
+lemma antipode_ι_apply (x : M) : antipode R (ι R x) = -ι R x := by
   simp [antipode]
 
 @[simp]
@@ -78,13 +78,13 @@ theorem antipode_antihom_apply (x y : T[M]) : antipode R (x * y) = antipode R y
 
 @[simp]
 theorem antipode_antihom : antipode R ∘ₗ mul' R T[M] =
-    mul' R T[M] ∘ₗ TensorProduct.comm R T[M] T[M] ∘ₗ ((antipode R) ⊗ₘ (antipode R)) := by
+    mul' R T[M] ∘ₗ TensorProduct.comm R T[M] T[M] ∘ₗ (antipode R ⊗ₘ antipode R) := by
   ext
   simp
 
 @[simp]
 lemma antipode_algebraMap_apply (r : R) :
-    antipode R ((algebraMap R T[M]) r) = algebraMap R T[M] r := by
+    antipode R (algebraMap R T[M] r) = algebraMap R T[M] r := by
   simp [antipode]
 
 open Algebra Bialgebra Coalgebra in

From 1807384184c68aa081abe1babf2a9d354cc47f86 Mon Sep 17 00:00:00 2001
From: Nikolas Tapia <tapia@wias-berlin.de>
Date: Sat, 22 Nov 2025 22:13:49 +0100
Subject: [PATCH 18/23] split files

---
 Mathlib.lean                                  |  1 +
 .../RingTheory/Bialgebra/TensorAlgebra.lean   | 56 +++++++++++
 .../RingTheory/HopfAlgebra/TensorAlgebra.lean | 99 ++++++-------------
 3 files changed, 88 insertions(+), 68 deletions(-)
 create mode 100644 Mathlib/RingTheory/Bialgebra/TensorAlgebra.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 6cf89a2562735e..b983c3cfbb639f 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -5660,6 +5660,7 @@ public import Mathlib.RingTheory.Bialgebra.Equiv
 public import Mathlib.RingTheory.Bialgebra.GroupLike
 public import Mathlib.RingTheory.Bialgebra.Hom
 public import Mathlib.RingTheory.Bialgebra.MonoidAlgebra
+public import Mathlib.RingTheory.Bialgebra.TensorAlgebra
 public import Mathlib.RingTheory.Bialgebra.TensorProduct
 public import Mathlib.RingTheory.Binomial
 public import Mathlib.RingTheory.ChainOfDivisors
diff --git a/Mathlib/RingTheory/Bialgebra/TensorAlgebra.lean b/Mathlib/RingTheory/Bialgebra/TensorAlgebra.lean
new file mode 100644
index 00000000000000..c363e9ed86f373
--- /dev/null
+++ b/Mathlib/RingTheory/Bialgebra/TensorAlgebra.lean
@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2025 Nikolas Tapia. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nikolas Tapia
+-/
+module
+
+public import Mathlib.LinearAlgebra.TensorAlgebra.Basic
+public import Mathlib.RingTheory.Bialgebra.Basic
+
+/-!
+# Bialgebra structure on `TensorAlgebra R M`
+
+In this file we implement the natural bialgebra structure on `TensorAlgebra R M`.
+The comultiplication is the unique algebra map satisfying `comul (ι R x) = ι R x ⊗ 1 + 1 ⊗ ι R
+x` for all `x : M`, and `algebraMapInv` acts as the counit.
+-/
+
+@[expose] public section
+
+namespace TensorAlgebra
+
+open scoped TensorProduct RingTheory.LinearMap
+open TensorProduct
+
+variable (R : Type*) [CommSemiring R] {M : Type*} [AddCommMonoid M] [Module R M]
+
+local notation "T[" M "]" => TensorAlgebra R M
+
+/-- Comultiplication in `TensorAlgebra R M` as an algebra map.
+It is induced by the linear map sending `(m : M)` to `ι R m ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ι R m`.
+See `comul_apply`.
+-/
+def comul : T[M] →ₐ[R] T[M] ⊗[R] T[M] := lift R (
+  (ι R ⊗ₘ Algebra.linearMap R T[M]) ∘ₗ (TensorProduct.rid R M).symm +
+  (Algebra.linearMap R T[M] ⊗ₘ ι R) ∘ₗ (TensorProduct.lid R M).symm
+  )
+
+@[simp]
+lemma comul_apply (m : M) : comul R (ι R m) = ι R m ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ι R m := by
+  simp [comul]
+
+@[simp]
+lemma algebraMapInv_ι_apply (m : M) : algebraMapInv (ι R m) = 0 := by
+  simp [algebraMapInv]
+
+@[simp]
+lemma algebraMapInv_ι_eq_zero : algebraMapInv.toLinearMap ∘ₗ (ι R) = (0 : M →ₗ[R] R) :=
+  LinearMap.ext <| algebraMapInv_ι_apply _
+
+instance instBialgebra : Bialgebra R T[M] := Bialgebra.ofAlgHom (comul R) algebraMapInv
+    (by ext; simpa [comul, Algebra.TensorProduct.one_def, add_tmul, tmul_add] using by abel)
+    (by ext; simp [comul, algebraMapInv])
+    (by ext; simp [comul, algebraMapInv])
+
+end TensorAlgebra
diff --git a/Mathlib/RingTheory/HopfAlgebra/TensorAlgebra.lean b/Mathlib/RingTheory/HopfAlgebra/TensorAlgebra.lean
index 02ba6501cc53fc..6bd616eeb4ba26 100644
--- a/Mathlib/RingTheory/HopfAlgebra/TensorAlgebra.lean
+++ b/Mathlib/RingTheory/HopfAlgebra/TensorAlgebra.lean
@@ -5,8 +5,7 @@ Authors: Nikolas Tapia
 -/
 module
 
-public import Mathlib.LinearAlgebra.TensorAlgebra.Basic
-public import Mathlib.RingTheory.Coalgebra.Convolution
+public import Mathlib.RingTheory.Bialgebra.TensorAlgebra
 public import Mathlib.RingTheory.HopfAlgebra.Basic
 
 /-!
@@ -21,44 +20,9 @@ TensorAlgebra R M → (TensorAlgebra R M)ᵐᵒᵖ` induced by `fun x => op -(ι
 @[expose] public section
 
 namespace TensorAlgebra
-open scoped TensorProduct RingTheory.LinearMap Coalgebra
-open LinearMap TensorProduct
-
-section Bialgebra
-
-variable (R : Type*) [CommSemiring R] {M : Type*} [AddCommMonoid M] [Module R M]
-
-local notation "T[" M "]" => TensorAlgebra R M
-
-/-- Comultiplication in `TensorAlgebra R M` as an algebra map.
-It is induced by the linear map sending `(m : M)` to `ι R m ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ι R m`.
-See `comul_apply`.
--/
-def comul : T[M] →ₐ[R] T[M] ⊗[R] T[M] := lift R (
-  (ι R ⊗ₘ Algebra.linearMap R T[M]) ∘ₗ (TensorProduct.rid R M).symm +
-  (Algebra.linearMap R T[M] ⊗ₘ ι R) ∘ₗ (TensorProduct.lid R M).symm
-  )
-
-@[simp]
-lemma comul_apply (m : M) : comul R (ι R m) = ι R m ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ι R m := by
-  simp [comul]
 
-@[simp]
-lemma algebraMapInv_ι_apply (m : M) : algebraMapInv (ι R m) = 0 := by
-  simp [algebraMapInv]
-
-@[simp]
-lemma algebraMapInv_ι_eq_zero : algebraMapInv.toLinearMap ∘ₗ (ι R) = (0 : M →ₗ[R] R) :=
-  LinearMap.ext <| algebraMapInv_ι_apply _
-
-instance instBialgebra : Bialgebra R T[M] := Bialgebra.ofAlgHom (comul R) algebraMapInv
-    (by ext; simpa [comul, Algebra.TensorProduct.one_def, add_tmul, tmul_add] using by abel)
-    (by ext; simp [comul, algebraMapInv])
-    (by ext; simp [comul, algebraMapInv])
-
-end Bialgebra
-
-section HopfAlgebra
+open scoped RingTheory.LinearMap
+open LinearMap TensorProduct
 
 variable (R : Type*) [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
 
@@ -91,7 +55,7 @@ open Algebra Bialgebra Coalgebra in
 instance instHopfAlgebra : HopfAlgebra R T[M] where
   antipode := antipode R
   mul_antipode_rTensor_comul := by
-    rw [LinearMap.rTensor, ← LinearMap.convMul_def, ← convOne_def]
+    rw [LinearMap.rTensor]
     ext x
     induction x using induction with
     | algebraMap r => simp
@@ -99,23 +63,24 @@ instance instHopfAlgebra : HopfAlgebra R T[M] where
     | ι u =>
         conv =>
           rhs
-          rw [convOne_def, comp_apply, CoalgebraStruct.counit, instBialgebra, toCoalgebraStruct,
+          rw [comp_apply, CoalgebraStruct.counit, instBialgebra, toCoalgebraStruct,
             toCoalgebra, ofAlgHom, mk', coe_coe, algebraMapInv_ι_apply, map_zero]
         conv =>
           lhs
-          rw [convMul_apply, CoalgebraStruct.comul, toCoalgebraStruct, toCoalgebra]
+          rw [CoalgebraStruct.comul, toCoalgebraStruct, toCoalgebra]
           unfold instBialgebra ofAlgHom mk'
-          simp only [coe_coe, comul_apply, map_add, map_tmul, antipode_ι_apply, id_coe, id_eq,
-            mul'_apply, mul_one, ← map_one (algebraMap R T[M]), antipode_algebraMap_apply]
-          simp only [map_one, mul_one, one_mul, neg_add_cancel]
+          simp only [coe_semilinearMap, comp_apply, comul_apply, map_add, map_tmul,
+            antipode_ι_apply, id_coe, id_eq, mul'_apply, mul_one]
+          rw [← map_one (algebraMap R _), antipode_algebraMap_apply]
+          simp
     | mul u v hu hv =>
         conv =>
           rhs
-          rw [convOne_apply, counit_mul, map_mul, ← convOne_apply, ← convOne_apply]
+          rw [comp_apply, counit_mul]
         have assoc4 {Q} [Semiring Q] (a b c d : Q) : a * b * (c * d) = a * (b * c) * d := by
           rw [← mul_assoc, mul_assoc a b c]
-        rw [convMul_apply, comul_mul, ← Coalgebra.Repr.eq (ℛ R u), ← Coalgebra.Repr.eq (ℛ R v),
-          Finset.sum_mul_sum, map_sum, map_sum] at *
+        rw [comp_apply, comp_apply, comul_mul, ← Coalgebra.Repr.eq (ℛ R u),
+          ← Coalgebra.Repr.eq (ℛ R v), Finset.sum_mul_sum, map_sum, map_sum] at *
         simp only [TensorProduct.tmul_mul_tmul, map_sum, map_tmul, antipode_antihom_apply, id_coe,
         id_eq, mul'_apply] at *
         conv =>
@@ -133,41 +98,40 @@ instance instHopfAlgebra : HopfAlgebra R T[M] where
           conv =>
             arg 2
             intro i
-            rw [← Finset.sum_mul, ← Finset.mul_sum, hu, convOne_apply,
-            ← Algebra.commutes, mul_assoc]
-          rw [← Finset.mul_sum, hv, ← convOne_apply]
+            rw [← Finset.sum_mul, ← Finset.mul_sum, hu, comp_apply, linearMap_apply,
+              ← commutes, mul_assoc]
+          rw [← Finset.mul_sum, hv, comp_apply, linearMap_apply, ← map_mul, ← linearMap_apply]
   mul_antipode_lTensor_comul := by
-    rw [LinearMap.lTensor, ← LinearMap.convMul_def, ← convOne_def]
+    rw [LinearMap.lTensor]
     ext x
     induction x using induction with
     | algebraMap r =>
-        simp only [convMul_apply, comul_algebraMap, TensorProduct.algebraMap_apply, map_tmul,
-          id_coe, id_eq, mul'_apply, convOne_apply, counit_algebraMap, ← map_one (algebraMap R
+        simp only [comp_apply, comul_algebraMap, TensorProduct.algebraMap_apply, map_tmul,
+          id_coe, id_eq, mul'_apply, counit_algebraMap, ← map_one (algebraMap R
           T[M]), antipode_algebraMap_apply]
         simp
     | add u v hu hv => rw [map_add, hu, hv, ← map_add]
     | ι u =>
         conv =>
           rhs
-          rw [convOne_def, comp_apply, CoalgebraStruct.counit, instBialgebra, toCoalgebraStruct,
+          rw [comp_apply, CoalgebraStruct.counit, instBialgebra, toCoalgebraStruct,
             toCoalgebra, ofAlgHom, mk', coe_coe, algebraMapInv_ι_apply, map_zero]
         conv =>
           lhs
-          rw [convMul_apply, CoalgebraStruct.comul, toCoalgebraStruct, toCoalgebra]
+          rw [CoalgebraStruct.comul, toCoalgebraStruct, toCoalgebra]
           unfold instBialgebra ofAlgHom mk'
           simp only [coe_coe, comul_apply, map_add, map_tmul, antipode_ι_apply, id_coe, id_eq,
-            mul'_apply, mul_one, ← map_one (algebraMap R T[M]), antipode_algebraMap_apply]
-          simp only [map_one, mul_one, one_mul, neg_add_cancel]
-          abel_nf
+            mul'_apply, mul_one, ← map_one (algebraMap R T[M]), antipode_algebraMap_apply,
+            coe_semilinearMap, comp_apply]
+          rw [map_one, one_mul, mul_one, add_neg_cancel]
     | mul u v hu hv =>
         conv =>
           rhs
-          rw [convOne_apply, counit_mul, map_mul, Algebra.commutes, ← convOne_apply,
-            ← convOne_apply]
+          rw [comp_apply, counit_mul]
         have assoc4 {Q} [Semiring Q] (a b c d : Q) : a * b * (c * d) = a * (b * c) * d := by
           rw [← mul_assoc, mul_assoc a b c]
-        rw [convMul_apply, comul_mul, ← Coalgebra.Repr.eq (ℛ R u), ← Coalgebra.Repr.eq (ℛ R v),
-          Finset.sum_mul_sum, map_sum, map_sum] at *
+        rw [comp_apply, comp_apply, comul_mul, ← Coalgebra.Repr.eq (ℛ R u),
+          ← Coalgebra.Repr.eq (ℛ R v), Finset.sum_mul_sum, map_sum, map_sum] at *
         simp only [TensorProduct.tmul_mul_tmul, map_sum, map_tmul, antipode_antihom_apply, id_coe,
         id_eq, mul'_apply] at *
         conv =>
@@ -184,10 +148,9 @@ instance instHopfAlgebra : HopfAlgebra R T[M] where
           conv =>
             arg 2
             intro i
-            rw [← Finset.sum_mul, ← Finset.mul_sum, hv, convOne_apply,
-            ← Algebra.commutes, mul_assoc]
-          rw [← Finset.mul_sum, hu, ← convOne_apply]
-
-end HopfAlgebra
+            rw [← Finset.sum_mul, ← Finset.mul_sum, hv, comp_apply, linearMap_apply,
+              ← Algebra.commutes, mul_assoc]
+          rw [← Finset.mul_sum, hu, comp_apply, linearMap_apply, commutes, ← map_mul,
+            ← linearMap_apply]
 
 end TensorAlgebra

From 00371892f2ad350aee659fe9462a4cd122fd87d4 Mon Sep 17 00:00:00 2001
From: Nikolas Tapia <tapia@wias-berlin.de>
Date: Sat, 22 Nov 2025 23:24:15 +0100
Subject: [PATCH 19/23] edit doc for .HopfAlgebra.TensorAlgebra

---
 Mathlib/RingTheory/HopfAlgebra/TensorAlgebra.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/RingTheory/HopfAlgebra/TensorAlgebra.lean b/Mathlib/RingTheory/HopfAlgebra/TensorAlgebra.lean
index 6bd616eeb4ba26..945b78853b3117 100644
--- a/Mathlib/RingTheory/HopfAlgebra/TensorAlgebra.lean
+++ b/Mathlib/RingTheory/HopfAlgebra/TensorAlgebra.lean
@@ -12,10 +12,10 @@ public import Mathlib.RingTheory.HopfAlgebra.Basic
 # Hopf algebra structure on `TensorAlgebra R M`
 
 In this file we implement the natura Hopf algebra structure on `TensorAlgebra R M`.
-The comultiplication is the unique algebra map satisfying `comul ((ι R) x) = (ι R) x ⊗ 1 + 1 ⊗ (ι R)
-x` for all `x : M`.
-`algebraMapInv` acts as the counit, and the antipode is the unique algebra map `antipode :
-TensorAlgebra R M → (TensorAlgebra R M)ᵐᵒᵖ` induced by `fun x => op -(ι R) x`.
+The bialgebra structure is implemented in `TensorAlgebra.instBialgebra`.
+
+The antipode is the unique algebra map `antipode : TensorAlgebra R M → (TensorAlgebra R M)ᵐᵒᵖ`
+induced by `fun x => op -(ι R x)`.
 -/
 @[expose] public section
 

From 9fe7619bdffd3d9c4de6ccd04e2899dcee629252 Mon Sep 17 00:00:00 2001
From: Nikolas Tapia <tapia@wias-berlin.de>
Date: Mon, 24 Nov 2025 19:45:16 +0100
Subject: [PATCH 20/23] apply suggestions

---
 .../LinearAlgebra/TensorAlgebra/Basic.lean    |  8 +++++
 .../RingTheory/Bialgebra/TensorAlgebra.lean   | 29 +++++--------------
 2 files changed, 15 insertions(+), 22 deletions(-)

diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
index 4f8fefefd49b81..cd4ea331ef4629 100644
--- a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
+++ b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
@@ -221,6 +221,14 @@ theorem range_lift {A : Type*} [Semiring A] [Algebra R A] (f : M →ₗ[R] A) :
 def algebraMapInv : TensorAlgebra R M →ₐ[R] R :=
   lift R (0 : M →ₗ[R] R)
 
+@[simp]
+lemma algebraMapInv_ι_apply (m : M) : algebraMapInv (ι R m) = 0 := by
+  simp [algebraMapInv]
+
+@[simp]
+lemma algebraMapInv_ι_eq_zero : algebraMapInv.toLinearMap ∘ₗ ι R = (0 : M →ₗ[R] R) :=
+  LinearMap.ext <| algebraMapInv_ι_apply
+
 variable (M)
 
 theorem algebraMap_leftInverse :
diff --git a/Mathlib/RingTheory/Bialgebra/TensorAlgebra.lean b/Mathlib/RingTheory/Bialgebra/TensorAlgebra.lean
index c363e9ed86f373..0a7edc6ecdf800 100644
--- a/Mathlib/RingTheory/Bialgebra/TensorAlgebra.lean
+++ b/Mathlib/RingTheory/Bialgebra/TensorAlgebra.lean
@@ -23,34 +23,19 @@ namespace TensorAlgebra
 open scoped TensorProduct RingTheory.LinearMap
 open TensorProduct
 
-variable (R : Type*) [CommSemiring R] {M : Type*} [AddCommMonoid M] [Module R M]
-
-local notation "T[" M "]" => TensorAlgebra R M
+variable {R : Type*} [CommSemiring R] {M : Type*} [AddCommMonoid M] [Module R M]
 
 /-- Comultiplication in `TensorAlgebra R M` as an algebra map.
 It is induced by the linear map sending `(m : M)` to `ι R m ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ι R m`.
 See `comul_apply`.
 -/
-def comul : T[M] →ₐ[R] T[M] ⊗[R] T[M] := lift R (
-  (ι R ⊗ₘ Algebra.linearMap R T[M]) ∘ₗ (TensorProduct.rid R M).symm +
-  (Algebra.linearMap R T[M] ⊗ₘ ι R) ∘ₗ (TensorProduct.lid R M).symm
-  )
-
-@[simp]
-lemma comul_apply (m : M) : comul R (ι R m) = ι R m ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ι R m := by
-  simp [comul]
-
-@[simp]
-lemma algebraMapInv_ι_apply (m : M) : algebraMapInv (ι R m) = 0 := by
-  simp [algebraMapInv]
-
-@[simp]
-lemma algebraMapInv_ι_eq_zero : algebraMapInv.toLinearMap ∘ₗ (ι R) = (0 : M →ₗ[R] R) :=
-  LinearMap.ext <| algebraMapInv_ι_apply _
+def comul : TensorAlgebra R M →ₐ[R] TensorAlgebra R M ⊗[R] TensorAlgebra R M := lift R <|
+  (ι R ⊗ₘ Algebra.linearMap R (TensorAlgebra R M)) ∘ₗ (TensorProduct.rid R M).symm +
+  (Algebra.linearMap R (TensorAlgebra R M) ⊗ₘ ι R) ∘ₗ (TensorProduct.lid R M).symm
 
-instance instBialgebra : Bialgebra R T[M] := Bialgebra.ofAlgHom (comul R) algebraMapInv
+instance instBialgebra : Bialgebra R (TensorAlgebra R M) := Bialgebra.ofAlgHom comul algebraMapInv
     (by ext; simpa [comul, Algebra.TensorProduct.one_def, add_tmul, tmul_add] using by abel)
-    (by ext; simp [comul, algebraMapInv])
-    (by ext; simp [comul, algebraMapInv])
+    (by ext; simp [comul])
+    (by ext; simp [comul])
 
 end TensorAlgebra

From a85323ddff46934e46ae4a085a39c03ef104a037 Mon Sep 17 00:00:00 2001
From: Nikolas Tapia <tapia@wias-berlin.de>
Date: Sun, 30 Nov 2025 14:54:52 +0100
Subject: [PATCH 21/23] implement for FreeAlgebra

---
 Mathlib.lean                                  |  2 ++
 Mathlib/Algebra/FreeAlgebra.lean              |  4 +++
 Mathlib/RingTheory/Bialgebra/FreeAlgebra.lean | 35 +++++++++++++++++++
 Mathlib/RingTheory/Coalgebra/FreeAlgebra.lean | 28 +++++++++++++++
 4 files changed, 69 insertions(+)
 create mode 100644 Mathlib/RingTheory/Bialgebra/FreeAlgebra.lean
 create mode 100644 Mathlib/RingTheory/Coalgebra/FreeAlgebra.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index b983c3cfbb639f..91a82157613ab5 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -5657,6 +5657,7 @@ public import Mathlib.RingTheory.Artinian.Ring
 public import Mathlib.RingTheory.Bezout
 public import Mathlib.RingTheory.Bialgebra.Basic
 public import Mathlib.RingTheory.Bialgebra.Equiv
+public import Mathlib.RingTheory.Bialgebra.FreeAlgebra
 public import Mathlib.RingTheory.Bialgebra.GroupLike
 public import Mathlib.RingTheory.Bialgebra.Hom
 public import Mathlib.RingTheory.Bialgebra.MonoidAlgebra
@@ -5668,6 +5669,7 @@ public import Mathlib.RingTheory.ClassGroup
 public import Mathlib.RingTheory.Coalgebra.Basic
 public import Mathlib.RingTheory.Coalgebra.Convolution
 public import Mathlib.RingTheory.Coalgebra.Equiv
+public import Mathlib.RingTheory.Coalgebra.FreeAlgebra
 public import Mathlib.RingTheory.Coalgebra.GroupLike
 public import Mathlib.RingTheory.Coalgebra.Hom
 public import Mathlib.RingTheory.Coalgebra.MonoidAlgebra
diff --git a/Mathlib/Algebra/FreeAlgebra.lean b/Mathlib/Algebra/FreeAlgebra.lean
index 20b263bc974f17..8997c0a94d130d 100644
--- a/Mathlib/Algebra/FreeAlgebra.lean
+++ b/Mathlib/Algebra/FreeAlgebra.lean
@@ -478,6 +478,10 @@ section
 def algebraMapInv : FreeAlgebra R X →ₐ[R] R :=
   lift R (0 : X → R)
 
+@[simp]
+lemma algebraMapInv_ι_apply (x : X) : algebraMapInv (ι R x) = 0 := by
+  simp [algebraMapInv]
+
 theorem algebraMap_leftInverse :
     Function.LeftInverse algebraMapInv (algebraMap R <| FreeAlgebra R X) := fun x ↦ by
   simp [algebraMapInv]
diff --git a/Mathlib/RingTheory/Bialgebra/FreeAlgebra.lean b/Mathlib/RingTheory/Bialgebra/FreeAlgebra.lean
new file mode 100644
index 00000000000000..e7b5184ca6c67f
--- /dev/null
+++ b/Mathlib/RingTheory/Bialgebra/FreeAlgebra.lean
@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2025 Nikolas Tapia. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nikolas Tapia
+-/
+module
+
+public import Mathlib.Algebra.FreeAlgebra
+public import Mathlib.RingTheory.Bialgebra.Basic
+
+/-!
+# Bialgebra structure on `FreeAlgebra R M`
+
+In this file we implement the natural bialgebra structure on `FreeAlgebra R M`.
+The comultiplication is the unique algebra map satisfying `comul (ι R x) = ι R x ⊗ 1 + 1 ⊗ ι R
+x` for all `x : M`, and `algebraMapInv` acts as the counit.
+-/
+
+@[expose] public section
+
+open FreeAlgebra TensorProduct
+open scoped TensorProduct
+
+namespace FreeAlgebra
+
+variable (R X) [CommSemiring R]
+
+instance instBialgebra : Bialgebra R (FreeAlgebra R X) := Bialgebra.ofAlgHom
+  (lift R <| fun (x : X) => ι R x ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ι R x)
+  algebraMapInv
+  (by ext; simpa [tmul_add, add_tmul, Algebra.TensorProduct.one_def] using by abel)
+  (by ext; simp)
+  (by ext; simp)
+
+end FreeAlgebra
diff --git a/Mathlib/RingTheory/Coalgebra/FreeAlgebra.lean b/Mathlib/RingTheory/Coalgebra/FreeAlgebra.lean
new file mode 100644
index 00000000000000..069a60e2a63fe1
--- /dev/null
+++ b/Mathlib/RingTheory/Coalgebra/FreeAlgebra.lean
@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2025 Nikolas Tapia. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nikolas Tapia
+-/
+module
+
+public import Mathlib.Algebra.FreeAlgebra
+public import Mathlib.RingTheory.Bialgebra.FreeAlgebra
+
+/-!
+# Coalgebra structure on `FreeAlgebra R M`
+
+In this file we implement the natural bialgebra structure on `FreeAlgebra R M`.
+The comultiplication is the unique algebra map satisfying `comul (ι R x) = ι R x ⊗ 1 + 1 ⊗ ι R
+x` for all `x : M`.
+-/
+
+@[expose] public section
+
+namespace FreeAlgebra
+
+variable (R X) [CommSemiring R]
+
+instance instCoalgebra : Coalgebra R (FreeAlgebra R X) :=
+  (FreeAlgebra.instBialgebra R X).toCoalgebra
+
+end FreeAlgebra

From eb726410f7bcc74548cbff93204822b7be502bab Mon Sep 17 00:00:00 2001
From: Nikolas Tapia <tapia@wias-berlin.de>
Date: Tue, 2 Dec 2025 14:11:07 +0100
Subject: [PATCH 22/23] apply suggestions

---
 Mathlib/Algebra/FreeAlgebra.lean              |  2 +-
 Mathlib/RingTheory/Bialgebra/FreeAlgebra.lean | 10 +++++--
 Mathlib/RingTheory/Coalgebra/FreeAlgebra.lean | 28 -------------------
 3 files changed, 9 insertions(+), 31 deletions(-)
 delete mode 100644 Mathlib/RingTheory/Coalgebra/FreeAlgebra.lean

diff --git a/Mathlib/Algebra/FreeAlgebra.lean b/Mathlib/Algebra/FreeAlgebra.lean
index 8997c0a94d130d..7e548866194624 100644
--- a/Mathlib/Algebra/FreeAlgebra.lean
+++ b/Mathlib/Algebra/FreeAlgebra.lean
@@ -479,7 +479,7 @@ def algebraMapInv : FreeAlgebra R X →ₐ[R] R :=
   lift R (0 : X → R)
 
 @[simp]
-lemma algebraMapInv_ι_apply (x : X) : algebraMapInv (ι R x) = 0 := by
+lemma algebraMapInv_ι (x : X) : algebraMapInv (ι R x) = 0 := by
   simp [algebraMapInv]
 
 theorem algebraMap_leftInverse :
diff --git a/Mathlib/RingTheory/Bialgebra/FreeAlgebra.lean b/Mathlib/RingTheory/Bialgebra/FreeAlgebra.lean
index e7b5184ca6c67f..57bb983a87534c 100644
--- a/Mathlib/RingTheory/Bialgebra/FreeAlgebra.lean
+++ b/Mathlib/RingTheory/Bialgebra/FreeAlgebra.lean
@@ -26,10 +26,16 @@ namespace FreeAlgebra
 variable (R X) [CommSemiring R]
 
 instance instBialgebra : Bialgebra R (FreeAlgebra R X) := Bialgebra.ofAlgHom
-  (lift R <| fun (x : X) => ι R x ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ι R x)
+  (lift R fun x => ι R x ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ι R x)
   algebraMapInv
-  (by ext; simpa [tmul_add, add_tmul, Algebra.TensorProduct.one_def] using by abel)
+  (by ext; simp [tmul_add, add_tmul, Algebra.TensorProduct.one_def]; abel)
   (by ext; simp)
   (by ext; simp)
 
+/-- The comultiplication is the unique algebra map satisfying `comul (ι R x) = ι R x ⊗ 1 + 1 ⊗ ι R
+x` for all `x : M` -/
+@[simp]
+lemma comul_ι (x : X) : Coalgebra.comul (ι R x) = ι R x ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ι R x := by
+  simp [CoalgebraStruct.comul, instBialgebra, Bialgebra.mk']
+
 end FreeAlgebra
diff --git a/Mathlib/RingTheory/Coalgebra/FreeAlgebra.lean b/Mathlib/RingTheory/Coalgebra/FreeAlgebra.lean
deleted file mode 100644
index 069a60e2a63fe1..00000000000000
--- a/Mathlib/RingTheory/Coalgebra/FreeAlgebra.lean
+++ /dev/null
@@ -1,28 +0,0 @@
-/-
-Copyright (c) 2025 Nikolas Tapia. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Nikolas Tapia
--/
-module
-
-public import Mathlib.Algebra.FreeAlgebra
-public import Mathlib.RingTheory.Bialgebra.FreeAlgebra
-
-/-!
-# Coalgebra structure on `FreeAlgebra R M`
-
-In this file we implement the natural bialgebra structure on `FreeAlgebra R M`.
-The comultiplication is the unique algebra map satisfying `comul (ι R x) = ι R x ⊗ 1 + 1 ⊗ ι R
-x` for all `x : M`.
--/
-
-@[expose] public section
-
-namespace FreeAlgebra
-
-variable (R X) [CommSemiring R]
-
-instance instCoalgebra : Coalgebra R (FreeAlgebra R X) :=
-  (FreeAlgebra.instBialgebra R X).toCoalgebra
-
-end FreeAlgebra

From d777657c680d2e2977c91a2ecf66eabfa6503451 Mon Sep 17 00:00:00 2001
From: Nikolas Tapia <tapia@wias-berlin.de>
Date: Wed, 3 Dec 2025 11:13:13 +0100
Subject: [PATCH 23/23] update Mathlib.lean

---
 Mathlib.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index ab86d3d4ff99e2..ee52ca5c8193fc 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -5773,7 +5773,6 @@ public import Mathlib.RingTheory.ClassGroup
 public import Mathlib.RingTheory.Coalgebra.Basic
 public import Mathlib.RingTheory.Coalgebra.Convolution
 public import Mathlib.RingTheory.Coalgebra.Equiv
-public import Mathlib.RingTheory.Coalgebra.FreeAlgebra
 public import Mathlib.RingTheory.Coalgebra.GroupLike
 public import Mathlib.RingTheory.Coalgebra.Hom
 public import Mathlib.RingTheory.Coalgebra.MonoidAlgebra