Skip to content

Commit d321988

Browse files
hawkrobehawkrobe
committed
feat(RingTheory/HopfAlgebra): connected graded bialgebras are Hopf algebras
1 parent 859caf7 commit d321988

6 files changed

Lines changed: 653 additions & 0 deletions

File tree

‎Mathlib.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6401,8 +6401,10 @@ public import Mathlib.RingTheory.Bialgebra.Basic
64016401
public import Mathlib.RingTheory.Bialgebra.Convolution
64026402
public import Mathlib.RingTheory.Bialgebra.Equiv
64036403
public import Mathlib.RingTheory.Bialgebra.GroupLike
6404+
public import Mathlib.RingTheory.Bialgebra.Graded
64046405
public import Mathlib.RingTheory.Bialgebra.Hom
64056406
public import Mathlib.RingTheory.Bialgebra.MonoidAlgebra
6407+
public import Mathlib.RingTheory.Bialgebra.Primitive
64066408
public import Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
64076409
public import Mathlib.RingTheory.Bialgebra.TensorProduct
64086410
public import Mathlib.RingTheory.Binomial
@@ -6414,6 +6416,7 @@ public import Mathlib.RingTheory.Coalgebra.Basic
64146416
public import Mathlib.RingTheory.Coalgebra.CoassocSimps
64156417
public import Mathlib.RingTheory.Coalgebra.Convolution
64166418
public import Mathlib.RingTheory.Coalgebra.Equiv
6419+
public import Mathlib.RingTheory.Coalgebra.Graded
64176420
public import Mathlib.RingTheory.Coalgebra.GroupLike
64186421
public import Mathlib.RingTheory.Coalgebra.Hom
64196422
public import Mathlib.RingTheory.Coalgebra.MonoidAlgebra
@@ -6556,8 +6559,10 @@ public import Mathlib.RingTheory.HahnSeries.Summable
65566559
public import Mathlib.RingTheory.HahnSeries.Valuation
65576560
public import Mathlib.RingTheory.Henselian
65586561
public import Mathlib.RingTheory.HopfAlgebra.Basic
6562+
public import Mathlib.RingTheory.HopfAlgebra.Graded
65596563
public import Mathlib.RingTheory.HopfAlgebra.GroupLike
65606564
public import Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
6565+
public import Mathlib.RingTheory.HopfAlgebra.Primitive
65616566
public import Mathlib.RingTheory.HopfAlgebra.TensorProduct
65626567
public import Mathlib.RingTheory.HopkinsLevitzki
65636568
public import Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

‎Mathlib/RingTheory/Bialgebra/Graded.lean‎

