feat(RingTheory): Every connected graded bialgebra is a Hopf algebra

Mathlib.lean

@@ -6483,6 +6483,7 @@ public import Mathlib.RingTheory.Bezout
 public import Mathlib.RingTheory.Bialgebra.Basic
 public import Mathlib.RingTheory.Bialgebra.Convolution
 public import Mathlib.RingTheory.Bialgebra.Equiv
+public import Mathlib.RingTheory.Bialgebra.Graded
 public import Mathlib.RingTheory.Bialgebra.GroupLike
 public import Mathlib.RingTheory.Bialgebra.Hom
 public import Mathlib.RingTheory.Bialgebra.MonoidAlgebra
@@ -6498,6 +6499,7 @@ public import Mathlib.RingTheory.Coalgebra.Basic
 public import Mathlib.RingTheory.Coalgebra.CoassocSimps
 public import Mathlib.RingTheory.Coalgebra.Convolution
 public import Mathlib.RingTheory.Coalgebra.Equiv
+public import Mathlib.RingTheory.Coalgebra.Graded
 public import Mathlib.RingTheory.Coalgebra.GroupLike
 public import Mathlib.RingTheory.Coalgebra.Hom
 public import Mathlib.RingTheory.Coalgebra.MonoidAlgebra
@@ -6622,6 +6624,7 @@ public import Mathlib.RingTheory.FreeRing
 public import Mathlib.RingTheory.Frobenius
 public import Mathlib.RingTheory.GradedAlgebra.AlgHom
 public import Mathlib.RingTheory.GradedAlgebra.Basic
+public import Mathlib.RingTheory.GradedAlgebra.Connected
 public import Mathlib.RingTheory.GradedAlgebra.FiniteType
 public import Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
 public import Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
@@ -6647,6 +6650,7 @@ public import Mathlib.RingTheory.HahnSeries.Valuation
 public import Mathlib.RingTheory.Henselian
 public import Mathlib.RingTheory.HopfAlgebra.Basic
 public import Mathlib.RingTheory.HopfAlgebra.Convolution
+public import Mathlib.RingTheory.HopfAlgebra.Graded
 public import Mathlib.RingTheory.HopfAlgebra.GroupLike
 public import Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
 public import Mathlib.RingTheory.HopfAlgebra.Quotient

Mathlib/RingTheory/Bialgebra/Graded.lean

