feat(LinearAlgebra/TensorAlgebra): implement HopfAlgebra for TensorAlgebra

Mathlib.lean

@@ -5761,9 +5761,11 @@ 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
+public import Mathlib.RingTheory.Bialgebra.TensorAlgebra
 public import Mathlib.RingTheory.Bialgebra.TensorProduct
 public import Mathlib.RingTheory.Binomial
 public import Mathlib.RingTheory.ChainOfDivisors
@@ -5898,6 +5900,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

Mathlib/Algebra/FreeAlgebra.lean

@@ -478,6 +478,10 @@ section
 def algebraMapInv : FreeAlgebra R X →ₐ[R] R :=
   lift R (0 : X → R)
 
+@[simp]
+lemma algebraMapInv_ι (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]

Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean

@@ -219,6 +219,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 :

Mathlib/RingTheory/Bialgebra/FreeAlgebra.lean

@@ -0,0 +1,41 @@
+/-
+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 => ι R x ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ι R x)
+  algebraMapInv
+  (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

Mathlib/RingTheory/Bialgebra/TensorAlgebra.lean

@@ -0,0 +1,41 @@
+/-
+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]
+
+/-- 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 : 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 (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])
+    (by ext; simp [comul])
+
+end TensorAlgebra

Mathlib/RingTheory/HopfAlgebra/TensorAlgebra.lean

@@ -0,0 +1,156 @@
+/-
+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.RingTheory.Bialgebra.TensorAlgebra
+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 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
+
+namespace TensorAlgebra
+
+open scoped RingTheory.LinearMap
+open LinearMap TensorProduct
+
+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 a linear 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
+  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
+  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
+  mul_antipode_rTensor_comul := by
+    rw [LinearMap.rTensor]
+    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 [comp_apply, CoalgebraStruct.counit, instBialgebra, toCoalgebraStruct,
+            toCoalgebra, ofAlgHom, mk', coe_coe, algebraMapInv_ι_apply, map_zero]
+        conv =>
+          lhs
+          rw [CoalgebraStruct.comul, toCoalgebraStruct, toCoalgebra]
+          unfold instBialgebra ofAlgHom mk'
+          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 [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 [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 =>
+          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, 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]
+    ext x
+    induction x using induction with
+    | 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 [comp_apply, CoalgebraStruct.counit, instBialgebra, toCoalgebraStruct,
+            toCoalgebra, ofAlgHom, mk', coe_coe, algebraMapInv_ι_apply, map_zero]
+        conv =>
+          lhs
+          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,
+            coe_semilinearMap, comp_apply]
+          rw [map_one, one_mul, mul_one, add_neg_cancel]
+    | mul u v hu hv =>
+        conv =>
+          rhs
+          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 [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 =>
+          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, comp_apply, linearMap_apply,
+              ← Algebra.commutes, mul_assoc]
+          rw [← Finset.mul_sum, hu, comp_apply, linearMap_apply, commutes, ← map_mul,
+            ← linearMap_apply]
+
+end TensorAlgebra