Lines changed: 183 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,183 @@
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.Basic
9+
public import Mathlib.RingTheory.Bialgebra.Primitive
10+
public import Mathlib.RingTheory.Coalgebra.Graded
11+
public import Mathlib.RingTheory.GradedAlgebra.Basic
12+
13+
/-!
14+
# Graded bialgebras
15+
16+
Structural lemmas about graded connected bialgebras.
17+
18+
## References
19+
20+
* [Grinberg, D. and Reiner, V., *Hopf Algebras in Combinatorics*][grinberg-reiner-2020],
21+
Exercise 1.3.20(h) and the proof of Proposition 1.4.16.
22+
-/
23+
24+
@[expose] public section
25+
26+
/-! ### Connectedness of a graded algebra -/
27+
28+
/-- A graded algebra is *connected* (in the Hopf-algebra sense) if its degree-zero part is
29+
spanned by the unit element `1 : A`. -/
30+
class Coalgebra.IsConnected {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
31+
{ι : Type*} [DecidableEq ι] [AddMonoid ι] (𝒜 : ι → Submodule R A) : Prop where
32+
/-- The degree-zero part is the `R`-span of `1`. -/
33+
eq_span_one : 𝒜 0 = Submodule.span R {(1 : A)}
34+
35+
namespace Coalgebra.IsConnected
36+
37+
variable {R A : Type*} [CommSemiring R] [Ring A] [Bialgebra R A]
38+
variable (𝒜 : ℕ → Submodule R A) [Coalgebra.IsConnected 𝒜]
39+
40+
open Coalgebra TensorProduct
41+
42+
/-- Every element of the degree-zero part equals its counit times the unit. -/
43+
theorem coe_eq_counit_smul_one {a : A} (ha : a ∈ 𝒜 0) : a = counit (R := R) a • 1 := by
44+
obtain ⟨r, rfl⟩ := Submodule.mem_span_singleton.mp (eq_span_one (𝒜 := 𝒜) ▸ ha)
45+
simp [Bialgebra.counit_one]
46+
47+
/-- The degree-zero submodule of a connected graded bialgebra is canonically isomorphic to
48+
the base ring via the counit. -/
49+
noncomputable def zeroLEquiv : 𝒜 0 ≃ₗ[R] R where
50+
toFun a := counit (a : A)
51+
map_add' _ _ := by simp
52+
map_smul' _ _ := by simp
53+
invFun r := ⟨r • 1, eq_span_one (𝒜 := 𝒜) ▸ Submodule.smul_mem _ r (Submodule.subset_span rfl)⟩
54+
left_inv := fun ⟨a, ha⟩ => Subtype.ext (coe_eq_counit_smul_one 𝒜 ha).symm
55+
right_inv _ := by simp [Bialgebra.counit_one]
56+
57+
@[simp]
58+
theorem zeroLEquiv_apply (a : 𝒜 0) : zeroLEquiv 𝒜 a = counit (a : A) := rfl
59+
60+
@[simp]
61+
theorem zeroLEquiv_symm_apply_coe (r : R) : ((zeroLEquiv 𝒜).symm r : A) = r • 1 := rfl
62+
63+
end Coalgebra.IsConnected
64+
65+
namespace Bialgebra
66+
67+
variable {R A : Type*} [CommSemiring R] [Ring A] [Bialgebra R A]
68+
variable (𝒜 : ℕ → Submodule R A)
69+
70+
open Coalgebra DirectSum LinearMap TensorProduct
71+
72+
/-- A linear map on `A ⊗[R] A` that carries each pure tensor of the bigraded part into a
73+
submodule `S` carries the whole `⨆_{p+q=n} 𝒜 p ⊗ 𝒜 q` into `S`. -/
74+
theorem apply_mem_of_mem_bigradedPart {M : Type*} [AddCommMonoid M] [Module R M]
75+
(f : A ⊗[R] A →ₗ[R] M) (S : Submodule R M) {n : ℕ}
76+
(h : ∀ {p q : ℕ}, p + q = n → ∀ (a : 𝒜 p) (b : 𝒜 q), f ((a : A) ⊗ₜ[R] (b : A)) ∈ S)
77+
{z : A ⊗[R] A}
78+
(hz : z ∈ ⨆ p, ⨆ q, ⨆ (_ : p + q = n),
79+
LinearMap.range (TensorProduct.map (𝒜 p).subtype (𝒜 q).subtype)) :
80+
f z ∈ S := by
81+
refine Submodule.mem_comap.mp <|
82+
(show (⨆ p, ⨆ q, ⨆ (_ : p + q = n),
83+
LinearMap.range (TensorProduct.map (𝒜 p).subtype (𝒜 q).subtype)) ≤
84+
Submodule.comap f S from ?_) hz
85+
refine iSup_le fun p => iSup_le fun q => iSup_le fun hpq => ?_
86+
rw [LinearMap.range_le_iff_comap, Submodule.eq_top_iff']
87+
intro w
88+
simp only [Submodule.mem_comap]
89+
induction w using TensorProduct.induction_on with
90+
| zero => simp
91+
| tmul a b => exact h hpq a b
92+
| add y₁ y₂ ih₁ ih₂ => simp only [map_add]; exact add_mem ih₁ ih₂
93+
94+
variable [GradedAlgebra 𝒜] [GradedCoalgebra 𝒜]
95+
96+
/-- The counit factors through the degree-zero projection. -/
97+
theorem counit_eq_counit_comp_projZero (a : A) :
98+
counit (R := R) a = counit (GradedAlgebra.proj 𝒜 0 a) := by
99+
classical
100+
rw [GradedAlgebra.proj_apply]
101+
conv_lhs => rw [← DirectSum.sum_support_decompose 𝒜 a, map_sum]
102+
exact Finset.sum_eq_single 0
103+
(fun i _ hi => GradedCoalgebra.counit_eq_zero_of_ne_zero hi (DirectSum.decompose 𝒜 a i).2)
104+
(fun h => by simp [DFinsupp.notMem_support_iff.mp h])
105+
106+
variable [Coalgebra.IsConnected 𝒜]
107+
108+
/-- Under connectedness, the degree-zero projection equals `algebraMap ∘ counit`. -/
109+
theorem proj_zero_eq_algebraMap_comp_counit :
110+
(GradedAlgebra.proj 𝒜 0 : A →ₗ[R] A) = Algebra.linearMap R A ∘ₗ counit := by
111+
ext x
112+
have hmem : GradedAlgebra.proj 𝒜 0 x ∈ 𝒜 0 := by
113+
rw [GradedAlgebra.proj_apply]; exact SetLike.coe_mem _
114+
rw [LinearMap.comp_apply, Algebra.linearMap_apply,
115+
Coalgebra.IsConnected.coe_eq_counit_smul_one 𝒜 hmem,
116+
← counit_eq_counit_comp_projZero, ← Algebra.algebraMap_eq_smul_one]
117+
118+
/-- Applying `id ⊗ q_0` to `Δ(x)` gives `x ⊗ 1`, where `q_0 = GradedAlgebra.proj 𝒜 0`. -/
119+
@[simp]
120+
theorem lTensor_projZero_comul (x : A) :
121+
(LinearMap.lTensor A (GradedAlgebra.proj 𝒜 0)) (comul x) = x ⊗ₜ[R] (1 : A) := by
122+
rw [proj_zero_eq_algebraMap_comp_counit, LinearMap.lTensor_comp_apply,
123+
Coalgebra.lTensor_counit_comul]
124+
simp
125+
126+
/-- Applying `q_0 ⊗ id` to `Δ(x)` gives `1 ⊗ x`, where `q_0 = GradedAlgebra.proj 𝒜 0`. -/
127+
@[simp]
128+
theorem rTensor_projZero_comul (x : A) :
129+
(LinearMap.rTensor A (GradedAlgebra.proj 𝒜 0)) (comul x) = (1 : A) ⊗ₜ[R] x := by
130+
rw [proj_zero_eq_algebraMap_comp_counit, LinearMap.rTensor_comp_apply,
131+
Coalgebra.rTensor_counit_comul]
132+
simp
133+
134+
/-- In a connected graded bialgebra, every homogeneous element of degree 1 is primitive. -/
135+
theorem isPrimitiveElem_of_mem_one {x : A} (hx : x ∈ 𝒜 1) : IsPrimitiveElem R x where
136+
counit_eq_zero := GradedCoalgebra.counit_eq_zero_of_ne_zero one_ne_zero hx
137+
comul_eq_tmul_one_add_one_tmul := by
138+
classical
139+
have hL : ((LinearMap.id - LinearMap.lTensor A (GradedAlgebra.proj 𝒜 0) -
140+
LinearMap.rTensor A (GradedAlgebra.proj 𝒜 0) :
141+
A ⊗[R] A →ₗ[R] A ⊗[R] A)) (comul x) = 0 := by
142+
refine (Submodule.mem_bot R).mp <| apply_mem_of_mem_bigradedPart 𝒜 _ ⊥
143+
(fun {p q} hpq a b => (Submodule.mem_bot R).mpr ?_) (GradedCoalgebra.comul_mem hx)
144+
simp only [LinearMap.sub_apply, LinearMap.id_coe, id_eq,
145+
LinearMap.lTensor_tmul, LinearMap.rTensor_tmul]
146+
obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ : p = 0 ∧ q = 1 ∨ p = 1 ∧ q = 0 := by omega
147+
· rw [show GradedAlgebra.proj 𝒜 0 (a : A) = a from
148+
DirectSum.decompose_of_mem_same _ a.2,
149+
show GradedAlgebra.proj 𝒜 0 (b : A) = 0 from
150+
DirectSum.decompose_of_mem_ne _ b.2 one_ne_zero,
151+
TensorProduct.tmul_zero, sub_zero, sub_self]
152+
· rw [show GradedAlgebra.proj 𝒜 0 (a : A) = 0 from
153+
DirectSum.decompose_of_mem_ne _ a.2 one_ne_zero,
154+
show GradedAlgebra.proj 𝒜 0 (b : A) = b from
155+
DirectSum.decompose_of_mem_same _ b.2,
156+
TensorProduct.zero_tmul, sub_zero, sub_self]
157+
simp only [LinearMap.sub_apply, LinearMap.id_coe, id_eq] at hL
158+
rw [sub_sub, sub_eq_zero, lTensor_projZero_comul, rTensor_projZero_comul] at hL
159+
exact hL
160+
161+
/-- For `x ∈ 𝒜 n`, `Δ(x) - x ⊗ 1` lies in the part of `A ⊗ A` whose left tensor factor has degree
162+
strictly less than `n`. -/
163+
theorem comul_sub_tmul_one_mem_lower {n : ℕ} {x : A} (hx : x ∈ 𝒜 n) :
164+
comul x - x ⊗ₜ[R] (1 : A) ∈
165+
⨆ p : ℕ, ⨆ q : ℕ, ⨆ (_ : p + q = n), ⨆ (_ : p < n),
166+
LinearMap.range (TensorProduct.map (𝒜 p).subtype (𝒜 q).subtype) := by
167+
classical
168+
rw [show comul x - x ⊗ₜ[R] (1 : A) =
169+
((LinearMap.id - LinearMap.lTensor A (GradedAlgebra.proj 𝒜 0) :
170+
A ⊗[R] A →ₗ[R] A ⊗[R] A)) (comul x) from by simp]
171+
refine apply_mem_of_mem_bigradedPart 𝒜 _ _ (fun {p q} hpq a b => ?_)
172+
(GradedCoalgebra.comul_mem hx)
173+
simp only [LinearMap.sub_apply, LinearMap.id_coe, id_eq, LinearMap.lTensor_tmul]
174+
rcases Nat.eq_zero_or_pos q with rfl | hq
175+
· simp
176+
· have hqb : GradedAlgebra.proj 𝒜 0 (b : A) = 0 :=
177+
DirectSum.decompose_of_mem_ne _ b.2 (Nat.pos_iff_ne_zero.mp hq)
178+
rw [hqb, TensorProduct.tmul_zero, sub_zero]
179+
exact Submodule.mem_iSup_of_mem p <| Submodule.mem_iSup_of_mem q <|
180+
Submodule.mem_iSup_of_mem hpq <| Submodule.mem_iSup_of_mem (by omega)
181+
⟨a ⊗ₜ[R] b, by simp⟩
182+
183+
end Bialgebra

‎Mathlib/RingTheory/Bialgebra/Primitive.lean‎

Lines changed: 82 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
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.Basic
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+
22+
public section
23+
24+
open Coalgebra TensorProduct
25+
26+
section Semiring
27+
variable {R A : Type*} [CommSemiring R] [Semiring A] [Bialgebra R A] {a b : A}
28+
29+
variable (R) in
30+
/-- An element `a` of a bialgebra is *primitive* if `Δ a = a ⊗ 1 + 1 ⊗ a` and `ε a = 0`. -/
31+
@[mk_iff]
32+
structure IsPrimitiveElem (a : A) : Prop where
33+
comul_eq_tmul_one_add_one_tmul : comul a = a ⊗ₜ[R] 1 + 1 ⊗ₜ[R] a
34+
counit_eq_zero : counit (R := R) a = 0
35+
36+
attribute [simp] IsPrimitiveElem.counit_eq_zero
37+
38+
@[simp] lemma IsPrimitiveElem.zero : IsPrimitiveElem R (0 : A) where
39+
comul_eq_tmul_one_add_one_tmul := by
40+
simp only [map_zero, zero_tmul, tmul_zero, add_zero]
41+
counit_eq_zero := map_zero _
42+
43+
lemma IsPrimitiveElem.add (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) :
44+
IsPrimitiveElem R (a + b) where
45+
comul_eq_tmul_one_add_one_tmul := by
46+
rw [map_add, ha.comul_eq_tmul_one_add_one_tmul, hb.comul_eq_tmul_one_add_one_tmul,
47+
add_tmul, tmul_add]; abel
48+
counit_eq_zero := by rw [map_add, ha.counit_eq_zero, hb.counit_eq_zero, add_zero]
49+
50+
lemma IsPrimitiveElem.smul (ha : IsPrimitiveElem R a) (r : R) :
51+
IsPrimitiveElem R (r • a) where
52+
comul_eq_tmul_one_add_one_tmul := by
53+
rw [LinearMap.map_smul, ha.comul_eq_tmul_one_add_one_tmul, smul_add,
54+
smul_tmul' r a 1, ← tmul_smul r 1 a]
55+
counit_eq_zero := by rw [LinearMap.map_smul, ha.counit_eq_zero, smul_zero]
56+
57+
variable (R A) in
58+
/-- The primitive elements form a submodule. -/
59+
def primitiveSubmodule : Submodule R A where
60+
carrier := {a | IsPrimitiveElem R a}
61+
add_mem' := IsPrimitiveElem.add
62+
zero_mem' := .zero
63+
smul_mem' r _ ha := ha.smul r
64+
65+
@[simp] lemma mem_primitiveSubmodule {a : A} :
66+
a ∈ primitiveSubmodule R A ↔ IsPrimitiveElem R a := Iff.rfl
67+
68+
end Semiring
69+
70+
section Ring
71+
variable {R A : Type*} [CommRing R] [Ring A] [Bialgebra R A] {a : A}
72+
73+
lemma IsPrimitiveElem.neg (ha : IsPrimitiveElem R a) : IsPrimitiveElem R (-a) where
74+
comul_eq_tmul_one_add_one_tmul := by
75+
rw [map_neg, ha.comul_eq_tmul_one_add_one_tmul, neg_add, neg_tmul, tmul_neg]
76+
counit_eq_zero := by rw [map_neg, ha.counit_eq_zero, neg_zero]
77+
78+
lemma IsPrimitiveElem.sub (ha : IsPrimitiveElem R a) {b : A} (hb : IsPrimitiveElem R b) :
79+
IsPrimitiveElem R (a - b) :=
80+
sub_eq_add_neg a b ▸ ha.add hb.neg
81+
82+
end Ring

‎Mathlib/RingTheory/Coalgebra/Graded.lean‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
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.Coalgebra.Basic
9+
10+
/-!
11+
# Graded coalgebras
12+
13+
A coalgebra `A` over `R` is *graded* by a family of submodules `𝒜 : ι → Submodule R A` if both
14+
the comultiplication and counit respect the grading: `Δ(𝒜 n) ⊆ ⨆_{p+q=n} 𝒜 p ⊗ 𝒜 q` and
15+
`ε(𝒜 n) = 0` for `n ≠ 0`.
16+
-/
17+
18+
public section
19+
20+
variable {R A ι : Type*} [CommSemiring R]
21+
[AddCommMonoid A] [Module R A] [Coalgebra R A] [AddMonoid ι]
22+
23+
/-- A coalgebra is *graded* by `𝒜 : ι → Submodule R A` if both the comultiplication and counit
24+
respect the grading: `Δ(𝒜 n) ⊆ ⨆_{p+q=n} 𝒜 p ⊗ 𝒜 q` and `ε(𝒜 n) = 0` for `n ≠ 0`. -/
25+
class GradedCoalgebra (𝒜 : ι → Submodule R A) : Prop where
26+
/-- The comultiplication takes degree-`n` elements to the sum of `𝒜 p ⊗ 𝒜 q` over `p + q = n`. -/
27+
comul_mem : ∀ {n : ι} {x : A}, x ∈ 𝒜 n →
28+
Coalgebra.comul x ∈
29+
⨆ p : ι, ⨆ q : ι, ⨆ (_ : p + q = n),
30+
LinearMap.range (TensorProduct.map (𝒜 p).subtype (𝒜 q).subtype)
31+
/-- The counit vanishes on elements of nonzero degree. -/
32+
counit_eq_zero_of_ne_zero : ∀ {n : ι} {x : A}, n ≠ 0 → x ∈ 𝒜 n →
33+
Coalgebra.counit (R := R) x = 0

0 commit comments

Comments
 (0)