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

Generalize `ofAlgHom` to take `A →ₐ[R] Aᵐᵒᵖ` (non-commutative case
via the opposite ring), and add `rTensor/lTensorAntipodeEqualizer`
subalgebras + `mul_*_comul_eq_of_mem_adjoin` corollaries that let
consumers verify the antipode axiom on a generating set
(Takeuchi 1971, Lemma 1).

Motivates leanprover-community#31898: the TensorAlgebra Hopf instance reduces from a
~100-line Sweedler proof to a ~16-line application of the new API.

Author: hawkrobe

Mathlib/RingTheory/HopfAlgebra/Basic.lean

@@ -19,11 +19,18 @@ 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.
+* `HopfAlgebra.rTensorAntipodeEqualizer`, `HopfAlgebra.lTensorAntipodeEqualizer` : the
+  subalgebras of `A` on which a candidate antipode satisfies the antipode identity.
 
 ## Main results
 
 * `HopfAlgebra.antipode_one` : the antipode of the unit is the unit.
 * `HopfAlgebra.antipode_mul` : the antipode is an antihomomorphism: `S(ab) = S(b)S(a)`.
+* `HopfAlgebra.mul_rTensor_comul_eq_of_mem_adjoin`,
+  `HopfAlgebra.mul_lTensor_comul_eq_of_mem_adjoin` : the antipode identity propagates
+  from a generating set of `A` to all of `Algebra.adjoin R s`.
 
 ## TODO
 
