Skip to content

Commit fd6aa8e

Browse files
hawkrobehawkrobe
committed
feat(RingTheory/HopfAlgebra): construction on primitive elements
1 parent db77934 commit fd6aa8e

4 files changed

Lines changed: 273 additions & 0 deletions

File tree

‎Mathlib.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6368,6 +6368,7 @@ public import Mathlib.RingTheory.Bialgebra.Equiv
63686368
public import Mathlib.RingTheory.Bialgebra.GroupLike
63696369
public import Mathlib.RingTheory.Bialgebra.Hom
63706370
public import Mathlib.RingTheory.Bialgebra.MonoidAlgebra
6371+
public import Mathlib.RingTheory.Bialgebra.Primitive
63716372
public import Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
63726373
public import Mathlib.RingTheory.Bialgebra.TensorProduct
63736374
public import Mathlib.RingTheory.Binomial
@@ -6519,8 +6520,10 @@ public import Mathlib.RingTheory.HahnSeries.Summable
65196520
public import Mathlib.RingTheory.HahnSeries.Valuation
65206521
public import Mathlib.RingTheory.Henselian
65216522
public import Mathlib.RingTheory.HopfAlgebra.Basic
6523+
public import Mathlib.RingTheory.HopfAlgebra.Generators
65226524
public import Mathlib.RingTheory.HopfAlgebra.GroupLike
65236525
public import Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
6526+
public import Mathlib.RingTheory.HopfAlgebra.Primitive
65246527
public import Mathlib.RingTheory.HopfAlgebra.TensorProduct
65256528
public import Mathlib.RingTheory.HopkinsLevitzki
65266529
public import Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

‎Mathlib/RingTheory/Bialgebra/Primitive.lean‎

