feat(RingTheory): hopf algebra definition (#10079)

Add definition of a Hopf algebra. For FLT.



Co-authored-by: al-ramsey <s2158261@ed.ac.uk>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib.lean

@@ -3227,6 +3227,7 @@ import Mathlib.RingTheory.HahnSeries.Multiplication
 import Mathlib.RingTheory.HahnSeries.PowerSeries
 import Mathlib.RingTheory.HahnSeries.Summable
 import Mathlib.RingTheory.Henselian
+import Mathlib.RingTheory.HopfAlgebra
 import Mathlib.RingTheory.Ideal.AssociatedPrime
 import Mathlib.RingTheory.Ideal.Basic
 import Mathlib.RingTheory.Ideal.Cotangent

Mathlib/RingTheory/HopfAlgebra.lean

@@ -0,0 +1,92 @@
+/-
+Copyright (c) 2024 Ali Ramsey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ali Ramsey
+-/
+import Mathlib.RingTheory.Bialgebra
+
+/-!
+# Hopf algebras
+
+In this file we define `HopfAlgebra`, and provide instances for:
+
+* Commutative semirings: `CommSemiring.toHopfAlgebra`
+
+# Main definitions
+
+* `HopfAlgebra R A` : the Hopf algebra structure on an `R`-bialgebra `A`.
+* `HopfAlgebra.antipode` : The `R`-linear map `A →ₗ[R] A`.
+
+## TODO
+
+* Uniqueness of Hopf algebra structure on a bialgebra (i.e. if the algebra and coalgebra structures
+agree then the antipodes must also agree).
+
+* `antipode 1 = 1` and `antipode (a * b) = antipode b * antipode a`, so in particular if `A` is
+  commutative then `antipode` is an algebra homomorphism.
+
+* If `A` is commutative then `antipode` is necessarily a bijection and its square is
+  the identity.
+
+## References
+
+* <https://en.wikipedia.org/wiki/Hopf_algebra>
+
+* [C. Kassel, *Quantum Groups* (§III.3)][Kassel1995]
+
+
+-/
+
+suppress_compilation
+
+universe u v
+
+/-- A Hopf algebra over a commutative (semi)ring `R` is a bialgebra over `R` equipped with an
+`R`-linear endomorphism `antipode` satisfying the antipode axioms. -/
+class HopfAlgebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] extends
+    Bialgebra R A where
+  /-- The antipode of the Hopf algebra. -/
+  antipode : A →ₗ[R] A
+  /-- One of the antipode axioms for a Hopf algebra. -/
+  mul_antipode_rTensor_comul :
+    LinearMap.mul' R A ∘ₗ antipode.rTensor A ∘ₗ comul = (Algebra.linearMap R A) ∘ₗ counit
+  /-- One of the antipode axioms for a Hopf algebra. -/
+  mul_antipode_lTensor_comul :
+    LinearMap.mul' R A ∘ₗ antipode.lTensor A ∘ₗ comul = (Algebra.linearMap R A) ∘ₗ counit
+
+namespace HopfAlgebra
+
+variable {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [HopfAlgebra R A]
+
+@[simp]
+theorem mul_antipode_rTensor_comul_apply (a : A) :
+    LinearMap.mul' R A (antipode.rTensor A (Coalgebra.comul a)) =
+    algebraMap R A (Coalgebra.counit a) :=
+  LinearMap.congr_fun mul_antipode_rTensor_comul a
+
+@[simp]
+theorem mul_antipode_lTensor_comul_apply (a : A) :
+    LinearMap.mul' R A (antipode.lTensor A (Coalgebra.comul a)) =
+    algebraMap R A (Coalgebra.counit a) :=
+  LinearMap.congr_fun mul_antipode_lTensor_comul a
+
+end HopfAlgebra
+
+section CommSemiring
+
+variable (R : Type u) [CommSemiring R]
+
+open HopfAlgebra
+
+namespace CommSemiring
+
+/-- Every commutative (semi)ring is a Hopf algebra over itself -/
+instance toHopfAlgebra : HopfAlgebra R R where
+  antipode := .id
+  mul_antipode_rTensor_comul := by ext; simp
+  mul_antipode_lTensor_comul := by ext; simp
+
+@[simp]
+theorem antipode_eq_id : antipode (R := R) (A := R) = .id := rfl
+
+end CommSemiring

Mathlib/RingTheory/TensorProduct.lean

@@ -32,7 +32,7 @@ multiplication is characterized by `(a₁ ⊗ₜ b₁) * (a₂ ⊗ₜ b₂) = (a
 
 ## References
 
-* [C. Kassel, *Quantum Groups* (§II.4)][kasselTensorProducts1995]
+* [C. Kassel, *Quantum Groups* (§II.4)][Kassel1995]
 
 -/
 

docs/references.bib

@@ -1825,19 +1825,20 @@ @Book{            Kashiwara2006
   title         = {Categories and Sheaves}
 }
 
-@InBook{          kasselTensorProducts1995,
-  title         = {Tensor {{Products}}},
-  booktitle     = {Quantum {{Groups}}},
+@Book{            Kassel1995,
   author        = {Kassel, Christian},
-  year          = {1995},
+  title         = {Quantum groups},
+  series        = {Graduate Texts in Mathematics},
   volume        = {155},
-  pages         = {23--38},
-  publisher     = {{Springer New York}},
-  address       = {{New York, NY}},
-  doi           = {10.1007/978-1-4612-0783-2_2},
-  urldate       = {2023-09-28},
-  collaborator  = {Kassel, Christian},
-  isbn          = {978-1-4612-6900-7 978-1-4612-0783-2}
+  publisher     = {Springer-Verlag, New York},
+  year          = {1995},
+  pages         = {xii+531},
+  isbn          = {0-387-94370-6},
+  mrclass       = {17B37 (16W30 18D10 20F36 57M25 81R50)},
+  mrnumber      = {1321145},
+  mrreviewer    = {Yu.\ N.\ Bespalov},
+  doi           = {10.1007/978-1-4612-0783-2},
+  url           = {https://doi.org/10.1007/978-1-4612-0783-2}
 }
 
 @Book{            katz_mazur,