Skip to content

Commit b25795e

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

4 files changed

Lines changed: 294 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: 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.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.counit_eq_zero, hb.counit_eq_zero]
57+
comul_eq_tmul_add_tmul := by
58+
simp [ha.comul_eq_tmul_add_tmul, hb.comul_eq_tmul_add_tmul, add_tmul, tmul_add]; abel
59+
60+
/-- Primitive elements in a bialgebra are stable under scalar multiplication. -/
61+
lemma IsPrimitiveElem.smul (ha : IsPrimitiveElem R a) (r : R) :
62+
IsPrimitiveElem R (r • a) where
63+
counit_eq_zero := by rw [map_smul, ha.counit_eq_zero, smul_zero]
64+
comul_eq_tmul_add_tmul := by simp [ha.comul_eq_tmul_add_tmul, smul_add, smul_tmul']
65+
66+
/-- A bialgebra homomorphism sends primitive elements to primitive elements. -/
67+
lemma IsPrimitiveElem.map [FunLike F A B] [BialgHomClass F R A B] (f : F)
68+
(ha : IsPrimitiveElem R a) : IsPrimitiveElem R (f a) where
69+
counit_eq_zero := by simp [ha.counit_eq_zero]
70+
comul_eq_tmul_add_tmul := by
71+
rw [← CoalgHomClass.map_comp_comul_apply, ha.comul_eq_tmul_add_tmul]; simp
72+
73+
variable (R A) in
74+
/-- The primitive elements form a submodule. -/
75+
def primitiveSubmodule : Submodule R A where
76+
carrier := {a | IsPrimitiveElem R a}
77+
add_mem' := IsPrimitiveElem.add
78+
zero_mem' := .zero
79+
smul_mem' r _ ha := ha.smul r
80+
81+
@[simp] lemma mem_primitiveSubmodule :
82+
a ∈ primitiveSubmodule R A ↔ IsPrimitiveElem R a := Iff.rfl
83+
84+
end Semiring
85+
86+
section Ring
87+
variable [CommSemiring R] [Ring A] [Bialgebra R A] {a b : A}
88+
89+
/-- Primitive elements in a bialgebra are stable under negation. -/
90+
lemma IsPrimitiveElem.neg (ha : IsPrimitiveElem R a) : IsPrimitiveElem R (-a) where
91+
counit_eq_zero := by
92+
have h : counit (R := R) (-a) + counit (R := R) a = 0 := by
93+
rw [← map_add, neg_add_cancel, map_zero]
94+
simpa [ha.counit_eq_zero] using h
95+
comul_eq_tmul_add_tmul := by rw [map_neg, ha.comul_eq_tmul_add_tmul, neg_add, neg_tmul, tmul_neg]
96+
97+
/-- Primitive elements in a bialgebra are stable under subtraction. -/
98+
lemma IsPrimitiveElem.sub (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) :
99+
IsPrimitiveElem R (a - b) :=
100+
sub_eq_add_neg a b ▸ ha.add hb.neg
101+
102+
/-- The commutator `[a, b] = a * b - b * a` of two primitive elements is primitive. -/
103+
lemma IsPrimitiveElem.commutator (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) :
104+
IsPrimitiveElem R (a * b - b * a) where
105+
counit_eq_zero := by
106+
have h : counit (R := R) (a * b - b * a) + counit (R := R) (b * a) = 0 := by
107+
rw [← map_add, sub_add_cancel, counit_mul, ha.counit_eq_zero, zero_mul]
108+
simpa [hb.counit_eq_zero] using h
109+
comul_eq_tmul_add_tmul := by
110+
simp only [map_sub, comul_mul, ha.comul_eq_tmul_add_tmul, hb.comul_eq_tmul_add_tmul,
111+
add_mul, mul_add, tmul_mul_tmul, mul_one, one_mul, sub_tmul, tmul_sub]
112+
abel
113+
114+
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: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
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 := by
35+
have key := mul_antipode_rTensor_comul_apply (R := R) a
36+
simp only [ha.comul_eq_tmul_add_tmul, ha.counit_eq_zero, map_add, rTensor_tmul,
37+
antipode_one, mul'_apply, mul_one, one_mul, map_zero] at key
38+
exact eq_neg_of_add_eq_zero_left key
39+
40+
/-- The antipode preserves primitivity. -/
41+
protected lemma IsPrimitiveElem.antipode (ha : IsPrimitiveElem R a) :
42+
IsPrimitiveElem R (antipode R a) :=
43+
ha.antipode_eq_neg ▸ ha.neg
44+
45+
end Ring
46+
47+
namespace HopfAlgebra
48+
49+
/-- Upgrade a bialgebra generated by primitive elements to a Hopf algebra by specifying the
50+
antipode-on-generators formula `S p = op (-p)`. -/
51+
noncomputable abbrev ofPrimitives [Ring A] [Bialgebra R A]
52+
(S : A →ₐ[R] Aᵐᵒᵖ) {s : Set A}
53+
(adjoin_eq_top : Algebra.adjoin R s = ⊤)
54+
(prim : ∀ p ∈ s, IsPrimitiveElem R p)
55+
(S_apply : ∀ p ∈ s, S p = op (-p)) :
56+
HopfAlgebra R A := by
57+
refine ofGenerators ((opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap)
58+
(by simp [map_one]) (fun _ _ => by simp [map_mul]) adjoin_eq_top ?_ ?_ <;>
59+
exact fun p hp => by
60+
simp [convMul_apply, (prim p hp).comul_eq_tmul_add_tmul,
61+
(prim p hp).counit_eq_zero, S_apply p hp]
62+
63+
end HopfAlgebra

0 commit comments

Comments
 (0)