feat(RingTheory/HopfAlgebra): primitive-generated construction toolkit

hawkrobe · hawkrobe · commit 62d838a2514b · 2026-05-25T09:43:34.000-07:00
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -6346,6 +6346,7 @@ public import Mathlib.RingTheory.Bialgebra.Equiv
 public import Mathlib.RingTheory.Bialgebra.GroupLike
 public import Mathlib.RingTheory.Bialgebra.Hom
 public import Mathlib.RingTheory.Bialgebra.MonoidAlgebra
+public import Mathlib.RingTheory.Bialgebra.Primitive
 public import Mathlib.RingTheory.Bialgebra.TensorProduct
 public import Mathlib.RingTheory.Binomial
 public import Mathlib.RingTheory.ChainOfDivisors
@@ -6354,6 +6355,7 @@ public import Mathlib.RingTheory.Coalgebra.Basic
 public import Mathlib.RingTheory.Coalgebra.CoassocSimps
 public import Mathlib.RingTheory.Coalgebra.Convolution
 public import Mathlib.RingTheory.Coalgebra.Equiv
+public import Mathlib.RingTheory.Coalgebra.Graded
 public import Mathlib.RingTheory.Coalgebra.GroupLike
 public import Mathlib.RingTheory.Coalgebra.Hom
 public import Mathlib.RingTheory.Coalgebra.MonoidAlgebra
@@ -6498,6 +6500,7 @@ public import Mathlib.RingTheory.Henselian
 public import Mathlib.RingTheory.HopfAlgebra.Basic
 public import Mathlib.RingTheory.HopfAlgebra.GroupLike
 public import Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
+public import Mathlib.RingTheory.HopfAlgebra.Primitive
 public import Mathlib.RingTheory.HopfAlgebra.TensorProduct
 public import Mathlib.RingTheory.HopkinsLevitzki
 public import Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