Lines changed: 100 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,100 @@
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+
counit_eq_zero : counit (R := R) a = 0
42+
comul_eq_tmul_add_tmul : comul a = a ⊗ₜ[R] 1 + 1 ⊗ₜ[R] a
43+
44+
attribute [simp] IsPrimitiveElem.counit_eq_zero IsPrimitiveElem.comul_eq_tmul_add_tmul
45+
46+
lemma IsPrimitiveElem.zero : IsPrimitiveElem R (0 : A) where
47+
counit_eq_zero := map_zero _
48+
comul_eq_tmul_add_tmul := by simp
49+
50+
lemma IsPrimitiveElem.add (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) :
51+
IsPrimitiveElem R (a + b) where
52+
counit_eq_zero := by simp [ha.counit_eq_zero, hb.counit_eq_zero]
53+
comul_eq_tmul_add_tmul := by
54+
simp [ha.comul_eq_tmul_add_tmul, hb.comul_eq_tmul_add_tmul, add_tmul, tmul_add]; abel
55+
56+
lemma IsPrimitiveElem.smul (ha : IsPrimitiveElem R a) (r : R) :
57+
IsPrimitiveElem R (r • a) where
58+
counit_eq_zero := by rw [map_smul, ha.counit_eq_zero, smul_zero]
59+
comul_eq_tmul_add_tmul := by simp [ha.comul_eq_tmul_add_tmul, smul_add, smul_tmul']
60+
61+
lemma IsPrimitiveElem.map [FunLike F A B] [BialgHomClass F R A B] (f : F)
62+
(ha : IsPrimitiveElem R a) : IsPrimitiveElem R (f a) where
63+
counit_eq_zero := by simp [ha.counit_eq_zero]
64+
comul_eq_tmul_add_tmul := by
65+
rw [← CoalgHomClass.map_comp_comul_apply, ha.comul_eq_tmul_add_tmul]; simp
66+
67+
variable (R A) in
68+
/-- The primitive elements form a submodule. -/
69+
def primitiveSubmodule : Submodule R A where
70+
carrier := {a | IsPrimitiveElem R a}
71+
add_mem' := IsPrimitiveElem.add
72+
zero_mem' := .zero
73+
smul_mem' r _ ha := ha.smul r
74+
75+
@[simp] lemma mem_primitiveSubmodule {a : A} :
76+
a ∈ primitiveSubmodule R A ↔ IsPrimitiveElem R a := Iff.rfl
77+
78+
end Semiring
79+
80+
section Ring
81+
variable [CommRing R] [Ring A] [Bialgebra R A] {a b : A}
82+
83+
lemma IsPrimitiveElem.neg (ha : IsPrimitiveElem R a) : IsPrimitiveElem R (-a) where
84+
counit_eq_zero := by rw [map_neg, ha.counit_eq_zero, neg_zero]
85+
comul_eq_tmul_add_tmul := by rw [map_neg, ha.comul_eq_tmul_add_tmul, neg_add, neg_tmul, tmul_neg]
86+
87+
lemma IsPrimitiveElem.sub (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) :
88+
IsPrimitiveElem R (a - b) :=
89+
sub_eq_add_neg a b ▸ ha.add hb.neg
90+
91+
/-- The commutator `[a, b] = a * b - b * a` of two primitive elements is primitive. -/
92+
lemma IsPrimitiveElem.commutator (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) :
93+
IsPrimitiveElem R (a * b - b * a) where
94+
counit_eq_zero := by simp [ha.counit_eq_zero, hb.counit_eq_zero]
95+
comul_eq_tmul_add_tmul := by
96+
simp only [map_sub, comul_mul, ha.comul_eq_tmul_add_tmul, hb.comul_eq_tmul_add_tmul,
97+
add_mul, mul_add, tmul_mul_tmul, mul_one, one_mul, sub_tmul, tmul_sub]
98+
abel
99+
100+
end Ring

‎Mathlib/RingTheory/HopfAlgebra/Generators.lean‎

Lines changed: 111 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,111 @@
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 its left analogue: the
21+
extension principle promoting pointwise convolution-inverse on generators to a global identity.
22+
-/
23+
24+
public section
25+
26+
namespace HopfAlgebra
27+
28+
open Coalgebra LinearMap WithConv
29+
30+
variable {R A : Type*} [CommSemiring R]
31+
32+
section ExtensionPrinciple
33+
34+
/-! ### Extension principle from algebra generators -/
35+
36+
variable [Semiring A] [Bialgebra R A] {S₀ : A →ₗ[R] A} {s : Set A}
37+
38+
/-- A unital antimultiplicative right convolution inverse of the identity on an
39+
algebra-generating set is one globally. -/
40+
theorem convMul_id_eq_one_of_adjoin_eq_top (hS₀_one : S₀ 1 = 1)
41+
(hS₀_anti : ∀ x y : A, S₀ (x * y) = S₀ y * S₀ x)
42+
(hgen : Algebra.adjoin R s = ⊤)
43+
(h_on_s : ∀ p ∈ s,
44+
(toConv S₀ * toConv (.id : A →ₗ[R] A)) p = (1 : WithConv (A →ₗ[R] A)) p) :
45+
toConv S₀ * toConv .id = 1 := by
46+
refine WithConv.ext (ext fun x => ?_)
47+
refine Algebra.adjoin_induction h_on_s
48+
(fun r => by simp [hS₀_one, Algebra.algebraMap_eq_smul_one, Algebra.TensorProduct.one_def])
49+
(fun a b _ _ ha hb => by simp [map_add, ha, hb])
50+
(fun a b _ _ ha hb => ?_) (hgen ▸ Algebra.mem_top : x ∈ Algebra.adjoin R s)
51+
let 𝓡a := ℛ R a; let 𝓡b := ℛ R b
52+
simp only [𝓡a.convMul_apply, 𝓡b.convMul_apply, id_apply, convOne_apply] at ha hb
53+
rw [convOne_apply]
54+
calc (toConv S₀ * toConv (.id : A →ₗ[R] A)) (a * b)
55+
_ = ∑ p ∈ 𝓡a.index, ∑ q ∈ 𝓡b.index,
56+
S₀ (𝓡a.left p * 𝓡b.left q) * (𝓡a.right p * 𝓡b.right q) := by
57+
simp [← 𝓡a.eq, ← 𝓡b.eq, Finset.sum_mul_sum]
58+
_ = ∑ p ∈ 𝓡a.index, ∑ q ∈ 𝓡b.index,
59+
S₀ (𝓡b.left q) * (S₀ (𝓡a.left p) * 𝓡a.right p) * 𝓡b.right q := by
60+
simp_rw [hS₀_anti, mul_assoc]
61+
_ = ∑ q ∈ 𝓡b.index, algebraMap R A (counit a) * S₀ (𝓡b.left q) * 𝓡b.right q := by
62+
rw [Finset.sum_comm]; simp_rw [← Finset.sum_mul, ← Finset.mul_sum, ha, ← Algebra.commutes]
63+
_ = algebraMap R A (counit (a * b)) := by
64+
simp_rw [mul_assoc, ← Finset.mul_sum, hb, ← map_mul, ← Bialgebra.counit_mul]
65+
66+
/-- Left analogue of `convMul_id_eq_one_of_adjoin_eq_top`. -/
67+
theorem id_convMul_eq_one_of_adjoin_eq_top (hS₀_one : S₀ 1 = 1)
68+
(hS₀_anti : ∀ x y : A, S₀ (x * y) = S₀ y * S₀ x)
69+
(hgen : Algebra.adjoin R s = ⊤)
70+
(h_on_s : ∀ p ∈ s,
71+
(toConv (.id : A →ₗ[R] A) * toConv S₀) p = (1 : WithConv (A →ₗ[R] A)) p) :
72+
toConv .id * toConv S₀ = 1 := by
73+
refine WithConv.ext (ext fun x => ?_)
74+
refine Algebra.adjoin_induction h_on_s
75+
(fun r => by simp [hS₀_one, Algebra.algebraMap_eq_smul_one, Algebra.TensorProduct.one_def])
76+
(fun a b _ _ ha hb => by simp [map_add, ha, hb])
77+
(fun a b _ _ ha hb => ?_) (hgen ▸ Algebra.mem_top : x ∈ Algebra.adjoin R s)
78+
let 𝓡a := ℛ R a; let 𝓡b := ℛ R b
79+
simp only [𝓡a.convMul_apply, 𝓡b.convMul_apply, id_apply, convOne_apply] at ha hb
80+
rw [convOne_apply]
81+
calc (toConv (.id : A →ₗ[R] A) * toConv S₀) (a * b)
82+
_ = ∑ p ∈ 𝓡a.index, ∑ q ∈ 𝓡b.index,
83+
(𝓡a.left p * 𝓡b.left q) * S₀ (𝓡a.right p * 𝓡b.right q) := by
84+
simp [← 𝓡a.eq, ← 𝓡b.eq, Finset.sum_mul_sum]
85+
_ = ∑ p ∈ 𝓡a.index, ∑ q ∈ 𝓡b.index,
86+
𝓡a.left p * (𝓡b.left q * S₀ (𝓡b.right q)) * S₀ (𝓡a.right p) := by
87+
simp_rw [hS₀_anti, mul_assoc]
88+
_ = ∑ p ∈ 𝓡a.index,
89+
algebraMap R A (counit b) * 𝓡a.left p * S₀ (𝓡a.right p) := by
90+
simp_rw [← Finset.sum_mul, ← Finset.mul_sum, hb, ← Algebra.commutes]
91+
_ = algebraMap R A (counit (a * b)) := by
92+
simp_rw [mul_assoc, ← Finset.mul_sum, ha, ← map_mul, mul_comm (counit b),
93+
← Bialgebra.counit_mul]
94+
95+
variable (S₀) in
96+
/-- Upgrade a bialgebra to a Hopf algebra from a unital antimultiplicative candidate antipode
97+
that is a two-sided convolution inverse of the identity pointwise on an algebra-generating
98+
set. -/
99+
noncomputable abbrev ofGenerators (hS₀_one : S₀ 1 = 1)
100+
(hS₀_anti : ∀ x y : A, S₀ (x * y) = S₀ y * S₀ x)
101+
(hgen : Algebra.adjoin R s = ⊤)
102+
(hl : ∀ p ∈ s, (toConv S₀ * toConv (.id : A →ₗ[R] A)) p = (1 : WithConv (A →ₗ[R] A)) p)
103+
(hr : ∀ p ∈ s, (toConv (.id : A →ₗ[R] A) * toConv S₀) p = (1 : WithConv (A →ₗ[R] A)) p) :
104+
HopfAlgebra R A :=
105+
ofConvInverse S₀
106+
(convMul_id_eq_one_of_adjoin_eq_top hS₀_one hS₀_anti hgen hl)
107+
(id_convMul_eq_one_of_adjoin_eq_top hS₀_one hS₀_anti hgen hr)
108+
109+
end ExtensionPrinciple
110+
111+
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+
/-- The antipode of a Hopf algebra sends primitive elements to their negation. -/
31+
@[simp] theorem IsPrimitiveElem.antipode_eq_neg [Ring A] [HopfAlgebra R A] {a : A}
32+
(ha : IsPrimitiveElem R a) : antipode R a = -a := by
33+
have key := mul_antipode_rTensor_comul_apply (R := R) a
34+
simp only [ha.comul_eq_tmul_add_tmul, ha.counit_eq_zero, map_add, rTensor_tmul,
35+
antipode_one, mul'_apply, mul_one, one_mul, map_zero] at key
36+
exact eq_neg_of_add_eq_zero_left key
37+
38+
/-- The antipode preserves primitivity. -/
39+
protected lemma IsPrimitiveElem.antipode {R A : Type*} [CommRing R] [Ring A]
40+
[HopfAlgebra R A] {a : A} (ha : IsPrimitiveElem R a) : IsPrimitiveElem R (antipode R a) :=
41+
ha.antipode_eq_neg ▸ ha.neg
42+
43+
namespace HopfAlgebra
44+
45+
/-- Upgrade a bialgebra generated by primitive elements to a Hopf algebra by specifying the
46+
antipode-on-generators formula `S p = op (-p)`. -/
47+
noncomputable abbrev ofPrimitives [Ring A] [Bialgebra R A]
48+
(S : A →ₐ[R] Aᵐᵒᵖ) {s : Set A}
49+
(hs_gen : Algebra.adjoin R s = ⊤)
50+
(hs_prim : ∀ p ∈ s, IsPrimitiveElem R p)
51+
(hS : ∀ p ∈ s, S p = op (-p)) :
52+
HopfAlgebra R A := by
53+
refine ofGenerators ((opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap)
54+
(by simp [map_one]) (fun _ _ => by simp [map_mul]) hs_gen ?_ ?_ <;>
55+
exact fun p hp => by
56+
simp [convMul_apply, (hs_prim p hp).comul_eq_tmul_add_tmul,
57+
(hs_prim p hp).counit_eq_zero, hS p hp]
58+
59+
end HopfAlgebra

0 commit comments

Comments
 (0)