@@ -229,3 +236,136 @@ 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
+
+/-- The subalgebra of `a : A` where the `rTensor` antipode identity holds for a candidate
+anti-algebra hom `S : A →ₐ[R] Aᵐᵒᵖ`. Following Takeuchi (1971), Lemma 1, this set is closed
+under the algebra operations on `A`, with the multiplicative closure step being the
+Sweedler `comul_mul` calculation using anti-multiplicativity of `S`. -/
+noncomputable def rTensorAntipodeEqualizer (S : A →ₐ[R] Aᵐᵒᵖ) : Subalgebra R A where
+  carrier := {a | LinearMap.mul' R A
+    (((opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap).rTensor A (comul a))
+    = algebraMap R A (counit (R := R) a)}
+  add_mem' {x y} (hx : _ = _) (hy : _ = _) := by simp [map_add, hx, hy]
+  mul_mem' {x y} (hx : _ = _) (hy : _ = _) := by
+    set Ŝ : A →ₗ[R] A := (opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap
+    have antihom : ∀ a b : A, Ŝ (a * b) = Ŝ b * Ŝ a := fun a b => by simp [Ŝ]
+    let ℛx := ℛ R x
+    let ℛy := ℛ R y
+    have hx' : ∑ i ∈ ℛx.index, Ŝ (ℛx.left i) * ℛx.right i = algebraMap R A (counit x) := by
+      simpa [← ℛx.eq, map_sum, LinearMap.rTensor_tmul, LinearMap.mul'_apply] using hx
+    have hy' : ∑ j ∈ ℛy.index, Ŝ (ℛy.left j) * ℛy.right j = algebraMap R A (counit y) := by
+      simpa [← ℛy.eq, map_sum, LinearMap.rTensor_tmul, LinearMap.mul'_apply] using hy
+    change LinearMap.mul' R A _ = _
+    rw [Bialgebra.comul_mul]
+    conv_lhs => rw [← ℛx.eq, ← ℛy.eq]
+    simp only [Finset.sum_mul, Finset.mul_sum, Algebra.TensorProduct.tmul_mul_tmul,
+      map_sum, LinearMap.rTensor_tmul, LinearMap.mul'_apply, antihom]
+    calc ∑ j ∈ ℛy.index, ∑ i ∈ ℛx.index,
+          Ŝ (ℛy.left j) * Ŝ (ℛx.left i) * (ℛx.right i * ℛy.right j)
+        = ∑ j ∈ ℛy.index,
+            Ŝ (ℛy.left j) * (∑ i ∈ ℛx.index, Ŝ (ℛx.left i) * ℛx.right i) * ℛy.right j := by
+          simp [mul_assoc, Finset.sum_mul, Finset.mul_sum]
+      _ = ∑ j ∈ ℛy.index,
+            algebraMap R A (counit x) * (Ŝ (ℛy.left j) * ℛy.right j) := by
+          simp [hx', ← Algebra.commutes, mul_assoc]
+      _ = algebraMap R A (counit (x * y)) := by
+          rw [← Finset.mul_sum, hy', ← map_mul, ← Bialgebra.counit_mul]
+  algebraMap_mem' r := by simp
+
+@[simp]
+theorem mem_rTensorAntipodeEqualizer (S : A →ₐ[R] Aᵐᵒᵖ) (a : A) :
+    a ∈ rTensorAntipodeEqualizer S ↔
+      LinearMap.mul' R A
+          (((opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap).rTensor A (comul a))
+        = algebraMap R A (counit (R := R) a) :=
+  Iff.rfl
+
+/-- The subalgebra of `a : A` where the `lTensor` antipode identity holds for a candidate
+anti-algebra hom `S : A →ₐ[R] Aᵐᵒᵖ`. The mirror image of `rTensorAntipodeEqualizer`. -/
+noncomputable def lTensorAntipodeEqualizer (S : A →ₐ[R] Aᵐᵒᵖ) : Subalgebra R A where
+  carrier := {a | LinearMap.mul' R A
+    (((opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap).lTensor A (comul a))
+    = algebraMap R A (counit (R := R) a)}
+  add_mem' {x y} (hx : _ = _) (hy : _ = _) := by simp [map_add, hx, hy]
+  mul_mem' {x y} (hx : _ = _) (hy : _ = _) := by
+    set Ŝ : A →ₗ[R] A := (opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap
+    have antihom : ∀ a b : A, Ŝ (a * b) = Ŝ b * Ŝ a := fun a b => by simp [Ŝ]
+    let ℛx := ℛ R x
+    let ℛy := ℛ R y
+    have hx' : ∑ i ∈ ℛx.index, ℛx.left i * Ŝ (ℛx.right i) = algebraMap R A (counit x) := by
+      simpa [← ℛx.eq, map_sum, LinearMap.lTensor_tmul, LinearMap.mul'_apply] using hx
+    have hy' : ∑ j ∈ ℛy.index, ℛy.left j * Ŝ (ℛy.right j) = algebraMap R A (counit y) := by
+      simpa [← ℛy.eq, map_sum, LinearMap.lTensor_tmul, LinearMap.mul'_apply] using hy
+    change LinearMap.mul' R A _ = _
+    rw [Bialgebra.comul_mul]
+    conv_lhs => rw [← ℛx.eq, ← ℛy.eq]
+    simp only [Finset.sum_mul, Finset.mul_sum, Algebra.TensorProduct.tmul_mul_tmul,
+      map_sum, LinearMap.lTensor_tmul, LinearMap.mul'_apply, antihom]
+    rw [Finset.sum_comm]
+    calc ∑ i ∈ ℛx.index, ∑ j ∈ ℛy.index,
+          (ℛx.left i * ℛy.left j) * (Ŝ (ℛy.right j) * Ŝ (ℛx.right i))
+        = ∑ i ∈ ℛx.index,
+            ℛx.left i * (∑ j ∈ ℛy.index, ℛy.left j * Ŝ (ℛy.right j)) * Ŝ (ℛx.right i) := by
+          simp [mul_assoc, Finset.sum_mul, Finset.mul_sum]
+      _ = ∑ i ∈ ℛx.index,
+            algebraMap R A (counit y) * (ℛx.left i * Ŝ (ℛx.right i)) := by
+          simp [hy', ← Algebra.commutes, mul_assoc]
+      _ = algebraMap R A (counit (x * y)) := by
+          rw [← Finset.mul_sum, hx', ← map_mul, mul_comm, ← Bialgebra.counit_mul]
+  algebraMap_mem' r := by simp
+
+@[simp]
+theorem mem_lTensorAntipodeEqualizer (S : A →ₐ[R] Aᵐᵒᵖ) (a : A) :
+    a ∈ lTensorAntipodeEqualizer S ↔
+      LinearMap.mul' R A
+          (((opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap).lTensor A (comul a))
+        = algebraMap R A (counit (R := R) a) :=
+  Iff.rfl
+
+/-- If `S : A →ₐ[R] Aᵐᵒᵖ` satisfies the `rTensor` antipode identity on a generating set
+`s`, then it satisfies it on the whole algebra generated by `s`. -/
+theorem mul_rTensor_comul_eq_of_mem_adjoin
+    (S : A →ₐ[R] Aᵐᵒᵖ) {s : Set A}
+    (h : ∀ ⦃x⦄, x ∈ s → LinearMap.mul' R A
+            (((opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap).rTensor A (comul x))
+          = algebraMap R A (counit (R := R) x))
+    {x : A} (hx : x ∈ Algebra.adjoin R s) :
+    LinearMap.mul' R A
+        (((opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap).rTensor A (comul x))
+      = algebraMap R A (counit (R := R) x) :=
+  Algebra.adjoin_le (S := rTensorAntipodeEqualizer S) h hx
+
+/-- If `S : A →ₐ[R] Aᵐᵒᵖ` satisfies the `lTensor` antipode identity on a generating set
+`s`, then it satisfies it on the whole algebra generated by `s`. -/
+theorem mul_lTensor_comul_eq_of_mem_adjoin
+    (S : A →ₐ[R] Aᵐᵒᵖ) {s : Set A}
+    (h : ∀ ⦃x⦄, x ∈ s → LinearMap.mul' R A
+            (((opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap).lTensor A (comul x))
+          = algebraMap R A (counit (R := R) x))
+    {x : A} (hx : x ∈ Algebra.adjoin R s) :
+    LinearMap.mul' R A
+        (((opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap).lTensor A (comul x))
+      = algebraMap R A (counit (R := R) x) :=
+  Algebra.adjoin_le (S := lTensorAntipodeEqualizer S) h hx
+
+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