Skip to content

Commit 81adc65

Browse files
hawkrobehawkrobe
committed
feat(RingTheory/HopfAlgebra): construction on primitive elements
1 parent 97f1212 commit 81adc65

4 files changed

Lines changed: 280 additions & 0 deletions

File tree

‎Mathlib.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6398,6 +6398,7 @@ public import Mathlib.RingTheory.Bialgebra.Equiv
63986398
public import Mathlib.RingTheory.Bialgebra.GroupLike
63996399
public import Mathlib.RingTheory.Bialgebra.Hom
64006400
public import Mathlib.RingTheory.Bialgebra.MonoidAlgebra
6401+
public import Mathlib.RingTheory.Bialgebra.Primitive
64016402
public import Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
64026403
public import Mathlib.RingTheory.Bialgebra.TensorProduct
64036404
public import Mathlib.RingTheory.Binomial
@@ -6551,8 +6552,10 @@ public import Mathlib.RingTheory.HahnSeries.Summable
65516552
public import Mathlib.RingTheory.HahnSeries.Valuation
65526553
public import Mathlib.RingTheory.Henselian
65536554
public import Mathlib.RingTheory.HopfAlgebra.Basic
6555+
public import Mathlib.RingTheory.HopfAlgebra.Generators
65546556
public import Mathlib.RingTheory.HopfAlgebra.GroupLike
65556557
public import Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
6558+
public import Mathlib.RingTheory.HopfAlgebra.Primitive
65566559
public import Mathlib.RingTheory.HopfAlgebra.TensorProduct
65576560
public import Mathlib.RingTheory.HopkinsLevitzki
65586561
public import Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

‎Mathlib/RingTheory/Bialgebra/Primitive.lean‎

