feat(RingTheory/HopfAlgebra): construct from anti-algebra hom

Author: hawkrobe

Mathlib/RingTheory/HopfAlgebra/Basic.lean

@@ -19,6 +19,8 @@ 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.ofAlgHom` : construct a Hopf algebra structure from an algebra hom
+  `A →ₐ[R] Aᵐᵒᵖ` satisfying the antipode identities.
 
 ## Main results
 
@@ -229,3 +231,25 @@ instance toHopfAlgebra : HopfAlgebra R R where
 theorem antipode_eq_id : antipode R (A := R) = .id := rfl
 
 end CommSemiring
+
+namespace HopfAlgebra
+
+variable {R A : Type*} [CommSemiring R] [Semiring A] [Bialgebra R A]
+
+open Coalgebra MulOpposite
+
+/-- Upgrade a bialgebra to a Hopf algebra by specifying the antipode as an algebra map
+`A →ₐ[R] Aᵐᵒᵖ` with appropriate conditions. -/
+noncomputable abbrev ofAlgHom (antipode : A →ₐ[R] Aᵐᵒᵖ)
+    (mul_antipode_rTensor_comul :
+      LinearMap.mul' R A ∘ₗ ((opLinearEquiv R).symm.toLinearMap ∘ₗ
+        antipode.toLinearMap).rTensor A ∘ₗ comul = Algebra.linearMap R A ∘ₗ counit)
+    (mul_antipode_lTensor_comul :
+      LinearMap.mul' R A ∘ₗ ((opLinearEquiv R).symm.toLinearMap ∘ₗ
+        antipode.toLinearMap).lTensor A ∘ₗ comul = Algebra.linearMap R A ∘ₗ counit) :
+    HopfAlgebra R A where
+  antipode := (opLinearEquiv R).symm.toLinearMap ∘ₗ antipode.toLinearMap
+  mul_antipode_rTensor_comul := mul_antipode_rTensor_comul
+  mul_antipode_lTensor_comul := mul_antipode_lTensor_comul
+
+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