@@ -0,0 +1,134 @@
+/-
+Copyright (c) 2026 Robert Hawkins. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robert Hawkins
+-/
+module
+
+public import Mathlib.RingTheory.Bialgebra.Basic
+public import Mathlib.RingTheory.Coalgebra.Graded
+public import Mathlib.RingTheory.GradedAlgebra.Connected
+
+/-!
+# Graded bialgebras
+
+Structural lemmas about graded connected bialgebras.
+
+## Main declarations
+
+* `GradedAlgebra.IsConnected.zeroLEquiv`: for a connected graded bialgebra, the counit restricts
+  to an isomorphism `𝒜 0 ≃ₗ[R] R`.
+* `Bialgebra.comul_sub_tmul_one_mem_lower`: for `x ∈ 𝒜 n`, `Δ(x) - x ⊗ 1` has left tensor
+  factors of degree strictly less than `n`.
+
+## References
+
+* [Grinberg, D. and Reiner, V., *Hopf Algebras in Combinatorics*][grinberg-reiner-2020],
+  Exercise 1.3.20(h) and the proof of Proposition 1.4.16.
+-/
+
+public section
+
+/-! ### The degree-zero part of a connected graded bialgebra -/
+
+namespace GradedAlgebra.IsConnected
+
+variable {R A : Type*} [CommSemiring R] [Semiring A] [Bialgebra R A]
+variable {ι : Type*} [Zero ι] (𝒜 : ι → Submodule R A) [GradedAlgebra.IsConnected 𝒜]
+
+open Coalgebra
+
+/-- Every element of the degree-zero part equals its counit times the unit. -/
+theorem eq_counit_smul_one {a : A} (ha : a ∈ 𝒜 0) : a = counit (R := R) a • 1 := by
+  obtain ⟨r, rfl⟩ := Submodule.mem_span_singleton.mp (eq_span_one (𝒜 := 𝒜) ▸ ha)
+  simp
+
+/-- The degree-zero submodule of a connected graded bialgebra is canonically isomorphic to
+the base ring via the counit. -/
+@[expose] noncomputable def zeroLEquiv : 𝒜 0 ≃ₗ[R] R where
+  toFun a := counit (a : A)
+  map_add' _ _ := by simp
+  map_smul' _ _ := by simp
+  invFun r := ⟨r • 1, eq_span_one (𝒜 := 𝒜) ▸ Submodule.smul_mem _ r (Submodule.subset_span rfl)⟩
+  left_inv := fun ⟨a, ha⟩ => Subtype.ext (eq_counit_smul_one 𝒜 ha).symm
+  right_inv _ := by simp
+
+@[simp]
+theorem zeroLEquiv_apply (a : 𝒜 0) : zeroLEquiv 𝒜 a = counit (a : A) := rfl
+
+@[simp]
+theorem zeroLEquiv_symm_apply_coe (r : R) : ((zeroLEquiv 𝒜).symm r : A) = r • 1 := rfl
+
+end GradedAlgebra.IsConnected
+
+namespace Bialgebra
+
+variable {R A : Type*} [CommSemiring R] [Ring A] [Bialgebra R A]
+variable (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [GradedCoalgebra 𝒜]
+
+open Coalgebra TensorProduct
+
+/-- The counit factors through the degree-zero projection. -/
+theorem counit_eq_counit_proj_zero (a : A) :
+    counit (R := R) a = counit (GradedAlgebra.proj 𝒜 0 a) := by
+  classical
+  rw [GradedAlgebra.proj_apply]
+  conv_lhs => rw [← DirectSum.sum_support_decompose 𝒜 a, map_sum]
+  exact Finset.sum_eq_single 0
+    (fun i _ hi =>
+      GradedCoalgebra.counit_eq_zero_of_ne_zero hi (DirectSum.decompose 𝒜 a i).2)
+    (fun h => by simp [DFinsupp.notMem_support_iff.mp h])
+
+variable [GradedAlgebra.IsConnected 𝒜]
+
+/-- Under connectedness, the degree-zero projection equals `algebraMap ∘ counit`. -/
+theorem proj_zero_eq_algebraMap_comp_counit :
+    (GradedAlgebra.proj 𝒜 0 : A →ₗ[R] A) = Algebra.linearMap R A ∘ₗ counit := by
+  ext x
+  have hmem : GradedAlgebra.proj 𝒜 0 x ∈ 𝒜 0 := by
+    rw [GradedAlgebra.proj_apply]; exact SetLike.coe_mem _
+  rw [LinearMap.comp_apply, Algebra.linearMap_apply,
+    GradedAlgebra.IsConnected.eq_counit_smul_one 𝒜 hmem,
+    ← counit_eq_counit_proj_zero, ← Algebra.algebraMap_eq_smul_one]
+
+/-- Applying `id ⊗ q_0` to `Δ(x)` gives `x ⊗ 1`, where `q_0 = GradedAlgebra.proj 𝒜 0`. -/
+@[simp]
+theorem lTensor_proj_zero_comul (x : A) :
+    (LinearMap.lTensor A (GradedAlgebra.proj 𝒜 0)) (comul x) = x ⊗ₜ[R] (1 : A) := by
+  rw [proj_zero_eq_algebraMap_comp_counit, LinearMap.lTensor_comp_apply,
+    Coalgebra.lTensor_counit_comul]
+  simp
+
+/-- Applying `q_0 ⊗ id` to `Δ(x)` gives `1 ⊗ x`, where `q_0 = GradedAlgebra.proj 𝒜 0`. -/
+@[simp]
+theorem rTensor_proj_zero_comul (x : A) :
+    (LinearMap.rTensor A (GradedAlgebra.proj 𝒜 0)) (comul x) = (1 : A) ⊗ₜ[R] x := by
+  rw [proj_zero_eq_algebraMap_comp_counit, LinearMap.rTensor_comp_apply,
+    Coalgebra.rTensor_counit_comul]
+  simp
+
+/-- For `x ∈ 𝒜 n`, `Δ(x) - x ⊗ 1` lies in the part of `A ⊗ A` whose left tensor factor has degree
+strictly less than `n`. -/
+theorem comul_sub_tmul_one_mem_lower {n : ℕ} {x : A} (hx : x ∈ 𝒜 n) :
+    comul x - x ⊗ₜ[R] (1 : A) ∈
+      ⨆ (p : ℕ) (q : ℕ) (_ : p + q = n) (_ : p < n),
+        Submodule.map₂ (TensorProduct.mk R A A) (𝒜 p) (𝒜 q) := by
+  have hΔ : comul x - x ⊗ₜ[R] (1 : A) =
+      (LinearMap.id - LinearMap.lTensor A (GradedAlgebra.proj 𝒜 0) :
+        A ⊗[R] A →ₗ[R] A ⊗[R] A) (comul x) := by
+    simp only [LinearMap.sub_apply, LinearMap.id_coe, id_eq, lTensor_proj_zero_comul]
+  rw [hΔ]
+  refine apply_mem_of_mem_bigradedPart 𝒜 _ _ (fun p q hpq a ha b hb => ?_)
+    (GradedCoalgebra.comul_mem hx)
+  simp only [LinearMap.sub_apply, LinearMap.id_coe, id_eq, LinearMap.lTensor_tmul]
+  obtain rfl | hq := Nat.eq_zero_or_pos q
+  · rw [show GradedAlgebra.proj 𝒜 0 b = b from DirectSum.decompose_of_mem_same _ hb, sub_self]
+    exact zero_mem _
+  · have hqb : GradedAlgebra.proj 𝒜 0 b = 0 :=
+      DirectSum.decompose_of_mem_ne _ hb (Nat.pos_iff_ne_zero.mp hq)
+    rw [hqb, TensorProduct.tmul_zero, sub_zero]
+    exact Submodule.mem_iSup_of_mem p <| Submodule.mem_iSup_of_mem q <|
+      Submodule.mem_iSup_of_mem hpq <| Submodule.mem_iSup_of_mem (by omega) <|
+        Submodule.apply_mem_map₂ _ ha hb
+
+end Bialgebra

Mathlib/RingTheory/Coalgebra/Graded.lean

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2026 Robert Hawkins. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robert Hawkins
+-/
+module
+
+public import Mathlib.RingTheory.Coalgebra.Basic
+
+/-!
+# Graded coalgebras
+
+A coalgebra `A` over `R` is *graded* by a family of submodules `𝒜 : ι → Submodule R A` if both
+the comultiplication and counit respect the grading: `Δ(𝒜 n) ⊆ ⨆_{p+q=n} 𝒜 p ⊗ 𝒜 q` and
+`ε(𝒜 n) = 0` for `n ≠ 0`.
+
+## Main definitions
+
+* `GradedCoalgebra 𝒜`: the comultiplication and counit respect the grading `𝒜`.
+
+## Main results
+
+* `apply_mem_of_mem_bigradedPart`: a linear map out of `A ⊗[R] A` that sends each homogeneous
+  pure tensor of total degree `n` into a submodule `S` sends the whole degree-`n` part into `S`.
+  This is the bookkeeping lemma for working with `GradedCoalgebra.comul_mem`.
+-/
+
+public section
+
+open scoped TensorProduct
+
+variable {R A ι : Type*} [CommSemiring R] [AddCommMonoid A] [Module R A]
+
+/-- A linear map on `A ⊗[R] A` that carries each pure tensor `a ⊗ₜ b` with `a ∈ 𝒜 p`, `b ∈ 𝒜 q`,
+`p + q = n` into a submodule `S` carries the whole degree-`n` part `⨆_{p+q=n} 𝒜 p ⊗ 𝒜 q` into `S`.
+This is the membership companion to `GradedCoalgebra.comul_mem`. -/
+theorem apply_mem_of_mem_bigradedPart [Add ι] {M : Type*} [AddCommMonoid M] [Module R M]
+    (𝒜 : ι → Submodule R A) (f : A ⊗[R] A →ₗ[R] M) (S : Submodule R M) {n : ι}
+    (h : ∀ p q, p + q = n → ∀ a ∈ 𝒜 p, ∀ b ∈ 𝒜 q, f (a ⊗ₜ[R] b) ∈ S) {z : A ⊗[R] A}
+    (hz : z ∈ ⨆ (p : ι) (q : ι) (_ : p + q = n),
+      Submodule.map₂ (TensorProduct.mk R A A) (𝒜 p) (𝒜 q)) :
+    f z ∈ S :=
+  Submodule.mem_comap.mp <| (iSup_le fun p => iSup_le fun q => iSup_le fun hpq =>
+    Submodule.map₂_le.2 fun a ha b hb => h p q hpq a ha b hb) hz
+
+variable [Coalgebra R A] [Add ι] [Zero ι]
+
+/-- A coalgebra is *graded* by `𝒜 : ι → Submodule R A` if both the comultiplication and counit
+respect the grading: `Δ(𝒜 n) ⊆ ⨆_{p+q=n} 𝒜 p ⊗ 𝒜 q` and `ε(𝒜 n) = 0` for `n ≠ 0`. -/
+class GradedCoalgebra (𝒜 : ι → Submodule R A) : Prop where
+  /-- The comultiplication takes degree-`n` elements to the sum of `𝒜 p ⊗ 𝒜 q` over `p + q = n`. -/
+  comul_mem : ∀ {n : ι} {x : A}, x ∈ 𝒜 n →
+    Coalgebra.comul x ∈
+      ⨆ (p : ι) (q : ι) (_ : p + q = n), Submodule.map₂ (TensorProduct.mk R A A) (𝒜 p) (𝒜 q)
+  /-- The counit vanishes on elements of nonzero degree. -/
+  counit_eq_zero_of_ne_zero : ∀ {n : ι} {x : A}, n ≠ 0 → x ∈ 𝒜 n →
+    Coalgebra.counit (R := R) x = 0

Mathlib/RingTheory/GradedAlgebra/Connected.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2026 Robert Hawkins. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robert Hawkins
+-/
+module
+
+public import Mathlib.RingTheory.GradedAlgebra.Basic
+
+/-!
+# Connected graded algebras
+
+A graded algebra is *connected* if its degree-zero part is the `R`-span of the unit `1`.
+Over a field this says `𝒜 0` is one-dimensional; for a graded bialgebra it is equivalent to the
+counit restricting to an isomorphism `𝒜 0 ≃ R`.
+
+## Main definitions
+
+* `GradedAlgebra.IsConnected 𝒜`: the degree-zero part of the grading `𝒜` is spanned by `1`.
+
+## References
+
+* [Grinberg, D. and Reiner, V., *Hopf Algebras in Combinatorics*][grinberg-reiner-2020],
+  Definition 1.3.15 and Exercise 1.3.20.
+-/
+
+public section
+
+/-- A graded algebra is *connected* if its degree-zero part is spanned by the unit element
+`1 : A`. Over a field this is the statement that `𝒜 0` is one-dimensional. -/
+class GradedAlgebra.IsConnected {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
+    {ι : Type*} [Zero ι] (𝒜 : ι → Submodule R A) : Prop where
+  /-- The degree-zero part is the `R`-span of `1`. -/
+  eq_span_one : 𝒜 0 = Submodule.span R {(1 : A)}
+
+/-- An element of `A` lies in the degree-zero part of a connected grading iff it is an
+`R`-multiple of `1`. -/
+theorem GradedAlgebra.IsConnected.mem_zero_iff {R A : Type*} [CommSemiring R] [Semiring A]
+    [Algebra R A] {ι : Type*} [Zero ι] (𝒜 : ι → Submodule R A) [GradedAlgebra.IsConnected 𝒜]
+    {a : A} : a ∈ 𝒜 0 ↔ ∃ r : R, r • (1 : A) = a := by
+  rw [eq_span_one (𝒜 := 𝒜), Submodule.mem_span_singleton]