diff --git a/Mathlib.lean b/Mathlib.lean index c1d24ccd4a4ae3..42f45fcef88ce1 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/RingTheory/Bialgebra/Graded.lean b/Mathlib/RingTheory/Bialgebra/Graded.lean new file mode 100644 index 00000000000000..9122b6830d92c8 --- /dev/null +++ b/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 diff --git a/Mathlib/RingTheory/Coalgebra/Graded.lean b/Mathlib/RingTheory/Coalgebra/Graded.lean new file mode 100644 index 00000000000000..d20ef09cd942f6 --- /dev/null +++ b/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 diff --git a/Mathlib/RingTheory/GradedAlgebra/Connected.lean b/Mathlib/RingTheory/GradedAlgebra/Connected.lean new file mode 100644 index 00000000000000..be7b3fcbbfc7fa --- /dev/null +++ b/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] diff --git a/Mathlib/RingTheory/HopfAlgebra/Graded.lean b/Mathlib/RingTheory/HopfAlgebra/Graded.lean new file mode 100644 index 00000000000000..ca793df1f03cf1 --- /dev/null +++ b/Mathlib/RingTheory/HopfAlgebra/Graded.lean @@ -0,0 +1,210 @@ +/- +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.Algebra.Ring.GeomSum +public import Mathlib.RingTheory.Bialgebra.Graded +public import Mathlib.RingTheory.Coalgebra.Convolution +public import Mathlib.RingTheory.HopfAlgebra.Basic + +/-! +# Graded connected bialgebras are Hopf algebras + +Every connected graded bialgebra admits an antipode, given by Takeuchi's formula. + +## Main declarations + +* `HopfAlgebra.takeuchiAntipode`: the antipode of a connected graded bialgebra, defined on `๐’œ n` + as the truncated Takeuchi series `โˆ‘_{k=0}^{n} (-(id - uฮต))^k` in the convolution algebra. +* `HopfAlgebra.ofGradedConnected`: every connected graded bialgebra is a Hopf algebra. + +## TODO + +* Show that `takeuchiAntipode` is a graded map. + +## References + +* [Grinberg, D. and Reiner, V., *Hopf Algebras in Combinatorics*][grinberg-reiner-2020], + Proposition 1.4.16 (existence) and Proposition 1.4.24 (Takeuchi's formula). +-/ + +public section + +namespace HopfAlgebra + +open Coalgebra DirectSum LinearMap TensorProduct WithConv + +variable {R A : Type*} [CommSemiring R] [Ring A] [Bialgebra R A] + +/-! ### The Takeuchi element and its partial geometric series in `WithConv` -/ + +/-- The element `id - uฮต = toConv LinearMap.id - 1` of the convolution algebra +`WithConv (A โ†’โ‚—[R] A)`, whose convolution powers enter Takeuchi's antipode formula. -/ +noncomputable def takeuchiF : WithConv (A โ†’โ‚—[R] A) := toConv LinearMap.id - 1 + +/-- The truncated Takeuchi series `โˆ‘ k โˆˆ Finset.range (N + 1), (-takeuchiF) ^ k` in +`WithConv (A โ†’โ‚—[R] A)`. -/ +noncomputable def takeuchiT (N : โ„•) : WithConv (A โ†’โ‚—[R] A) := + โˆ‘ k โˆˆ Finset.range (N + 1), (-takeuchiF) ^ k + +private lemma toConv_id_eq : (toConv LinearMap.id : WithConv (A โ†’โ‚—[R] A)) = 1 - -takeuchiF := by + unfold takeuchiF; abel + +lemma takeuchiT_mul_id (N : โ„•) : + (takeuchiT N : WithConv (A โ†’โ‚—[R] A)) * toConv LinearMap.id = 1 - (-takeuchiF) ^ (N + 1) := by + rw [takeuchiT, toConv_id_eq]; exact geom_sum_mul_neg _ _ + +lemma id_mul_takeuchiT (N : โ„•) : + (toConv LinearMap.id : WithConv (A โ†’โ‚—[R] A)) * takeuchiT N = 1 - (-takeuchiF) ^ (N + 1) := by + rw [takeuchiT, toConv_id_eq]; exact mul_neg_geom_sum _ _ + +/-! ### Local nilpotence: `(g^k).ofConv` annihilates `๐’œ m` for `m < k` -/ + +section LocalNilpotence + +variable (๐’œ : โ„• โ†’ Submodule R A) [GradedCoalgebra ๐’œ] + +/-- If `g.ofConv` annihilates `๐’œ 0`, then `g^k` annihilates `๐’œ m` for `m < k`. -/ +private lemma convPow_apply_eq_zero_of_lt (g : WithConv (A โ†’โ‚—[R] A)) + (hg : โˆ€ x โˆˆ ๐’œ 0, g.ofConv x = 0) + {m k : โ„•} (hmk : m < k) {x : A} (hx : x โˆˆ ๐’œ m) : + (g ^ k).ofConv x = 0 := by + induction k generalizing m x with + | zero => omega + | succ k' ih => + rw [pow_succ', convMul_apply] + suffices h : (TensorProduct.map g.ofConv (g^k').ofConv) (comul x) = 0 by + rw [h, map_zero] + refine (Submodule.mem_bot R).mp <| + apply_mem_of_mem_bigradedPart ๐’œ _ โŠฅ (fun p q hpq a ha b hb => ?_) + (GradedCoalgebra.comul_mem hx) + rw [Submodule.mem_bot, TensorProduct.map_tmul] + obtain rfl | hp := Nat.eq_zero_or_pos p + ยท rw [hg a ha, TensorProduct.zero_tmul] + ยท rw [ih (show q < k' by omega) hb, TensorProduct.tmul_zero] + +end LocalNilpotence + +/-! ### The Takeuchi antipode and its axioms -/ + +section Connected + +variable (๐’œ : โ„• โ†’ Submodule R A) + +open Bialgebra + +section +variable [GradedAlgebra.IsConnected ๐’œ] [GradedCoalgebra ๐’œ] + +/-- `(-takeuchiF) ^ k` annihilates `๐’œ m` for `m < k`. The case `k = 1` is connectedness: the +Takeuchi element `id - uฮต` vanishes on `๐’œ 0`. -/ +private lemma neg_takeuchiF_pow_apply_of_mem {m k : โ„•} (hmk : m < k) {x : A} (hx : x โˆˆ ๐’œ m) : + ((-takeuchiF (R := R)) ^ k).ofConv x = 0 := by + refine convPow_apply_eq_zero_of_lt ๐’œ _ (fun x hx => ?_) hmk hx + change -(x - algebraMap R A (counit x)) = 0 + rw [Algebra.algebraMap_eq_smul_one, + โ† GradedAlgebra.IsConnected.eq_counit_smul_one (๐’œ := ๐’œ) hx, sub_self, neg_zero] + +end + +section +variable [DirectSum.Decomposition ๐’œ] + +/-- The Takeuchi antipode: on `๐’œ n` it equals `(takeuchiT n).ofConv`, extended to all of `A` via +the direct-sum decomposition `A โ‰ƒ โจ n, ๐’œ n`. -/ +noncomputable def takeuchiAntipode : A โ†’โ‚—[R] A := + (toModule R โ„• A + (fun n => ((takeuchiT n).ofConv).comp (๐’œ n).subtype)).comp + (decomposeLinearEquiv ๐’œ).toLinearMap + +/-- On `๐’œ m`, the antipode equals `(takeuchiT m).ofConv`. -/ +lemma takeuchiAntipode_apply_of_mem {m : โ„•} {a : A} (ha : a โˆˆ ๐’œ m) : + takeuchiAntipode ๐’œ a = (takeuchiT (R := R) m).ofConv a := by + simp [takeuchiAntipode, decomposeLinearEquiv_apply_coe (โ„ณ := ๐’œ) m โŸจa, haโŸฉ] + +end + +section +variable [GradedAlgebra ๐’œ] [GradedCoalgebra ๐’œ] [GradedAlgebra.IsConnected ๐’œ] + +/-- On `๐’œ m`, the antipode equals `(takeuchiT N).ofConv` for any `N โ‰ฅ m`: the truncated series +stabilizes once `N โ‰ฅ m`, since `(-takeuchiF) ^ k` kills `๐’œ m` for every `k > m`. -/ +private lemma takeuchiAntipode_apply_eq_takeuchiT_of_le {m N : โ„•} (hmN : m โ‰ค N) + {a : A} (ha : a โˆˆ ๐’œ m) : + takeuchiAntipode ๐’œ a = (takeuchiT (R := R) N).ofConv a := by + simp only [takeuchiAntipode_apply_of_mem ๐’œ ha, takeuchiT, WithConv.ofConv_sum, + LinearMap.sum_apply] + refine Finset.sum_subset (Finset.range_mono (Nat.succ_le_succ hmN)) fun k _ hk => ?_ + rw [Finset.mem_range, not_lt] at hk + exact neg_takeuchiF_pow_apply_of_mem ๐’œ (Nat.lt_of_succ_le hk) ha + +/-- Agreement of the piecewise antipode and the uniform truncation on the image of `comul x` +via `rTensor` (controlling the left factor's degree). -/ +private lemma takeuchiAntipode_rTensor_comul_eq {n : โ„•} {x : A} (hx : x โˆˆ ๐’œ n) : + ((takeuchiAntipode ๐’œ).rTensor A) (comul x) = + (((takeuchiT n).ofConv).rTensor A) (comul x) := by + refine sub_eq_zero.mp <| (Submodule.mem_bot R).mp <| + apply_mem_of_mem_bigradedPart ๐’œ + ((takeuchiAntipode ๐’œ).rTensor A - ((takeuchiT n).ofConv).rTensor A) โŠฅ + (fun p q hpq a ha b hb => (Submodule.mem_bot R).mpr ?_) (GradedCoalgebra.comul_mem hx) + simp [takeuchiAntipode_apply_eq_takeuchiT_of_le ๐’œ (show p โ‰ค n by omega) ha] + +/-- Agreement on the image of `comul x` via `lTensor` (controlling the right factor's degree). -/ +private lemma takeuchiAntipode_lTensor_comul_eq {n : โ„•} {x : A} (hx : x โˆˆ ๐’œ n) : + ((takeuchiAntipode ๐’œ).lTensor A) (comul x) = + (((takeuchiT n).ofConv).lTensor A) (comul x) := by + refine sub_eq_zero.mp <| (Submodule.mem_bot R).mp <| + apply_mem_of_mem_bigradedPart ๐’œ + ((takeuchiAntipode ๐’œ).lTensor A - ((takeuchiT n).ofConv).lTensor A) โŠฅ + (fun p q hpq a ha b hb => (Submodule.mem_bot R).mpr ?_) (GradedCoalgebra.comul_mem hx) + simp [takeuchiAntipode_apply_eq_takeuchiT_of_le ๐’œ (show q โ‰ค n by omega) hb] + +/-- Right antipode axiom for `takeuchiAntipode`. -/ +theorem takeuchiAntipode_mul_rTensor_comul : + mul' R A โˆ˜โ‚— (takeuchiAntipode ๐’œ).rTensor A โˆ˜โ‚— comul = Algebra.linearMap R A โˆ˜โ‚— counit := by + ext x + refine Decomposition.inductionOn (โ„ณ := ๐’œ) ?_ ?_ ?_ x + ยท simp + ยท rintro i โŸจa, haโŸฉ + change mul' R A (((takeuchiAntipode ๐’œ).rTensor A) (comul a)) = algebraMap R A (counit a) + rw [takeuchiAntipode_rTensor_comul_eq ๐’œ ha] + change ((takeuchiT i * toConv LinearMap.id : + WithConv (A โ†’โ‚—[R] A))).ofConv a = algebraMap R A (counit a) + rw [takeuchiT_mul_id, WithConv.ofConv_sub, LinearMap.sub_apply, + neg_takeuchiF_pow_apply_of_mem ๐’œ (Nat.lt_succ_self i) ha, sub_zero, convOne_apply] + ยท intro yโ‚ yโ‚‚ hโ‚ hโ‚‚ + simp only [comp_apply, map_add, hโ‚, hโ‚‚] + +/-- Left antipode axiom for `takeuchiAntipode`. -/ +theorem takeuchiAntipode_mul_lTensor_comul : + mul' R A โˆ˜โ‚— (takeuchiAntipode ๐’œ).lTensor A โˆ˜โ‚— comul = Algebra.linearMap R A โˆ˜โ‚— counit := by + ext x + refine Decomposition.inductionOn (โ„ณ := ๐’œ) ?_ ?_ ?_ x + ยท simp + ยท rintro i โŸจa, haโŸฉ + change mul' R A (((takeuchiAntipode ๐’œ).lTensor A) (comul a)) = algebraMap R A (counit a) + rw [takeuchiAntipode_lTensor_comul_eq ๐’œ ha] + change ((toConv LinearMap.id * takeuchiT i : + WithConv (A โ†’โ‚—[R] A))).ofConv a = algebraMap R A (counit a) + rw [id_mul_takeuchiT, WithConv.ofConv_sub, LinearMap.sub_apply, + neg_takeuchiF_pow_apply_of_mem ๐’œ (Nat.lt_succ_self i) ha, sub_zero, convOne_apply] + ยท intro yโ‚ yโ‚‚ hโ‚ hโ‚‚ + simp only [comp_apply, map_add, hโ‚, hโ‚‚] + +/-! ### Assembling the Hopf algebra structure -/ + +/-- Every connected graded bialgebra carries a Hopf algebra structure, with antipode given by +Takeuchi's formula. -/ +noncomputable abbrev ofGradedConnected : HopfAlgebra R A where + antipode := takeuchiAntipode ๐’œ + mul_antipode_rTensor_comul := takeuchiAntipode_mul_rTensor_comul ๐’œ + mul_antipode_lTensor_comul := takeuchiAntipode_mul_lTensor_comul ๐’œ + +end + +end Connected + +end HopfAlgebra diff --git a/docs/references.bib b/docs/references.bib index 5a22b39d8fdf62..1b71839a4c1288 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -2659,6 +2659,15 @@ @Article{ Grillet-1969b doi = {10.1090/S0002-9947-1969-0237688-1} } +@Misc{ grinberg-reiner-2020, + author = {Grinberg, Darij and Reiner, Victor}, + title = {{Hopf} algebras in combinatorics}, + year = {2020}, + eprint = {1409.8356v7}, + archiveprefix = {arXiv}, + url = {https://arxiv.org/abs/1409.8356} +} + @Unpublished{ grinberg_clifford_2016, title = {The {Clifford} algebra and the {Chevalley} map- a computational approach (summary version 1)},