refactor(RingTheory/HopfAlgebra): ofConvInverse constructor (#39785)

The antipode of a Hopf algebra is [generally](https://arxiv.org/pdf/1409.8356) the two-sided inverse of the identity in the convolution algebra `End(A)`. When `A` is commutative, algebra homs are closed under convolution and this lifts to AlgHom equality. See [this comment](#31898 (comment)) on #31898.

Author: hawkrobe

Mathlib/RingTheory/HopfAlgebra/Basic.lean

@@ -19,6 +19,9 @@ In this file we define `HopfAlgebra`, and provide instances for:
 
 * `HopfAlgebra R A` : the Hopf algebra structure on an `R`-bialgebra `A`.
 * `HopfAlgebra.antipode` : the `R`-linear map `A →ₗ[R] A`.
+* `HopfAlgebra.ofConvInverse` : construct a Hopf algebra from a two-sided convolution inverse
+  of the identity.
+* `HopfAlgebra.ofAlgHom` : the same for commutative `A`, with `AlgHom` hypotheses.
 
 ## Main results
 
@@ -230,3 +233,40 @@ instance toHopfAlgebra : HopfAlgebra R R where
 theorem antipode_eq_id : antipode R (A := R) = .id := rfl
 
 end CommSemiring
+
+namespace HopfAlgebra
+
+variable {R A : Type*}
+
+open Coalgebra WithConv LinearMap
+
+/-- Upgrade a bialgebra to a Hopf algebra by specifying a convolution inverse of the identity. -/
+noncomputable abbrev ofConvInverse [CommSemiring R] [Semiring A] [Bialgebra R A]
+    (antipode : A →ₗ[R] A)
+    (antipode_convMul_id : toConv antipode * toConv LinearMap.id = 1)
+    (id_convMul_antipode : toConv LinearMap.id * toConv antipode = 1) :
+    HopfAlgebra R A where
+  antipode := antipode
+  mul_antipode_rTensor_comul := by simpa using! congr(($antipode_convMul_id).ofConv)
+  mul_antipode_lTensor_comul := by simpa using! congr(($id_convMul_antipode).ofConv)
+
+/-- Upgrade a commutative bialgebra to a Hopf algebra by specifying the antipode `A →ₐ[R] A`
+with appropriate conditions. -/
+noncomputable abbrev ofAlgHom [CommSemiring R] [CommSemiring A] [Bialgebra R A]
+    (antipode : A →ₐ[R] A)
+    (mul_antipode_rTensor_comul :
+      ((Algebra.TensorProduct.lift antipode (.id R A) fun _ ↦ Commute.all _).comp
+        (Bialgebra.comulAlgHom R A)) = (Algebra.ofId R A).comp (Bialgebra.counitAlgHom R A))
+    (mul_antipode_lTensor_comul :
+      (Algebra.TensorProduct.lift (.id R A) antipode fun _ _ ↦ Commute.all _ _).comp
+        (Bialgebra.comulAlgHom R A) = (Algebra.ofId R A).comp (Bialgebra.counitAlgHom R A)) :
+    HopfAlgebra R A :=
+  ofConvInverse antipode.toLinearMap
+    (WithConv.ext <| by
+      simpa [← Algebra.TensorProduct.lmul'_comp_map]
+        using! congr(($mul_antipode_rTensor_comul).toLinearMap))
+    (WithConv.ext <| by
+      simpa [← Algebra.TensorProduct.lmul'_comp_map]
+        using! congr(($mul_antipode_lTensor_comul).toLinearMap))
+
+end HopfAlgebra

Mathlib/RingTheory/HopfAlgebra/TensorProduct.lean

@@ -17,26 +17,7 @@ We define the Hopf algebra instance on the tensor product of two Hopf algebras.
 
 @[expose] public section
 
-open Coalgebra TensorProduct HopfAlgebra
-
-/-- Upgrade a bialgebra to a Hopf algebra by specifying the antipode as an algebra map with
-appropriate conditions. -/
-noncomputable abbrev HopfAlgebra.ofAlgHom {R A : Type*} [CommSemiring R] [CommSemiring A]
-    [Bialgebra R A] (antipode : A →ₐ[R] A)
-    (mul_antipode_rTensor_comul :
-      ((Algebra.TensorProduct.lift antipode (.id R A) fun _ ↦ .all _).comp
-        (Bialgebra.comulAlgHom R A)) = (Algebra.ofId R A).comp (Bialgebra.counitAlgHom R A))
-    (mul_antipode_lTensor_comul :
-      (Algebra.TensorProduct.lift (.id R A) antipode fun _ _ ↦ .all _ _).comp
-        (Bialgebra.comulAlgHom R A) = (Algebra.ofId R A).comp (Bialgebra.counitAlgHom R A)) :
-    HopfAlgebra R A where
-  antipode := antipode
-  mul_antipode_rTensor_comul := by
-    rw [← Algebra.TensorProduct.lmul'_comp_map] at mul_antipode_rTensor_comul
-    exact congr(($mul_antipode_rTensor_comul).toLinearMap)
-  mul_antipode_lTensor_comul := by
-    rw [← Algebra.TensorProduct.lmul'_comp_map] at mul_antipode_lTensor_comul
-    exact congr(($mul_antipode_lTensor_comul).toLinearMap)
+open Coalgebra HopfAlgebra
 
 namespace TensorProduct