diff --git a/Mathlib/RingTheory/Bialgebra/Primitive.lean b/Mathlib/RingTheory/Bialgebra/Primitive.lean
@@ -0,0 +1,87 @@
+/-
+Copyright (c) 2026 Robert Hawkins. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robert Hawkins
+-/
+module
+
+public import Mathlib.RingTheory.Bialgebra.Basic
+
+/-!
+# Primitive elements in a bialgebra
+
+This file defines primitive elements in a bialgebra, i.e. elements `a` such that
+`Δ a = a ⊗ 1 + 1 ⊗ a` and `ε a = 0`.
+
+## Main declarations
+
+* `IsPrimitiveElem`: Predicate for an element in a bialgebra to be primitive.
+* `primitiveSubmodule`: The submodule of primitive elements.
+-/
+
+@[expose] public section
+
+open Coalgebra Bialgebra TensorProduct
+
+variable {R A : Type*}
+
+section Semiring
+variable [CommSemiring R] [Semiring A] [Bialgebra R A] {a b : A}
+
+variable (R) in
+/-- An element `a` of a bialgebra is *primitive* if `Δ a = a ⊗ 1 + 1 ⊗ a` and `ε a = 0`. -/
+@[mk_iff]
+structure IsPrimitiveElem (a : A) : Prop where
+  /-- A primitive element `a` satisfies `Δ a = a ⊗ 1 + 1 ⊗ a`. -/
+  comul_eq_tmul_one_add_one_tmul : comul a = a ⊗ₜ[R] 1 + 1 ⊗ₜ[R] a
+  /-- A primitive element `a` satisfies `ε a = 0`. -/
+  counit_eq_zero : counit (R := R) a = 0
+
+attribute [simp] IsPrimitiveElem.counit_eq_zero
+
+@[simp] lemma IsPrimitiveElem.zero : IsPrimitiveElem R (0 : A) where
+  comul_eq_tmul_one_add_one_tmul := by
+    simp only [map_zero, zero_tmul, tmul_zero, add_zero]
+  counit_eq_zero := map_zero _
+
+lemma IsPrimitiveElem.add (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) :
+    IsPrimitiveElem R (a + b) where
+  comul_eq_tmul_one_add_one_tmul := by
+    rw [map_add, ha.comul_eq_tmul_one_add_one_tmul, hb.comul_eq_tmul_one_add_one_tmul,
+      add_tmul, tmul_add]; abel
+  counit_eq_zero := by rw [map_add, ha.counit_eq_zero, hb.counit_eq_zero, add_zero]
+
+lemma IsPrimitiveElem.smul (ha : IsPrimitiveElem R a) (r : R) :
+    IsPrimitiveElem R (r • a) where
+  comul_eq_tmul_one_add_one_tmul := by
+    have h1 : r • (a ⊗ₜ[R] (1 : A)) = (r • a) ⊗ₜ[R] (1 : A) := smul_tmul' r a 1
+    have h2 : r • ((1 : A) ⊗ₜ[R] a) = (1 : A) ⊗ₜ[R] (r • a) := (tmul_smul r 1 a).symm
+    rw [LinearMap.map_smul, ha.comul_eq_tmul_one_add_one_tmul, smul_add, h1, h2]
+  counit_eq_zero := by rw [LinearMap.map_smul, ha.counit_eq_zero, smul_zero]
+
+variable (R A) in
+/-- The primitive elements form a submodule. -/
+def primitiveSubmodule : Submodule R A where
+  carrier := {a | IsPrimitiveElem R a}
+  add_mem' := IsPrimitiveElem.add
+  zero_mem' := .zero
+  smul_mem' r _ ha := ha.smul r
+
+@[simp] lemma mem_primitiveSubmodule {a : A} :
+    a ∈ primitiveSubmodule R A ↔ IsPrimitiveElem R a := Iff.rfl
+
+end Semiring
+
+section Ring
+variable [CommRing R] [Ring A] [Bialgebra R A] {a : A}
+
+lemma IsPrimitiveElem.neg (ha : IsPrimitiveElem R a) : IsPrimitiveElem R (-a) where
+  comul_eq_tmul_one_add_one_tmul := by
+    rw [map_neg, ha.comul_eq_tmul_one_add_one_tmul, neg_add, neg_tmul, tmul_neg]
+  counit_eq_zero := by rw [map_neg, ha.counit_eq_zero, neg_zero]
+
+lemma IsPrimitiveElem.sub (ha : IsPrimitiveElem R a) {b : A} (hb : IsPrimitiveElem R b) :
+    IsPrimitiveElem R (a - b) := by
+  rw [sub_eq_add_neg]; exact ha.add hb.neg
+
+end Ring
diff --git a/Mathlib/RingTheory/Coalgebra/Graded.lean b/Mathlib/RingTheory/Coalgebra/Graded.lean
@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2026 Robert Hawkins. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robert Hawkins
+-/
+module
+
+public import Mathlib.RingTheory.Coalgebra.Basic
+public import Mathlib.RingTheory.GradedAlgebra.Basic
+
+/-!
+# Graded coalgebras
+
+A coalgebra `A` over `R` is *graded* by a family of submodules `𝒜 : ι → Submodule R A`,
+forming a direct-sum decomposition, if the comultiplication respects the grading:
+`Δ(𝒜 n) ⊆ ⨆_{p+q=n} 𝒜 p ⊗ 𝒜 q`.
+
+## Main declarations
+
+* `GradedCoalgebra`: Predicate for a coalgebra to be graded.
+
+## Implementation notes
+
+The condition is stated as membership in an `iSup` of submodules rather than via a direct-sum
+decomposition of `A ⊗ A`, because the latter would require constructing an `ι × ι`-graded
+decomposition of `A ⊗[R] A` (or factoring through the diagonal `p + q = n`-graded version).
+The `iSup` form is what consumers typically unpack via `Submodule.mem_iSup_iff_exists_dfinsupp`.
+
+This file introduces the typeclass ahead of its main downstream consumer, a graded-connected
+antipode existence theorem `HopfAlgebra.ofGradedConnected`. The standard examples
+(`TensorAlgebra`, `FreeAlgebra`, `SymmetricAlgebra`, `ExteriorAlgebra`) are all graded coalgebras
+by `ℕ`.
+
+## TODO
+
+* Provide instances on `TensorAlgebra` and other free constructions.
+* `HopfAlgebra.ofGradedConnected` — given `[GradedCoalgebra 𝒜]` together with a connectedness
+  condition `𝒜 0 = R · 1`, construct the antipode recursively on degree.
+-/
+
+@[expose] public section
+
+open Coalgebra TensorProduct DirectSum
+
+variable {R A ι : Type*} [CommSemiring R]
+  [AddCommMonoid A] [Module R A] [Coalgebra R A]
+  [DecidableEq ι] [AddMonoid ι]
+
+/-- A coalgebra is *graded* by `𝒜 : ι → Submodule R A` if the comultiplication respects
+the grading: `Δ(𝒜 n) ⊆ ⨆_{p+q=n} 𝒜 p ⊗ 𝒜 q`. -/
+class GradedCoalgebra (𝒜 : ι → Submodule R A) [DirectSum.Decomposition 𝒜] : Prop where
+  /-- The comultiplication takes degree-`n` elements to the sum of `𝒜 p ⊗ 𝒜 q` over `p + q = n`. -/
+  comul_mem : ∀ {n : ι} {x : A}, x ∈ 𝒜 n →
+    Coalgebra.comul (R := R) x ∈
+      ⨆ p : ι, ⨆ q : ι, ⨆ (_ : p + q = n),
+        LinearMap.range (TensorProduct.map (𝒜 p).subtype (𝒜 q).subtype)
diff --git a/Mathlib/RingTheory/HopfAlgebra/Basic.lean b/Mathlib/RingTheory/HopfAlgebra/Basic.lean
@@ -19,17 +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.
 
 ## 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.antipode_unique` : the antipode is uniquely determined by the underlying bialgebra
