Skip to content

Commit 194adf4

Browse files
hawkrobehawkrobe
committed
feat(RingTheory/HopfAlgebra/Graded): connected graded bialgebra is a Hopf algebra
1 parent b122b2d commit 194adf4

5 files changed

Lines changed: 441 additions & 3 deletions

File tree

‎Mathlib.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6363,6 +6363,7 @@ public import Mathlib.RingTheory.Bezout
63636363
public import Mathlib.RingTheory.Bialgebra.Basic
63646364
public import Mathlib.RingTheory.Bialgebra.Convolution
63656365
public import Mathlib.RingTheory.Bialgebra.Equiv
6366+
public import Mathlib.RingTheory.Bialgebra.Graded
63666367
public import Mathlib.RingTheory.Bialgebra.GroupLike
63676368
public import Mathlib.RingTheory.Bialgebra.Hom
63686369
public import Mathlib.RingTheory.Bialgebra.MonoidAlgebra
@@ -6376,6 +6377,7 @@ public import Mathlib.RingTheory.Coalgebra.Basic
63766377
public import Mathlib.RingTheory.Coalgebra.CoassocSimps
63776378
public import Mathlib.RingTheory.Coalgebra.Convolution
63786379
public import Mathlib.RingTheory.Coalgebra.Equiv
6380+
public import Mathlib.RingTheory.Coalgebra.Graded
63796381
public import Mathlib.RingTheory.Coalgebra.GroupLike
63806382
public import Mathlib.RingTheory.Coalgebra.Hom
63816383
public import Mathlib.RingTheory.Coalgebra.MonoidAlgebra
@@ -6518,6 +6520,7 @@ public import Mathlib.RingTheory.HahnSeries.Summable
65186520
public import Mathlib.RingTheory.HahnSeries.Valuation
65196521
public import Mathlib.RingTheory.Henselian
65206522
public import Mathlib.RingTheory.HopfAlgebra.Basic
6523+
public import Mathlib.RingTheory.HopfAlgebra.Graded
65216524
public import Mathlib.RingTheory.HopfAlgebra.GroupLike
65226525
public import Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
65236526
public import Mathlib.RingTheory.HopfAlgebra.Primitive

‎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/Coalgebra/Graded.lean‎

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

‎Mathlib/RingTheory/HopfAlgebra/Basic.lean‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -37,11 +37,9 @@ In this file we define `HopfAlgebra`, and provide instances for:
3737
* If `A` is commutative then `antipode` is necessarily a bijection and its square is
3838
the identity.
3939
40-
(Note that all three facts have been proved for Hopf bimonoids in an arbitrary braided category,
40+
(Note that both facts have been proved for Hopf bimonoids in an arbitrary braided category,
4141
so we could deduce the facts here from an equivalence `HopfAlgCat R ≌ Hopf (ModuleCat R)`.)
4242
43-
* A graded connected bialgebra admits a unique antipode.
44-
4543
## References
4644
4745
* <https://en.wikipedia.org/wiki/Hopf_algebra>

0 commit comments

Comments
 (0)