Lines changed: 104 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,104 @@
1+
/-
2+
Copyright (c) 2026 Robert Hawkins. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Robert Hawkins
5+
-/
6+
module
7+
8+
public import Mathlib.RingTheory.Bialgebra.Hom
9+
10+
/-!
11+
# Primitive elements in a bialgebra
12+
13+
This file defines primitive elements in a bialgebra, i.e. elements `a` such that
14+
`Δ a = a ⊗ₜ 1 + 1 ⊗ₜ a` and `ε a = 0`.
15+
16+
## Main declarations
17+
18+
* `IsPrimitiveElem R a`: `a` is a primitive element of the `R`-bialgebra.
19+
* `primitiveSubmodule R A`: The submodule of primitive elements of `A`.
20+
21+
## TODO
22+
23+
* `primitiveSubmodule` is a `LieSubalgebra` with bracket `[a, b] = a * b - b * a`.
24+
* In characteristic 0 over a field, the primitive elements of a cocommutative connected
25+
bialgebra generate it as the universal enveloping of a Lie algebra.
26+
-/
27+
28+
public section
29+
30+
open Bialgebra Coalgebra TensorProduct Algebra.TensorProduct
31+
32+
variable {F R A B : Type*}
33+
34+
section Semiring
35+
variable [CommSemiring R] [Semiring A] [Bialgebra R A] [Semiring B] [Bialgebra R B] {a b : A}
36+
37+
variable (R) in
38+
/-- An element `a` of a bialgebra is *primitive* if `Δ a = a ⊗ₜ 1 + 1 ⊗ₜ a` and `ε a = 0`. -/
39+
@[mk_iff]
40+
structure IsPrimitiveElem (a : A) : Prop where
41+
/-- A primitive element `a` satisfies `ε(a) = 0`. -/
42+
counit_eq_zero : counit (R := R) a = 0
43+
/-- A primitive element `a` satisfies `Δ(a) = a ⊗ₜ 1 + 1 ⊗ₜ a`. -/
44+
comul_eq_tmul_add_tmul : comul a = a ⊗ₜ[R] 1 + 1 ⊗ₜ[R] a
45+
46+
attribute [simp] IsPrimitiveElem.counit_eq_zero IsPrimitiveElem.comul_eq_tmul_add_tmul
47+
48+
/-- In a bialgebra, `0` is a primitive element. -/
49+
lemma IsPrimitiveElem.zero : IsPrimitiveElem R (0 : A) where
50+
counit_eq_zero := map_zero _
51+
comul_eq_tmul_add_tmul := by simp
52+
53+
/-- Primitive elements in a bialgebra are stable under addition. -/
54+
lemma IsPrimitiveElem.add (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) :
55+
IsPrimitiveElem R (a + b) where
56+
counit_eq_zero := by simp [ha, hb]
57+
comul_eq_tmul_add_tmul := by simp [ha, hb, add_tmul, tmul_add]; abel
58+
59+
/-- Primitive elements in a bialgebra are stable under scalar multiplication. -/
60+
lemma IsPrimitiveElem.smul (ha : IsPrimitiveElem R a) (r : R) :
61+
IsPrimitiveElem R (r • a) where
62+
counit_eq_zero := by simp [ha]
63+
comul_eq_tmul_add_tmul := by simp [ha, smul_add, smul_tmul']
64+
65+
/-- A bialgebra homomorphism sends primitive elements to primitive elements. -/
66+
lemma IsPrimitiveElem.map [FunLike F A B] [BialgHomClass F R A B] (f : F)
67+
(ha : IsPrimitiveElem R a) : IsPrimitiveElem R (f a) where
68+
counit_eq_zero := by simp [ha]
69+
comul_eq_tmul_add_tmul := by rw [← CoalgHomClass.map_comp_comul_apply]; simp [ha]
70+
71+
variable (R A) in
72+
/-- The primitive elements form a submodule. -/
73+
def primitiveSubmodule : Submodule R A where
74+
carrier := {a | IsPrimitiveElem R a}
75+
add_mem' := .add
76+
zero_mem' := .zero
77+
smul_mem' r _ ha := ha.smul r
78+
79+
@[simp] lemma mem_primitiveSubmodule :
80+
a ∈ primitiveSubmodule R A ↔ IsPrimitiveElem R a := Iff.rfl
81+
82+
end Semiring
83+
84+
section Ring
85+
variable [CommSemiring R] [Ring A] [Bialgebra R A] {a b : A}
86+
87+
/-- Primitive elements in a bialgebra are stable under negation. -/
88+
lemma IsPrimitiveElem.neg (ha : IsPrimitiveElem R a) : IsPrimitiveElem R (-a) where
89+
counit_eq_zero := by simpa [ha, neg_add_cancel] using (map_add (counit (R := R)) (-a) a).symm
90+
comul_eq_tmul_add_tmul := by rw [map_neg, ha.comul_eq_tmul_add_tmul, neg_add, neg_tmul, tmul_neg]
91+
92+
/-- Primitive elements in a bialgebra are stable under subtraction. -/
93+
lemma IsPrimitiveElem.sub (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) :
94+
IsPrimitiveElem R (a - b) :=
95+
sub_eq_add_neg a b ▸ ha.add hb.neg
96+
97+
/-- The commutator `[a, b] = a * b - b * a` of two primitive elements is primitive. -/
98+
lemma IsPrimitiveElem.commutator (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) :
99+
IsPrimitiveElem R (a * b - b * a) where
100+
counit_eq_zero := by
101+
simpa [ha, hb, sub_add_cancel] using (map_add (counit (R := R)) (a * b - b * a) (b * a)).symm
102+
comul_eq_tmul_add_tmul := by simp [ha, hb, add_mul, mul_add, sub_tmul, tmul_sub]; abel
103+
104+
end Ring

‎Mathlib/RingTheory/HopfAlgebra/Generators.lean‎

Lines changed: 114 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,114 @@
1+
/-
2+
Copyright (c) 2026 Robert Hawkins. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Robert Hawkins
5+
-/
6+
module
7+
8+
public import Mathlib.RingTheory.Bialgebra.Convolution
9+
public import Mathlib.RingTheory.HopfAlgebra.Basic
10+
11+
/-!
12+
# Constructing Hopf algebras from algebra generators
13+
14+
This file provides constructors for Hopf algebras given antimultiplicative
15+
antipode data on an algebra-generating set.
16+
17+
## Main declarations
18+
19+
* `HopfAlgebra.ofGenerators` : construct a Hopf algebra from data on a generating set.
20+
* `HopfAlgebra.convMul_id_eq_one_of_adjoin_eq_top` and `id_convMul_eq_one_of_adjoin_eq_top`:
21+
the extension principle promoting a pointwise convolution inverse on generators to a global
22+
identity.
23+
-/
24+
25+
public section
26+
27+
namespace HopfAlgebra
28+
29+
open Coalgebra LinearMap WithConv
30+
31+
variable {R A : Type*} [CommSemiring R]
32+
33+
section ExtensionPrinciple
34+
35+
/-! ### Extension principle from algebra generators -/
36+
37+
variable [Semiring A] [Bialgebra R A] {S₀ : A →ₗ[R] A} {s : Set A}
38+
39+
/-- If a unital antimultiplicative map `S₀` satisfies `toConv S₀ * toConv .id = 1` pointwise
40+
on an algebra-generating set, then it does so globally. -/
41+
theorem convMul_id_eq_one_of_adjoin_eq_top (S₀_one : S₀ 1 = 1)
42+
(S₀_mul : ∀ x y : A, S₀ (x * y) = S₀ y * S₀ x)
43+
(adjoin_eq_top : Algebra.adjoin R s = ⊤)
44+
(S₀_convMul_id : ∀ p ∈ s,
45+
(toConv S₀ * toConv (.id : A →ₗ[R] A)) p = (1 : WithConv (A →ₗ[R] A)) p) :
46+
toConv S₀ * toConv .id = 1 := by
47+
refine WithConv.ext (ext fun x => ?_)
48+
refine Algebra.adjoin_induction S₀_convMul_id
49+
(fun r => by simp [S₀_one, Algebra.algebraMap_eq_smul_one, Algebra.TensorProduct.one_def])
50+
(fun a b _ _ ha hb => by simp [map_add, ha, hb])
51+
(fun a b _ _ ha hb => ?_) (adjoin_eq_top ▸ Algebra.mem_top : x ∈ Algebra.adjoin R s)
52+
let 𝓡a := ℛ R a; let 𝓡b := ℛ R b
53+
simp only [𝓡a.convMul_apply, 𝓡b.convMul_apply, id_apply, convOne_apply] at ha hb
54+
rw [convOne_apply]
55+
calc (toConv S₀ * toConv (.id : A →ₗ[R] A)) (a * b)
56+
_ = ∑ p ∈ 𝓡a.index, ∑ q ∈ 𝓡b.index,
57+
S₀ (𝓡a.left p * 𝓡b.left q) * (𝓡a.right p * 𝓡b.right q) := by
58+
simp [← 𝓡a.eq, ← 𝓡b.eq, Finset.sum_mul_sum]
59+
_ = ∑ p ∈ 𝓡a.index, ∑ q ∈ 𝓡b.index,
60+
S₀ (𝓡b.left q) * (S₀ (𝓡a.left p) * 𝓡a.right p) * 𝓡b.right q := by
61+
simp_rw [S₀_mul, mul_assoc]
62+
_ = ∑ q ∈ 𝓡b.index, algebraMap R A (counit a) * S₀ (𝓡b.left q) * 𝓡b.right q := by
63+
rw [Finset.sum_comm]; simp_rw [← Finset.sum_mul, ← Finset.mul_sum, ha, ← Algebra.commutes]
64+
_ = algebraMap R A (counit (a * b)) := by
65+
simp_rw [mul_assoc, ← Finset.mul_sum, hb, ← map_mul, ← Bialgebra.counit_mul]
66+
67+
/-- Analogue of `convMul_id_eq_one_of_adjoin_eq_top` for `toConv .id * toConv S₀ = 1`. -/
68+
theorem id_convMul_eq_one_of_adjoin_eq_top (S₀_one : S₀ 1 = 1)
69+
(S₀_mul : ∀ x y : A, S₀ (x * y) = S₀ y * S₀ x)
70+
(adjoin_eq_top : Algebra.adjoin R s = ⊤)
71+
(id_convMul_S₀ : ∀ p ∈ s,
72+
(toConv (.id : A →ₗ[R] A) * toConv S₀) p = (1 : WithConv (A →ₗ[R] A)) p) :
73+
toConv .id * toConv S₀ = 1 := by
74+
refine WithConv.ext (ext fun x => ?_)
75+
refine Algebra.adjoin_induction id_convMul_S₀
76+
(fun r => by simp [S₀_one, Algebra.algebraMap_eq_smul_one, Algebra.TensorProduct.one_def])
77+
(fun a b _ _ ha hb => by simp [map_add, ha, hb])
78+
(fun a b _ _ ha hb => ?_) (adjoin_eq_top ▸ Algebra.mem_top : x ∈ Algebra.adjoin R s)
79+
let 𝓡a := ℛ R a; let 𝓡b := ℛ R b
80+
simp only [𝓡a.convMul_apply, 𝓡b.convMul_apply, id_apply, convOne_apply] at ha hb
81+
rw [convOne_apply]
82+
calc (toConv (.id : A →ₗ[R] A) * toConv S₀) (a * b)
83+
_ = ∑ p ∈ 𝓡a.index, ∑ q ∈ 𝓡b.index,
84+
(𝓡a.left p * 𝓡b.left q) * S₀ (𝓡a.right p * 𝓡b.right q) := by
85+
simp [← 𝓡a.eq, ← 𝓡b.eq, Finset.sum_mul_sum]
86+
_ = ∑ p ∈ 𝓡a.index, ∑ q ∈ 𝓡b.index,
87+
𝓡a.left p * (𝓡b.left q * S₀ (𝓡b.right q)) * S₀ (𝓡a.right p) := by
88+
simp_rw [S₀_mul, mul_assoc]
89+
_ = ∑ p ∈ 𝓡a.index,
90+
algebraMap R A (counit b) * 𝓡a.left p * S₀ (𝓡a.right p) := by
91+
simp_rw [← Finset.sum_mul, ← Finset.mul_sum, hb, ← Algebra.commutes]
92+
_ = algebraMap R A (counit (a * b)) := by
93+
simp_rw [mul_assoc, ← Finset.mul_sum, ha, ← map_mul, mul_comm (counit b),
94+
← Bialgebra.counit_mul]
95+
96+
variable (S₀) in
97+
/-- Upgrade a bialgebra to a Hopf algebra from a unital antimultiplicative candidate antipode
98+
that is a two-sided convolution inverse of the identity pointwise on an algebra-generating
99+
set. -/
100+
noncomputable abbrev ofGenerators (S₀_one : S₀ 1 = 1)
101+
(S₀_mul : ∀ x y : A, S₀ (x * y) = S₀ y * S₀ x)
102+
(adjoin_eq_top : Algebra.adjoin R s = ⊤)
103+
(S₀_convMul_id : ∀ p ∈ s,
104+
(toConv S₀ * toConv (.id : A →ₗ[R] A)) p = (1 : WithConv (A →ₗ[R] A)) p)
105+
(id_convMul_S₀ : ∀ p ∈ s,
106+
(toConv (.id : A →ₗ[R] A) * toConv S₀) p = (1 : WithConv (A →ₗ[R] A)) p) :
107+
HopfAlgebra R A :=
108+
ofConvInverse S₀
109+
(convMul_id_eq_one_of_adjoin_eq_top S₀_one S₀_mul adjoin_eq_top S₀_convMul_id)
110+
(id_convMul_eq_one_of_adjoin_eq_top S₀_one S₀_mul adjoin_eq_top id_convMul_S₀)
111+
112+
end ExtensionPrinciple
113+
114+
end HopfAlgebra

‎Mathlib/RingTheory/HopfAlgebra/Primitive.lean‎

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
/-
2+
Copyright (c) 2026 Robert Hawkins. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Robert Hawkins
5+
-/
6+
module
7+
8+
public import Mathlib.RingTheory.Bialgebra.Primitive
9+
public import Mathlib.RingTheory.HopfAlgebra.Generators
10+
11+
/-!
12+
# Primitive elements in a Hopf algebra
13+
14+
Facts about primitive elements in a Hopf algebra, plus `HopfAlgebra.ofPrimitives`,
15+
a constructor for Hopf algebras generated as algebras by primitive elements.
16+
17+
## Main declarations
18+
19+
* `IsPrimitiveElem.antipode_eq_neg` : the antipode sends primitive elements to their negation.
20+
* `IsPrimitiveElem.antipode` : the antipode preserves primitivity.
21+
* `HopfAlgebra.ofPrimitives` : construct a Hopf algebra from a primitive-element generating set.
22+
-/
23+
24+
public section
25+
26+
open HopfAlgebra LinearMap MulOpposite
27+
28+
variable {R A : Type*} [CommSemiring R]
29+
30+
section Ring
31+
variable [Ring A] [HopfAlgebra R A] {a : A}
32+
33+
/-- The antipode of a Hopf algebra sends primitive elements to their negation. -/
34+
@[simp] theorem IsPrimitiveElem.antipode_eq_neg (ha : IsPrimitiveElem R a) : antipode R a = -a :=
35+
eq_neg_of_add_eq_zero_left <| by
36+
simpa [ha] using mul_antipode_rTensor_comul_apply (R := R) a
37+
38+
/-- The antipode preserves primitivity. -/
39+
protected lemma IsPrimitiveElem.antipode (ha : IsPrimitiveElem R a) :
40+
IsPrimitiveElem R (antipode R a) :=
41+
ha.antipode_eq_neg ▸ ha.neg
42+
43+
end Ring
44+
45+
namespace HopfAlgebra
46+
47+
/-- Upgrade a bialgebra generated by primitive elements to a Hopf algebra by specifying the
48+
antipode-on-generators formula `S p = op (-p)`. -/
49+
noncomputable abbrev ofPrimitives [Ring A] [Bialgebra R A]
50+
(S : A →ₐ[R] Aᵐᵒᵖ) {s : Set A}
51+
(adjoin_eq_top : Algebra.adjoin R s = ⊤)
52+
(prim : ∀ p ∈ s, IsPrimitiveElem R p)
53+
(S_apply : ∀ p ∈ s, S p = op (-p)) :
54+
HopfAlgebra R A := by
55+
refine ofGenerators ((opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap)
56+
(by simp) (fun _ _ => by simp) adjoin_eq_top ?_ ?_ <;>
57+
exact fun p hp => by simp [convMul_apply, prim p hp, S_apply p hp]
58+
59+
end HopfAlgebra

0 commit comments

Comments
 (0)