From 59f7aee8fce4435de65303dc849ba1a075ae4153 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Sun, 24 May 2026 15:41:02 -0700 Subject: [PATCH 01/16] feat(RingTheory/HopfAlgebra): construct from anti-algebra hom --- Mathlib/RingTheory/HopfAlgebra/Basic.lean | 24 +++++++++++++++++++ .../RingTheory/HopfAlgebra/TensorProduct.lean | 21 +--------------- 2 files changed, 25 insertions(+), 20 deletions(-) diff --git a/Mathlib/RingTheory/HopfAlgebra/Basic.lean b/Mathlib/RingTheory/HopfAlgebra/Basic.lean index 5358ec8038142a..77230bc1a47798 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Basic.lean +++ b/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 diff --git a/Mathlib/RingTheory/HopfAlgebra/TensorProduct.lean b/Mathlib/RingTheory/HopfAlgebra/TensorProduct.lean index 62706afae60a13..fd5f7fd303f390 100644 --- a/Mathlib/RingTheory/HopfAlgebra/TensorProduct.lean +++ b/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 From 68a3e9873604ace5be4be0514bea67d75500c92e Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Mon, 25 May 2026 00:18:12 -0700 Subject: [PATCH 02/16] Update Mathlib/RingTheory/HopfAlgebra/Basic.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Yaël Dillies --- Mathlib/RingTheory/HopfAlgebra/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/HopfAlgebra/Basic.lean b/Mathlib/RingTheory/HopfAlgebra/Basic.lean index 77230bc1a47798..b8ba488ff85214 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Basic.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Basic.lean @@ -240,7 +240,7 @@ 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ᵐᵒᵖ) +noncomputable abbrev ofAlgHomOp (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) From 47b4482da8f150cebbe43c53029f8d44ac2f5b03 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Mon, 25 May 2026 00:59:19 -0700 Subject: [PATCH 03/16] refactor(RingTheory/HopfAlgebra): keep commutative ofAlgHom --- Mathlib/RingTheory/HopfAlgebra/Basic.lean | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/HopfAlgebra/Basic.lean b/Mathlib/RingTheory/HopfAlgebra/Basic.lean index b8ba488ff85214..4948270346c415 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Basic.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Basic.lean @@ -19,8 +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.ofAlgHom` : construct a Hopf algebra structure from an algebra hom +* `HopfAlgebra.ofAlgHomOp` : construct a Hopf algebra structure from an algebra hom `A →ₐ[R] Aᵐᵒᵖ` satisfying the antipode identities. +* `HopfAlgebra.ofAlgHom` : the same for commutative `A`. ## Main results @@ -252,4 +253,19 @@ noncomputable abbrev ofAlgHomOp (antipode : A →ₐ[R] Aᵐᵒᵖ) mul_antipode_rTensor_comul := mul_antipode_rTensor_comul mul_antipode_lTensor_comul := mul_antipode_lTensor_comul +noncomputable abbrev ofAlgHom {A : Type*} [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 := + ofAlgHomOp (antipode.toOpposite fun _ _ ↦ .all _ _) + (by simpa [← Algebra.TensorProduct.lmul'_comp_map] + using congr(($mul_antipode_rTensor_comul).toLinearMap)) + (by simpa [← Algebra.TensorProduct.lmul'_comp_map] + using congr(($mul_antipode_lTensor_comul).toLinearMap)) + end HopfAlgebra From 5e62857db1e1f319027a693866004cd1f9ab691a Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Mon, 25 May 2026 05:42:54 -0700 Subject: [PATCH 04/16] docs(RingTheory/HopfAlgebra): add ofAlgHom docstring --- Mathlib/RingTheory/HopfAlgebra/Basic.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib/RingTheory/HopfAlgebra/Basic.lean b/Mathlib/RingTheory/HopfAlgebra/Basic.lean index 4948270346c415..f0a5a0af459709 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Basic.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Basic.lean @@ -253,6 +253,8 @@ noncomputable abbrev ofAlgHomOp (antipode : A →ₐ[R] Aᵐᵒᵖ) mul_antipode_rTensor_comul := mul_antipode_rTensor_comul mul_antipode_lTensor_comul := mul_antipode_lTensor_comul +/-- Upgrade a commutative bialgebra to a Hopf algebra by specifying the antipode `A →ₐ[R] A` +with appropriate conditions. -/ noncomputable abbrev ofAlgHom {A : Type*} [CommSemiring A] [Bialgebra R A] (antipode : A →ₐ[R] A) (mul_antipode_rTensor_comul : From 47429e14fdd6aa194aa2e952c640a5303b869fb7 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Mon, 25 May 2026 15:18:32 -0700 Subject: [PATCH 05/16] Apply suggestion from @eric-wieser Co-authored-by: Eric Wieser --- Mathlib/RingTheory/HopfAlgebra/Basic.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/HopfAlgebra/Basic.lean b/Mathlib/RingTheory/HopfAlgebra/Basic.lean index f0a5a0af459709..84eccd85875931 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Basic.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Basic.lean @@ -235,13 +235,14 @@ end CommSemiring namespace HopfAlgebra -variable {R A : Type*} [CommSemiring R] [Semiring A] [Bialgebra R A] +variable {R A : Type*} 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 ofAlgHomOp (antipode : A →ₐ[R] Aᵐᵒᵖ) +noncomputable abbrev ofAlgHomOp [CommSemiring R] [Semiring A] [Bialgebra R A] + (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) From 076d0e1e857a412411b95cc7629f0bde0deab9e0 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Mon, 25 May 2026 15:18:49 -0700 Subject: [PATCH 06/16] Update Mathlib/RingTheory/HopfAlgebra/Basic.lean Co-authored-by: Eric Wieser --- Mathlib/RingTheory/HopfAlgebra/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/HopfAlgebra/Basic.lean b/Mathlib/RingTheory/HopfAlgebra/Basic.lean index 84eccd85875931..e569649fb67a92 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Basic.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Basic.lean @@ -256,7 +256,7 @@ noncomputable abbrev ofAlgHomOp [CommSemiring R] [Semiring A] [Bialgebra R A] /-- Upgrade a commutative bialgebra to a Hopf algebra by specifying the antipode `A →ₐ[R] A` with appropriate conditions. -/ -noncomputable abbrev ofAlgHom {A : Type*} [CommSemiring A] [Bialgebra R A] +noncomputable abbrev ofAlgHom [CommSemiring A] [Bialgebra R A] (antipode : A →ₐ[R] A) (mul_antipode_rTensor_comul : ((Algebra.TensorProduct.lift antipode (.id R A) fun _ ↦ .all _).comp From 33e74574890ce6bb62b0cc3ba92228ac3a4ef54f Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Mon, 25 May 2026 15:27:31 -0700 Subject: [PATCH 07/16] Update Mathlib/RingTheory/HopfAlgebra/Basic.lean Co-authored-by: Eric Wieser --- Mathlib/RingTheory/HopfAlgebra/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/HopfAlgebra/Basic.lean b/Mathlib/RingTheory/HopfAlgebra/Basic.lean index e569649fb67a92..ee90df279a6f7e 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Basic.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Basic.lean @@ -256,7 +256,7 @@ noncomputable abbrev ofAlgHomOp [CommSemiring R] [Semiring A] [Bialgebra R A] /-- Upgrade a commutative bialgebra to a Hopf algebra by specifying the antipode `A →ₐ[R] A` with appropriate conditions. -/ -noncomputable abbrev ofAlgHom [CommSemiring A] [Bialgebra R A] +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 _ ↦ .all _).comp From 03e462bc594a20ae0e6d64aa01bede7d8353a572 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Mon, 25 May 2026 16:24:25 -0700 Subject: [PATCH 08/16] refactor(RingTheory/HopfAlgebra): replace ofAlgHomOp with ofConvInverse --- Mathlib/RingTheory/HopfAlgebra/Basic.lean | 43 ++++++++++++----------- 1 file changed, 23 insertions(+), 20 deletions(-) diff --git a/Mathlib/RingTheory/HopfAlgebra/Basic.lean b/Mathlib/RingTheory/HopfAlgebra/Basic.lean index ee90df279a6f7e..44e0f75e2310db 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Basic.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Basic.lean @@ -19,9 +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.ofAlgHomOp` : construct a Hopf algebra structure from an algebra hom - `A →ₐ[R] Aᵐᵒᵖ` satisfying the antipode identities. -* `HopfAlgebra.ofAlgHom` : the same for commutative `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 @@ -237,22 +237,23 @@ namespace HopfAlgebra variable {R A : Type*} -open Coalgebra MulOpposite +open Coalgebra WithConv LinearMap -/-- Upgrade a bialgebra to a Hopf algebra by specifying the antipode as an algebra map -`A →ₐ[R] Aᵐᵒᵖ` with appropriate conditions. -/ -noncomputable abbrev ofAlgHomOp [CommSemiring R] [Semiring A] [Bialgebra R A] - (antipode : A →ₐ[R] Aᵐᵒᵖ) +/-- 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) (mul_antipode_rTensor_comul : - LinearMap.mul' R A ∘ₗ ((opLinearEquiv R).symm.toLinearMap ∘ₗ - antipode.toLinearMap).rTensor A ∘ₗ comul = Algebra.linearMap R A ∘ₗ counit) + toConv antipode * toConv LinearMap.id = (1 : WithConv (A →ₗ[R] A))) (mul_antipode_lTensor_comul : - LinearMap.mul' R A ∘ₗ ((opLinearEquiv R).symm.toLinearMap ∘ₗ - antipode.toLinearMap).lTensor A ∘ₗ comul = Algebra.linearMap R A ∘ₗ counit) : + toConv LinearMap.id * toConv antipode = (1 : WithConv (A →ₗ[R] A))) : 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 + antipode := antipode + mul_antipode_rTensor_comul := by + simpa [convMul_def, convOne_def, ofConv_toConv, rTensor] + using congr(($mul_antipode_rTensor_comul).ofConv) + mul_antipode_lTensor_comul := by + simpa [convMul_def, convOne_def, ofConv_toConv, lTensor] + using congr(($mul_antipode_lTensor_comul).ofConv) /-- Upgrade a commutative bialgebra to a Hopf algebra by specifying the antipode `A →ₐ[R] A` with appropriate conditions. -/ @@ -265,10 +266,12 @@ noncomputable abbrev ofAlgHom [CommSemiring R] [CommSemiring A] [Bialgebra R A] (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 := - ofAlgHomOp (antipode.toOpposite fun _ _ ↦ .all _ _) - (by simpa [← Algebra.TensorProduct.lmul'_comp_map] - using congr(($mul_antipode_rTensor_comul).toLinearMap)) - (by simpa [← Algebra.TensorProduct.lmul'_comp_map] - using congr(($mul_antipode_lTensor_comul).toLinearMap)) + ofConvInverse antipode.toLinearMap + (WithConv.ext (by + simpa [← Algebra.TensorProduct.lmul'_comp_map, rTensor] + using congr(($mul_antipode_rTensor_comul).toLinearMap))) + (WithConv.ext (by + simpa [← Algebra.TensorProduct.lmul'_comp_map, lTensor] + using congr(($mul_antipode_lTensor_comul).toLinearMap))) end HopfAlgebra From 405f76efa5c8a88d6620c6dc64d96d29e99b0253 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Mon, 25 May 2026 17:09:18 -0700 Subject: [PATCH 09/16] refactor(RingTheory/HopfAlgebra): drop unused simp args in ofAlgHom --- Mathlib/RingTheory/HopfAlgebra/Basic.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/RingTheory/HopfAlgebra/Basic.lean b/Mathlib/RingTheory/HopfAlgebra/Basic.lean index 44e0f75e2310db..f6f7fed4c7b713 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Basic.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Basic.lean @@ -267,11 +267,11 @@ noncomputable abbrev ofAlgHom [CommSemiring R] [CommSemiring A] [Bialgebra R A] (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, rTensor] - using congr(($mul_antipode_rTensor_comul).toLinearMap))) - (WithConv.ext (by - simpa [← Algebra.TensorProduct.lmul'_comp_map, lTensor] - using congr(($mul_antipode_lTensor_comul).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 From 640a74a5774220fb2a53c99dd998120b78c8ee7e Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Wed, 27 May 2026 06:23:22 -0700 Subject: [PATCH 10/16] Update Mathlib/RingTheory/HopfAlgebra/Basic.lean Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/RingTheory/HopfAlgebra/Basic.lean | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/Mathlib/RingTheory/HopfAlgebra/Basic.lean b/Mathlib/RingTheory/HopfAlgebra/Basic.lean index f6f7fed4c7b713..513e605c54b731 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Basic.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Basic.lean @@ -248,12 +248,8 @@ noncomputable abbrev ofConvInverse [CommSemiring R] [Semiring A] [Bialgebra R A] toConv LinearMap.id * toConv antipode = (1 : WithConv (A →ₗ[R] A))) : HopfAlgebra R A where antipode := antipode - mul_antipode_rTensor_comul := by - simpa [convMul_def, convOne_def, ofConv_toConv, rTensor] - using congr(($mul_antipode_rTensor_comul).ofConv) - mul_antipode_lTensor_comul := by - simpa [convMul_def, convOne_def, ofConv_toConv, lTensor] - using congr(($mul_antipode_lTensor_comul).ofConv) + mul_antipode_rTensor_comul := by simpa using congr(($mul_antipode_rTensor_comul).ofConv) + mul_antipode_lTensor_comul := by simpa using congr(($mul_antipode_lTensor_comul).ofConv) /-- Upgrade a commutative bialgebra to a Hopf algebra by specifying the antipode `A →ₐ[R] A` with appropriate conditions. -/ From db77934641982ffc5ca8a8ab085ae3222e287c76 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Wed, 27 May 2026 06:23:38 -0700 Subject: [PATCH 11/16] Update Mathlib/RingTheory/HopfAlgebra/Basic.lean Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/RingTheory/HopfAlgebra/Basic.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Mathlib/RingTheory/HopfAlgebra/Basic.lean b/Mathlib/RingTheory/HopfAlgebra/Basic.lean index 513e605c54b731..d7c95fd66ce606 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Basic.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Basic.lean @@ -242,10 +242,8 @@ 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) - (mul_antipode_rTensor_comul : - toConv antipode * toConv LinearMap.id = (1 : WithConv (A →ₗ[R] A))) - (mul_antipode_lTensor_comul : - toConv LinearMap.id * toConv antipode = (1 : WithConv (A →ₗ[R] A))) : + (mul_antipode_rTensor_comul : toConv antipode * toConv LinearMap.id = 1) + (mul_antipode_lTensor_comul : toConv LinearMap.id * toConv antipode = 1) : HopfAlgebra R A where antipode := antipode mul_antipode_rTensor_comul := by simpa using congr(($mul_antipode_rTensor_comul).ofConv) From 8b5640fe3c9fdabcf0ff50b844ac63d81ff76c0f Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Wed, 27 May 2026 20:39:59 -0700 Subject: [PATCH 12/16] refactor(RingTheory/HopfAlgebra): rename lTensor antipode arguments --- Mathlib/RingTheory/HopfAlgebra/Basic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/RingTheory/HopfAlgebra/Basic.lean b/Mathlib/RingTheory/HopfAlgebra/Basic.lean index d7c95fd66ce606..ed675ac3dfe07f 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Basic.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Basic.lean @@ -243,11 +243,11 @@ open Coalgebra WithConv LinearMap noncomputable abbrev ofConvInverse [CommSemiring R] [Semiring A] [Bialgebra R A] (antipode : A →ₗ[R] A) (mul_antipode_rTensor_comul : toConv antipode * toConv LinearMap.id = 1) - (mul_antipode_lTensor_comul : toConv LinearMap.id * toConv antipode = 1) : + (mul_lTensor_antipode_comul : toConv LinearMap.id * toConv antipode = 1) : HopfAlgebra R A where antipode := antipode mul_antipode_rTensor_comul := by simpa using congr(($mul_antipode_rTensor_comul).ofConv) - mul_antipode_lTensor_comul := by simpa using congr(($mul_antipode_lTensor_comul).ofConv) + mul_antipode_lTensor_comul := by simpa using congr(($mul_lTensor_antipode_comul).ofConv) /-- Upgrade a commutative bialgebra to a Hopf algebra by specifying the antipode `A →ₐ[R] A` with appropriate conditions. -/ @@ -256,7 +256,7 @@ noncomputable abbrev ofAlgHom [CommSemiring R] [CommSemiring A] [Bialgebra 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 : + (mul_lTensor_antipode_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 := @@ -266,6 +266,6 @@ noncomputable abbrev ofAlgHom [CommSemiring R] [CommSemiring A] [Bialgebra R A] using congr(($mul_antipode_rTensor_comul).toLinearMap)) (WithConv.ext <| by simpa [← Algebra.TensorProduct.lmul'_comp_map] - using congr(($mul_antipode_lTensor_comul).toLinearMap)) + using congr(($mul_lTensor_antipode_comul).toLinearMap)) end HopfAlgebra From cb82f33516fb20377975ab7bc4d502b72ca3fe36 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Wed, 27 May 2026 21:33:09 -0700 Subject: [PATCH 13/16] refactor(RingTheory/HopfAlgebra): spell out Commute.all in ofAlgHom --- Mathlib/RingTheory/HopfAlgebra/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/HopfAlgebra/Basic.lean b/Mathlib/RingTheory/HopfAlgebra/Basic.lean index ed675ac3dfe07f..9d37470e4e88ab 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Basic.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Basic.lean @@ -254,10 +254,10 @@ 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 _ ↦ .all _).comp + ((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_lTensor_antipode_comul : - (Algebra.TensorProduct.lift (.id R A) antipode fun _ _ ↦ .all _ _).comp + (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 From 70fcb19175a654c2998646767d8d62d1db33ae8e Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Mon, 1 Jun 2026 05:51:42 -0700 Subject: [PATCH 14/16] refactor(RingTheory/HopfAlgebra): rename ofConvInverse hypotheses --- Mathlib/RingTheory/HopfAlgebra/Basic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/RingTheory/HopfAlgebra/Basic.lean b/Mathlib/RingTheory/HopfAlgebra/Basic.lean index 9d37470e4e88ab..bcc8ca6890710f 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Basic.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Basic.lean @@ -242,12 +242,12 @@ 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) - (mul_antipode_rTensor_comul : toConv antipode * toConv LinearMap.id = 1) - (mul_lTensor_antipode_comul : toConv LinearMap.id * toConv antipode = 1) : + (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(($mul_antipode_rTensor_comul).ofConv) - mul_antipode_lTensor_comul := by simpa using congr(($mul_lTensor_antipode_comul).ofConv) + 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. -/ From 597adf8aa9119bb3233e2dfbd22a89ec5844a472 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Mon, 1 Jun 2026 14:51:04 -0700 Subject: [PATCH 15/16] refactor(RingTheory/HopfAlgebra): restore ofAlgHom hypothesis name symmetry --- Mathlib/RingTheory/HopfAlgebra/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/HopfAlgebra/Basic.lean b/Mathlib/RingTheory/HopfAlgebra/Basic.lean index bcc8ca6890710f..9080d6e86e57fe 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Basic.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Basic.lean @@ -256,7 +256,7 @@ noncomputable abbrev ofAlgHom [CommSemiring R] [CommSemiring A] [Bialgebra 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_lTensor_antipode_comul : + (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 := @@ -266,6 +266,6 @@ noncomputable abbrev ofAlgHom [CommSemiring R] [CommSemiring A] [Bialgebra R A] using congr(($mul_antipode_rTensor_comul).toLinearMap)) (WithConv.ext <| by simpa [← Algebra.TensorProduct.lmul'_comp_map] - using congr(($mul_lTensor_antipode_comul).toLinearMap)) + using congr(($mul_antipode_lTensor_comul).toLinearMap)) end HopfAlgebra From bd33e0a4c95324751182beaf64b7d5528209d690 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Mon, 1 Jun 2026 17:09:55 -0700 Subject: [PATCH 16/16] fix(RingTheory/HopfAlgebra): use `simpa using!` for non-reducible defeq --- Mathlib/RingTheory/HopfAlgebra/Basic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/RingTheory/HopfAlgebra/Basic.lean b/Mathlib/RingTheory/HopfAlgebra/Basic.lean index 9080d6e86e57fe..c773f198fa6dc6 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Basic.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Basic.lean @@ -246,8 +246,8 @@ noncomputable abbrev ofConvInverse [CommSemiring R] [Semiring A] [Bialgebra R A] (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) + 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. -/ @@ -263,9 +263,9 @@ noncomputable abbrev ofAlgHom [CommSemiring R] [CommSemiring A] [Bialgebra R A] ofConvInverse antipode.toLinearMap (WithConv.ext <| by simpa [← Algebra.TensorProduct.lmul'_comp_map] - using congr(($mul_antipode_rTensor_comul).toLinearMap)) + using! congr(($mul_antipode_rTensor_comul).toLinearMap)) (WithConv.ext <| by simpa [← Algebra.TensorProduct.lmul'_comp_map] - using congr(($mul_antipode_lTensor_comul).toLinearMap)) + using! congr(($mul_antipode_lTensor_comul).toLinearMap)) end HopfAlgebra