+  structure.
 
 ## TODO
 
-* Uniqueness of Hopf algebra structure on a bialgebra (i.e. if the algebra and coalgebra structures
-  agree then the antipodes must also agree).
-
 * If `A` is commutative then `antipode` is an algebra homomorphism.
 
 * If `A` is commutative then `antipode` is necessarily a bijection and its square is
@@ -38,6 +39,8 @@ In this file we define `HopfAlgebra`, and provide instances for:
 (Note that all three facts have been proved for Hopf bimonoids in an arbitrary braided category,
 so we could deduce the facts here from an equivalence `HopfAlgCat R ≌ Hopf (ModuleCat R)`.)
 
+* A graded connected bialgebra admits a unique antipode.
+
 ## References
 
 * <https://en.wikipedia.org/wiki/Hopf_algebra>
@@ -75,6 +78,26 @@ namespace HopfAlgebra
 
 export HopfAlgebraStruct (antipode)
 
+section Bialgebra
+variable {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Bialgebra R A]
+
+open Coalgebra WithConv
+
+/-! ### Uniqueness of the antipode -/
+
+/-- If `S₁` and `S₂` are left and right convolution inverses of the identity, then `S₁ = S₂`. -/
+theorem antipode_unique {S₁ S₂ : A →ₗ[R] A}
+    (h₁ : LinearMap.mul' R A ∘ₗ S₁.rTensor A ∘ₗ comul = Algebra.linearMap R A ∘ₗ counit)
+    (h₂ : LinearMap.mul' R A ∘ₗ S₂.lTensor A ∘ₗ comul = Algebra.linearMap R A ∘ₗ counit) :
+    S₁ = S₂ := by
+  refine toConv_injective <| left_inv_eq_right_inv
+    (a := toConv LinearMap.id) (b := toConv S₁) (c := toConv S₂) ?_ ?_
+  · exact WithConv.ext h₁
+  · exact WithConv.ext h₂
+
+end Bialgebra
+
+section Semiring
 variable {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [HopfAlgebra R A] {a : A}
 
 @[simp]
@@ -211,6 +234,44 @@ theorem antipode_mul (a b : A) :
       _ = (counit (R := R) y • counit x) • (1 : A) := by
         simp only [smul_eq_mul, mul_comm (counit y)]
 
+/-! ### Antipode as unique convolution inverse -/
+
+/-- The antipode is the unique left convolution inverse of the identity. -/
+theorem eq_antipode_of_mul_rTensor_comul {S : A →ₗ[R] A}
+    (h : LinearMap.mul' R A ∘ₗ S.rTensor A ∘ₗ comul = Algebra.linearMap R A ∘ₗ counit) :
+    S = antipode R :=
+  antipode_unique h mul_antipode_lTensor_comul
+
+/-- The antipode is the unique right convolution inverse of the identity. -/
+theorem eq_antipode_of_mul_lTensor_comul {S : A →ₗ[R] A}
+    (h : LinearMap.mul' R A ∘ₗ S.lTensor A ∘ₗ comul = Algebra.linearMap R A ∘ₗ counit) :
+    S = antipode R :=
+  (antipode_unique mul_antipode_rTensor_comul h).symm
+
+end Semiring
+
+end HopfAlgebra
+
+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
 
 namespace CommSemiring
diff --git a/Mathlib/RingTheory/HopfAlgebra/Primitive.lean b/Mathlib/RingTheory/HopfAlgebra/Primitive.lean
