From 6d4337e138ee7454b521f6429d6429a3c8a0619f Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Wed, 3 Jun 2026 17:47:51 -0700 Subject: [PATCH 01/17] feat(RingTheory/HopfAlgebra): construction on primitive elements --- Mathlib.lean | 3 + Mathlib/RingTheory/Bialgebra/Primitive.lean | 101 +++++++++++++++ .../RingTheory/HopfAlgebra/Generators.lean | 120 ++++++++++++++++++ Mathlib/RingTheory/HopfAlgebra/Primitive.lean | 57 +++++++++ 4 files changed, 281 insertions(+) create mode 100644 Mathlib/RingTheory/Bialgebra/Primitive.lean create mode 100644 Mathlib/RingTheory/HopfAlgebra/Generators.lean create mode 100644 Mathlib/RingTheory/HopfAlgebra/Primitive.lean diff --git a/Mathlib.lean b/Mathlib.lean index 25ef1231b72dbe..ae053e64413dc0 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -6398,6 +6398,7 @@ public import Mathlib.RingTheory.Bialgebra.Equiv public import Mathlib.RingTheory.Bialgebra.GroupLike public import Mathlib.RingTheory.Bialgebra.Hom public import Mathlib.RingTheory.Bialgebra.MonoidAlgebra +public import Mathlib.RingTheory.Bialgebra.Primitive public import Mathlib.RingTheory.Bialgebra.SymmetricAlgebra public import Mathlib.RingTheory.Bialgebra.TensorProduct public import Mathlib.RingTheory.Binomial @@ -6551,8 +6552,10 @@ public import Mathlib.RingTheory.HahnSeries.Summable public import Mathlib.RingTheory.HahnSeries.Valuation public import Mathlib.RingTheory.Henselian public import Mathlib.RingTheory.HopfAlgebra.Basic +public import Mathlib.RingTheory.HopfAlgebra.Generators public import Mathlib.RingTheory.HopfAlgebra.GroupLike public import Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra +public import Mathlib.RingTheory.HopfAlgebra.Primitive public import Mathlib.RingTheory.HopfAlgebra.TensorProduct public import Mathlib.RingTheory.HopkinsLevitzki public import Mathlib.RingTheory.Ideal.AssociatedPrime.Basic diff --git a/Mathlib/RingTheory/Bialgebra/Primitive.lean b/Mathlib/RingTheory/Bialgebra/Primitive.lean new file mode 100644 index 00000000000000..053d949af4a73e --- /dev/null +++ b/Mathlib/RingTheory/Bialgebra/Primitive.lean @@ -0,0 +1,101 @@ +/- +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.Hom + +/-! +# Primitive elements in a bialgebra + +This file defines primitive elements in a bialgebra, i.e. elements `a` such that +`Δ a = a ⊗ₜ 1 + 1 ⊗ₜ a` and `ε a = 0`. + +## Main declarations + +* `IsPrimitiveElem R a`: `a` is a primitive element of the `R`-bialgebra. +* `primitiveSubmodule R A`: The submodule of primitive elements of `A`. + +## TODO + +* `primitiveSubmodule` is a `LieSubalgebra` with bracket `[a, b] = a * b - b * a`. +* In characteristic 0 over a field, the primitive elements of a cocommutative connected + bialgebra generate it as the universal enveloping of a Lie algebra. +-/ + +public section + +open Bialgebra Coalgebra TensorProduct Algebra.TensorProduct + +variable {F R A B : Type*} + +section Semiring +variable [CommSemiring R] [Semiring A] [Bialgebra R A] [Semiring B] [Bialgebra R B] {a b : A} + +variable (R) in +/-- An element `a` of a bialgebra is *primitive* if `Δ a = a ⊗ₜ 1 + 1 ⊗ₜ a` and `ε a = 0`. -/ +@[mk_iff] +structure IsPrimitiveElem (a : A) : Prop where + /-- A primitive element `a` satisfies `ε(a) = 0`. -/ + counit_eq_zero : counit (R := R) a = 0 + /-- A primitive element `a` satisfies `Δ(a) = a ⊗ₜ 1 + 1 ⊗ₜ a`. -/ + comul_eq_tmul_add_tmul : comul a = a ⊗ₜ[R] 1 + 1 ⊗ₜ[R] a + +attribute [simp] IsPrimitiveElem.counit_eq_zero IsPrimitiveElem.comul_eq_tmul_add_tmul + +/-- In a bialgebra, `0` is a primitive element. -/ +lemma IsPrimitiveElem.zero : IsPrimitiveElem R (0 : A) where + counit_eq_zero := map_zero _ + comul_eq_tmul_add_tmul := by simp + +/-- Primitive elements in a bialgebra are stable under addition. -/ +lemma IsPrimitiveElem.add (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) : + IsPrimitiveElem R (a + b) where + counit_eq_zero := by simp [ha, hb] + comul_eq_tmul_add_tmul := by simp [ha, hb, add_tmul, tmul_add]; abel + +/-- Primitive elements in a bialgebra are stable under scalar multiplication. -/ +lemma IsPrimitiveElem.smul (ha : IsPrimitiveElem R a) (r : R) : IsPrimitiveElem R (r • a) where + counit_eq_zero := by simp [ha] + comul_eq_tmul_add_tmul := by simp [ha, smul_add, smul_tmul'] + +/-- A bialgebra homomorphism sends primitive elements to primitive elements. -/ +lemma IsPrimitiveElem.map [FunLike F A B] [BialgHomClass F R A B] (f : F) + (ha : IsPrimitiveElem R a) : IsPrimitiveElem R (f a) where + counit_eq_zero := by simp [ha] + comul_eq_tmul_add_tmul := by rw [← CoalgHomClass.map_comp_comul_apply]; simp [ha] + +variable (R A) in +/-- The primitive elements form a submodule. -/ +def primitiveSubmodule : Submodule R A where + carrier := {a | IsPrimitiveElem R a} + add_mem' := .add + zero_mem' := .zero + smul_mem' r _ ha := ha.smul r + +@[simp] lemma mem_primitiveSubmodule : a ∈ primitiveSubmodule R A ↔ IsPrimitiveElem R a := Iff.rfl + +end Semiring + +section Ring +variable [CommSemiring R] [Ring A] [Bialgebra R A] {a b : A} + +/-- Primitive elements in a bialgebra are stable under negation. -/ +lemma IsPrimitiveElem.neg (ha : IsPrimitiveElem R a) : IsPrimitiveElem R (-a) where + counit_eq_zero := by simpa [ha, neg_add_cancel] using (map_add (counit (R := R)) (-a) a).symm + comul_eq_tmul_add_tmul := by rw [map_neg, ha.comul_eq_tmul_add_tmul, neg_add, neg_tmul, tmul_neg] + +/-- Primitive elements in a bialgebra are stable under subtraction. -/ +lemma IsPrimitiveElem.sub (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) : + IsPrimitiveElem R (a - b) := sub_eq_add_neg a b ▸ ha.add hb.neg + +/-- The commutator `[a, b] = a * b - b * a` of two primitive elements is primitive. -/ +lemma IsPrimitiveElem.commutator (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) : + IsPrimitiveElem R (a * b - b * a) where + counit_eq_zero := by + simpa [ha, hb, sub_add_cancel] using (map_add (counit (R := R)) (a * b - b * a) (b * a)).symm + comul_eq_tmul_add_tmul := by simp [ha, hb, add_mul, mul_add, sub_tmul, tmul_sub]; abel + +end Ring diff --git a/Mathlib/RingTheory/HopfAlgebra/Generators.lean b/Mathlib/RingTheory/HopfAlgebra/Generators.lean new file mode 100644 index 00000000000000..fc479f8aba5324 --- /dev/null +++ b/Mathlib/RingTheory/HopfAlgebra/Generators.lean @@ -0,0 +1,120 @@ +/- +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.Convolution +public import Mathlib.RingTheory.HopfAlgebra.Basic + +/-! +# Constructing Hopf algebras from algebra generators + +This file provides a constructor for Hopf algebras given antimultiplicative +antipode data on an algebra-generating set, via an extension principle for +pointwise convolution inverses of multiplicative maps. + +## Main declarations + +* `HopfAlgebra.ofGenerators` : construct a Hopf algebra from data on a generating set. +* `HopfAlgebra.convMul_eq_one_of_adjoin_eq_top_left` and + `convMul_eq_one_of_adjoin_eq_top_right`: the extension principle promoting a pointwise + one-sided convolution inverse of a multiplicative map on generators to a global one. +-/ + +public section + +namespace HopfAlgebra + +open Coalgebra LinearMap WithConv + +variable {R A B : Type*} [CommSemiring R] + +section ExtensionPrinciple + +/-! ### Extension principle from algebra generators -/ + +variable [Semiring A] [Bialgebra R A] [Semiring B] [Algebra R B] + {g f : A →ₗ[R] B} {s : Set A} + +/-- If a unital antimultiplicative map `g` and a unital multiplicative map `f` satisfy +`toConv g * toConv f = 1` pointwise on an algebra-generating set, then they do so globally: +a left convolution inverse on generators is a left convolution inverse. -/ +theorem convMul_eq_one_of_adjoin_eq_top_left + (g_one : g 1 = 1) (g_mul : ∀ x y, g (x * y) = g y * g x) + (f_one : f 1 = 1) (f_mul : ∀ x y, f (x * y) = f x * f y) + (adjoin_eq_top : Algebra.adjoin R s = ⊤) + (g_convMul_f : ∀ p ∈ s, (toConv g * toConv f) p = (1 : WithConv (A →ₗ[R] B)) p) : + toConv g * toConv f = 1 := by + refine WithConv.ext (ext fun x => ?_) + refine Algebra.adjoin_induction g_convMul_f + (fun r => by simp [g_one, f_one, Algebra.algebraMap_eq_smul_one, Algebra.TensorProduct.one_def]) + (fun a b _ _ ha hb => by simp [map_add, ha, hb]) + (fun a b _ _ ha hb => ?_) (adjoin_eq_top ▸ Algebra.mem_top : x ∈ Algebra.adjoin R s) + let 𝓡a := ℛ R a; let 𝓡b := ℛ R b + simp only [𝓡a.convMul_apply, 𝓡b.convMul_apply, convOne_apply] at ha hb + rw [convOne_apply] + calc (toConv g * toConv f) (a * b) + _ = ∑ p ∈ 𝓡a.index, ∑ q ∈ 𝓡b.index, + g (𝓡a.left p * 𝓡b.left q) * f (𝓡a.right p * 𝓡b.right q) := by + simp [← 𝓡a.eq, ← 𝓡b.eq, Finset.sum_mul_sum] + _ = ∑ p ∈ 𝓡a.index, ∑ q ∈ 𝓡b.index, + g (𝓡b.left q) * (g (𝓡a.left p) * f (𝓡a.right p)) * f (𝓡b.right q) := by + simp_rw [g_mul, f_mul, mul_assoc] + _ = ∑ q ∈ 𝓡b.index, algebraMap R B (counit a) * g (𝓡b.left q) * f (𝓡b.right q) := by + rw [Finset.sum_comm]; simp_rw [← Finset.sum_mul, ← Finset.mul_sum, ha, ← Algebra.commutes] + _ = algebraMap R B (counit (a * b)) := by + simp_rw [mul_assoc, ← Finset.mul_sum, hb, ← map_mul, ← Bialgebra.counit_mul] + +/-- Analogue of `convMul_eq_one_of_adjoin_eq_top_left` for `toConv f * toConv g = 1`: +a right convolution inverse on generators is a right convolution inverse. -/ +theorem convMul_eq_one_of_adjoin_eq_top_right + (g_one : g 1 = 1) (g_mul : ∀ x y, g (x * y) = g y * g x) + (f_one : f 1 = 1) (f_mul : ∀ x y, f (x * y) = f x * f y) + (adjoin_eq_top : Algebra.adjoin R s = ⊤) + (f_convMul_g : ∀ p ∈ s, (toConv f * toConv g) p = (1 : WithConv (A →ₗ[R] B)) p) : + toConv f * toConv g = 1 := by + refine WithConv.ext (ext fun x => ?_) + refine Algebra.adjoin_induction f_convMul_g + (fun r => by simp [g_one, f_one, Algebra.algebraMap_eq_smul_one, Algebra.TensorProduct.one_def]) + (fun a b _ _ ha hb => by simp [map_add, ha, hb]) + (fun a b _ _ ha hb => ?_) (adjoin_eq_top ▸ Algebra.mem_top : x ∈ Algebra.adjoin R s) + let 𝓡a := ℛ R a; let 𝓡b := ℛ R b + simp only [𝓡a.convMul_apply, 𝓡b.convMul_apply, convOne_apply] at ha hb + rw [convOne_apply] + calc (toConv f * toConv g) (a * b) + _ = ∑ p ∈ 𝓡a.index, ∑ q ∈ 𝓡b.index, + f (𝓡a.left p * 𝓡b.left q) * g (𝓡a.right p * 𝓡b.right q) := by + simp [← 𝓡a.eq, ← 𝓡b.eq, Finset.sum_mul_sum] + _ = ∑ p ∈ 𝓡a.index, ∑ q ∈ 𝓡b.index, + f (𝓡a.left p) * (f (𝓡b.left q) * g (𝓡b.right q)) * g (𝓡a.right p) := by + simp_rw [g_mul, f_mul, mul_assoc] + _ = ∑ p ∈ 𝓡a.index, algebraMap R B (counit b) * f (𝓡a.left p) * g (𝓡a.right p) := by + simp_rw [← Finset.sum_mul, ← Finset.mul_sum, hb, ← Algebra.commutes] + _ = algebraMap R B (counit (a * b)) := by + simp_rw [mul_assoc, ← Finset.mul_sum, ha, ← map_mul, mul_comm (counit b), + ← Bialgebra.counit_mul] + +end ExtensionPrinciple + +variable [Semiring A] [Bialgebra R A] {S₀ : A →ₗ[R] A} {s : Set A} + +variable (S₀) in +/-- Upgrade a bialgebra to a Hopf algebra from a unital antimultiplicative candidate antipode +that is a two-sided convolution inverse of the identity pointwise on an algebra-generating +set. -/ +noncomputable abbrev ofGenerators (S₀_one : S₀ 1 = 1) (S₀_mul : ∀ x y, S₀ (x * y) = S₀ y * S₀ x) + (adjoin_eq_top : Algebra.adjoin R s = ⊤) + (S₀_convMul_id : ∀ p ∈ s, + (toConv S₀ * toConv (.id : A →ₗ[R] A)) p = (1 : WithConv (A →ₗ[R] A)) p) + (id_convMul_S₀ : ∀ p ∈ s, + (toConv (.id : A →ₗ[R] A) * toConv S₀) p = (1 : WithConv (A →ₗ[R] A)) p) : + HopfAlgebra R A := + ofConvInverse S₀ + (convMul_eq_one_of_adjoin_eq_top_left S₀_one S₀_mul rfl (fun _ _ => rfl) + adjoin_eq_top S₀_convMul_id) + (convMul_eq_one_of_adjoin_eq_top_right S₀_one S₀_mul rfl (fun _ _ => rfl) + adjoin_eq_top id_convMul_S₀) + +end HopfAlgebra diff --git a/Mathlib/RingTheory/HopfAlgebra/Primitive.lean b/Mathlib/RingTheory/HopfAlgebra/Primitive.lean new file mode 100644 index 00000000000000..eec817d1ac47ca --- /dev/null +++ b/Mathlib/RingTheory/HopfAlgebra/Primitive.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.Bialgebra.Primitive +public import Mathlib.RingTheory.HopfAlgebra.Generators + +/-! +# Primitive elements in a Hopf algebra + +Facts about primitive elements in a Hopf algebra, plus `HopfAlgebra.ofPrimitives`, +a constructor for Hopf algebras generated as algebras by primitive elements. + +## Main declarations + +* `IsPrimitiveElem.antipode_eq_neg` : the antipode sends primitive elements to their negation. +* `IsPrimitiveElem.antipode` : the antipode preserves primitivity. +* `HopfAlgebra.ofPrimitives` : construct a Hopf algebra from a primitive-element generating set. +-/ + +public section + +open HopfAlgebra LinearMap MulOpposite + +variable {R A : Type*} [CommSemiring R] + +section Ring +variable [Ring A] [HopfAlgebra R A] {a : A} + +/-- The antipode of a Hopf algebra sends primitive elements to their negation. -/ +@[simp] theorem IsPrimitiveElem.antipode_eq_neg (ha : IsPrimitiveElem R a) : antipode R a = -a := + eq_neg_of_add_eq_zero_left <| by + simpa [ha] using mul_antipode_rTensor_comul_apply (R := R) a + +/-- The antipode preserves primitivity. -/ +protected lemma IsPrimitiveElem.antipode (ha : IsPrimitiveElem R a) : + IsPrimitiveElem R (antipode R a) := ha.antipode_eq_neg ▸ ha.neg + +end Ring + +namespace HopfAlgebra + +/-- Upgrade a bialgebra generated by primitive elements to a Hopf algebra by specifying the +antipode-on-generators formula `S p = op (-p)`. -/ +noncomputable abbrev ofPrimitives [Ring A] [Bialgebra R A] (S : A →ₐ[R] Aᵐᵒᵖ) {s : Set A} + (adjoin_eq_top : Algebra.adjoin R s = ⊤) + (prim : ∀ p ∈ s, IsPrimitiveElem R p) + (S_apply : ∀ p ∈ s, S p = op (-p)) : + HopfAlgebra R A := by + refine ofGenerators ((opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap) + (by simp) (fun _ _ => by simp) adjoin_eq_top ?_ ?_ <;> + exact fun p hp => by simp [convMul_apply, prim p hp, S_apply p hp] + +end HopfAlgebra From 3bd51994c4d63baafb22ac51764470bf6a8e406b Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Sun, 7 Jun 2026 14:19:27 -0700 Subject: [PATCH 02/17] chore(RingTheory): golf IsPrimitiveElem counit and antipode proofs --- Mathlib/RingTheory/Bialgebra/Primitive.lean | 5 ++--- Mathlib/RingTheory/HopfAlgebra/Primitive.lean | 5 ++--- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/Mathlib/RingTheory/Bialgebra/Primitive.lean b/Mathlib/RingTheory/Bialgebra/Primitive.lean index 053d949af4a73e..4ad0247d4d1352 100644 --- a/Mathlib/RingTheory/Bialgebra/Primitive.lean +++ b/Mathlib/RingTheory/Bialgebra/Primitive.lean @@ -84,7 +84,7 @@ variable [CommSemiring R] [Ring A] [Bialgebra R A] {a b : A} /-- Primitive elements in a bialgebra are stable under negation. -/ lemma IsPrimitiveElem.neg (ha : IsPrimitiveElem R a) : IsPrimitiveElem R (-a) where - counit_eq_zero := by simpa [ha, neg_add_cancel] using (map_add (counit (R := R)) (-a) a).symm + counit_eq_zero := by simpa [ha] using (map_add (counit (R := R)) (-a) a).symm comul_eq_tmul_add_tmul := by rw [map_neg, ha.comul_eq_tmul_add_tmul, neg_add, neg_tmul, tmul_neg] /-- Primitive elements in a bialgebra are stable under subtraction. -/ @@ -94,8 +94,7 @@ lemma IsPrimitiveElem.sub (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) /-- The commutator `[a, b] = a * b - b * a` of two primitive elements is primitive. -/ lemma IsPrimitiveElem.commutator (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) : IsPrimitiveElem R (a * b - b * a) where - counit_eq_zero := by - simpa [ha, hb, sub_add_cancel] using (map_add (counit (R := R)) (a * b - b * a) (b * a)).symm + counit_eq_zero := by simpa [ha] using (map_add (counit (R := R)) (a * b - b * a) (b * a)).symm comul_eq_tmul_add_tmul := by simp [ha, hb, add_mul, mul_add, sub_tmul, tmul_sub]; abel end Ring diff --git a/Mathlib/RingTheory/HopfAlgebra/Primitive.lean b/Mathlib/RingTheory/HopfAlgebra/Primitive.lean index eec817d1ac47ca..dae07c72119809 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Primitive.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Primitive.lean @@ -31,9 +31,8 @@ section Ring variable [Ring A] [HopfAlgebra R A] {a : A} /-- The antipode of a Hopf algebra sends primitive elements to their negation. -/ -@[simp] theorem IsPrimitiveElem.antipode_eq_neg (ha : IsPrimitiveElem R a) : antipode R a = -a := - eq_neg_of_add_eq_zero_left <| by - simpa [ha] using mul_antipode_rTensor_comul_apply (R := R) a +@[simp] theorem IsPrimitiveElem.antipode_eq_neg (ha : IsPrimitiveElem R a) : antipode R a = -a := by + simpa [ha, eq_neg_iff_add_eq_zero] using mul_antipode_rTensor_comul_apply (R := R) a /-- The antipode preserves primitivity. -/ protected lemma IsPrimitiveElem.antipode (ha : IsPrimitiveElem R a) : From a878464315ebd5e006249c1de9ca10859b32674b Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Sun, 7 Jun 2026 15:43:11 -0700 Subject: [PATCH 03/17] feat(RingTheory/HopfAlgebra): uniqueness of the antipode --- Mathlib/RingTheory/HopfAlgebra/Basic.lean | 7 +++++ .../RingTheory/HopfAlgebra/Generators.lean | 26 +++++++++++++++++-- Mathlib/RingTheory/HopfAlgebra/Primitive.lean | 12 +++++++++ 3 files changed, 43 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/HopfAlgebra/Basic.lean b/Mathlib/RingTheory/HopfAlgebra/Basic.lean index 0bd11d64e696c2..9ea12add0a4911 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Basic.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Basic.lean @@ -27,6 +27,8 @@ In this file we define `HopfAlgebra`, and provide instances for: * `HopfAlgebra.antipode_one` : the antipode of the unit is the unit. * `HopfAlgebra.antipode_mul` : the antipode is an antihomomorphism: `S(ab) = S(b)S(a)`. +* `HopfAlgebra.eq_antipode_of_convMul_id_eq_one` : a left convolution inverse of `id` is the + antipode. ## TODO @@ -215,6 +217,11 @@ theorem antipode_mul (a b : A) : _ = (counit (R := R) y • counit x) • (1 : A) := by simp only [smul_eq_mul, mul_comm (counit y)] +/-- A left convolution inverse of the identity is the antipode. -/ +theorem eq_antipode_of_convMul_id_eq_one {S₀ : A →ₗ[R] A} + (h : toConv S₀ * toConv LinearMap.id = 1) : S₀ = antipode R := + toConv_injective (left_inv_eq_right_inv h (WithConv.ext mul_antipode_lTensor_comul)) + end HopfAlgebra namespace CommSemiring diff --git a/Mathlib/RingTheory/HopfAlgebra/Generators.lean b/Mathlib/RingTheory/HopfAlgebra/Generators.lean index fc479f8aba5324..8c7a300ed4c79c 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Generators.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Generators.lean @@ -19,8 +19,10 @@ pointwise convolution inverses of multiplicative maps. * `HopfAlgebra.ofGenerators` : construct a Hopf algebra from data on a generating set. * `HopfAlgebra.convMul_eq_one_of_adjoin_eq_top_left` and - `convMul_eq_one_of_adjoin_eq_top_right`: the extension principle promoting a pointwise - one-sided convolution inverse of a multiplicative map on generators to a global one. + `HopfAlgebra.convMul_eq_one_of_adjoin_eq_top_right`: a pointwise one-sided convolution inverse of + a multiplicative map on generators is a global one. +* `HopfAlgebra.eq_antipode_of_adjoin_eq_top` : a left convolution inverse of `id` on a generating + set is the antipode. -/ public section @@ -98,6 +100,7 @@ theorem convMul_eq_one_of_adjoin_eq_top_right end ExtensionPrinciple +section Construction variable [Semiring A] [Bialgebra R A] {S₀ : A →ₗ[R] A} {s : Set A} variable (S₀) in @@ -117,4 +120,23 @@ noncomputable abbrev ofGenerators (S₀_one : S₀ 1 = 1) (S₀_mul : ∀ x y, S (convMul_eq_one_of_adjoin_eq_top_right S₀_one S₀_mul rfl (fun _ _ => rfl) adjoin_eq_top id_convMul_S₀) +end Construction + +section Uniqueness +variable [Semiring A] [HopfAlgebra R A] {S₀ : A →ₗ[R] A} {s : Set A} + +variable (S₀) in +/-- A unital antimultiplicative map that is a left convolution inverse of the identity on an +algebra-generating set is the antipode. -/ +theorem eq_antipode_of_adjoin_eq_top (S₀_one : S₀ 1 = 1) + (S₀_mul : ∀ x y, S₀ (x * y) = S₀ y * S₀ x) (adjoin_eq_top : Algebra.adjoin R s = ⊤) + (S₀_convMul_id : ∀ p ∈ s, + (toConv S₀ * toConv (.id : A →ₗ[R] A)) p = (1 : WithConv (A →ₗ[R] A)) p) : + S₀ = antipode R := + eq_antipode_of_convMul_id_eq_one + (convMul_eq_one_of_adjoin_eq_top_left S₀_one S₀_mul rfl (fun _ _ => rfl) + adjoin_eq_top S₀_convMul_id) + +end Uniqueness + end HopfAlgebra diff --git a/Mathlib/RingTheory/HopfAlgebra/Primitive.lean b/Mathlib/RingTheory/HopfAlgebra/Primitive.lean index dae07c72119809..0a06d2a2b9739a 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Primitive.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Primitive.lean @@ -19,6 +19,8 @@ a constructor for Hopf algebras generated as algebras by primitive elements. * `IsPrimitiveElem.antipode_eq_neg` : the antipode sends primitive elements to their negation. * `IsPrimitiveElem.antipode` : the antipode preserves primitivity. * `HopfAlgebra.ofPrimitives` : construct a Hopf algebra from a primitive-element generating set. +* `HopfAlgebra.eq_antipode_of_primitives` : the antipode is the unique anti-algebra hom negating a + primitive generating set. -/ public section @@ -53,4 +55,14 @@ noncomputable abbrev ofPrimitives [Ring A] [Bialgebra R A] (S : A →ₐ[R] Aᵐ (by simp) (fun _ _ => by simp) adjoin_eq_top ?_ ?_ <;> exact fun p hp => by simp [convMul_apply, prim p hp, S_apply p hp] +/-- On a Hopf algebra generated by primitive elements, the antipode is the unique anti-algebra hom +negating the generators. -/ +theorem eq_antipode_of_primitives [Ring A] [HopfAlgebra R A] (S : A →ₐ[R] Aᵐᵒᵖ) {s : Set A} + (adjoin_eq_top : Algebra.adjoin R s = ⊤) (prim : ∀ p ∈ s, IsPrimitiveElem R p) + (S_apply : ∀ p ∈ s, S p = op (-p)) : + (opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap = antipode R := + eq_antipode_of_adjoin_eq_top ((opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap) + (by simp) (fun _ _ => by simp) adjoin_eq_top + (fun p hp => by simp [convMul_apply, prim p hp, S_apply p hp]) + end HopfAlgebra From 3cc311f358c3274a29f278b1d757eba9f2f47307 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Wed, 24 Jun 2026 13:03:45 -0700 Subject: [PATCH 04/17] chore(RingTheory/Bialgebra): drop unused opens in Primitive --- Mathlib/RingTheory/Bialgebra/Primitive.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Bialgebra/Primitive.lean b/Mathlib/RingTheory/Bialgebra/Primitive.lean index 4ad0247d4d1352..50b16645d4c587 100644 --- a/Mathlib/RingTheory/Bialgebra/Primitive.lean +++ b/Mathlib/RingTheory/Bialgebra/Primitive.lean @@ -27,7 +27,7 @@ This file defines primitive elements in a bialgebra, i.e. elements `a` such that public section -open Bialgebra Coalgebra TensorProduct Algebra.TensorProduct +open Coalgebra TensorProduct variable {F R A B : Type*} From ce444bbf66565901fc60d5fa8a1f4fc733aa60ed Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Wed, 24 Jun 2026 13:03:45 -0700 Subject: [PATCH 05/17] refactor(RingTheory/HopfAlgebra): prove generator extension via equalizer subalgebra --- .../RingTheory/HopfAlgebra/Generators.lean | 58 ++++++++----------- 1 file changed, 25 insertions(+), 33 deletions(-) diff --git a/Mathlib/RingTheory/HopfAlgebra/Generators.lean b/Mathlib/RingTheory/HopfAlgebra/Generators.lean index 29473af38f9fce..6a8ebffee7ce99 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Generators.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Generators.lean @@ -10,13 +10,15 @@ public import Mathlib.RingTheory.HopfAlgebra.Convolution /-! # Constructing Hopf algebras from algebra generators -This file provides a constructor for Hopf algebras given antimultiplicative -antipode data on an algebra-generating set, via an extension principle for -pointwise convolution inverses of multiplicative maps. +This file provides an extension principle to upgrade a bialgebra to a Hopf algebra given +antimultiplicative antipode data on generators. -## Main declarations +## Main definitions * `HopfAlgebra.ofGenerators` : construct a Hopf algebra from data on a generating set. + +## Main results + * `HopfAlgebra.convMul_eq_one_of_adjoin_eq_top_left` and `HopfAlgebra.convMul_eq_one_of_adjoin_eq_top_right`: a pointwise one-sided convolution inverse of a multiplicative map on generators is a global one. @@ -30,7 +32,7 @@ public section namespace HopfAlgebra -open Coalgebra LinearMap WithConv +open Algebra Coalgebra LinearMap WithConv variable {R A B : Type*} [CommSemiring R] @@ -47,26 +49,21 @@ a left convolution inverse on generators is a left convolution inverse. -/ theorem convMul_eq_one_of_adjoin_eq_top_left (g_one : g 1 = 1) (g_mul : ∀ x y, g (x * y) = g y * g x) (f_one : f 1 = 1) (f_mul : ∀ x y, f (x * y) = f x * f y) - (adjoin_eq_top : Algebra.adjoin R s = ⊤) + (adjoin_eq_top : adjoin R s = ⊤) (g_convMul_f : ∀ p ∈ s, (toConv g * toConv f) p = (1 : WithConv (A →ₗ[R] B)) p) : toConv g * toConv f = 1 := by - refine WithConv.ext (ext fun x => ?_) - refine Algebra.adjoin_induction g_convMul_f - (fun r => by simp [g_one, f_one, Algebra.algebraMap_eq_smul_one, Algebra.TensorProduct.one_def]) - (fun a b _ _ ha hb => by simp [map_add, ha, hb]) - (fun a b _ _ ha hb => ?_) (adjoin_eq_top ▸ Algebra.mem_top : x ∈ Algebra.adjoin R s) + ext x; refine adjoin_le + (S := (eqLocus (toConv g * toConv f).ofConv (ofConv 1)).toSubalgebra ?_ fun a b ha hb => ?_) + g_convMul_f (adjoin_eq_top ▸ mem_top : x ∈ adjoin R s) + · simp [g_one, f_one, TensorProduct.one_def] let 𝓡a := ℛ R a; let 𝓡b := ℛ R b - simp only [𝓡a.convMul_apply, 𝓡b.convMul_apply, convOne_apply] at ha hb - rw [convOne_apply] + simp only [mem_eqLocus, 𝓡a.convMul_apply, 𝓡b.convMul_apply, convOne_apply] at ha hb ⊢ calc (toConv g * toConv f) (a * b) - _ = ∑ p ∈ 𝓡a.index, ∑ q ∈ 𝓡b.index, - g (𝓡a.left p * 𝓡b.left q) * f (𝓡a.right p * 𝓡b.right q) := by - simp [← 𝓡a.eq, ← 𝓡b.eq, Finset.sum_mul_sum] _ = ∑ p ∈ 𝓡a.index, ∑ q ∈ 𝓡b.index, g (𝓡b.left q) * (g (𝓡a.left p) * f (𝓡a.right p)) * f (𝓡b.right q) := by - simp_rw [g_mul, f_mul, mul_assoc] + simp [← 𝓡a.eq, ← 𝓡b.eq, Finset.sum_mul_sum, g_mul, f_mul, mul_assoc] _ = ∑ q ∈ 𝓡b.index, algebraMap R B (counit a) * g (𝓡b.left q) * f (𝓡b.right q) := by - rw [Finset.sum_comm]; simp_rw [← Finset.sum_mul, ← Finset.mul_sum, ha, ← Algebra.commutes] + rw [Finset.sum_comm]; simp_rw [← Finset.sum_mul, ← Finset.mul_sum, ha, ← commutes] _ = algebraMap R B (counit (a * b)) := by simp_rw [mul_assoc, ← Finset.mul_sum, hb, ← map_mul, ← Bialgebra.counit_mul] @@ -75,26 +72,21 @@ a right convolution inverse on generators is a right convolution inverse. -/ theorem convMul_eq_one_of_adjoin_eq_top_right (g_one : g 1 = 1) (g_mul : ∀ x y, g (x * y) = g y * g x) (f_one : f 1 = 1) (f_mul : ∀ x y, f (x * y) = f x * f y) - (adjoin_eq_top : Algebra.adjoin R s = ⊤) + (adjoin_eq_top : adjoin R s = ⊤) (f_convMul_g : ∀ p ∈ s, (toConv f * toConv g) p = (1 : WithConv (A →ₗ[R] B)) p) : toConv f * toConv g = 1 := by - refine WithConv.ext (ext fun x => ?_) - refine Algebra.adjoin_induction f_convMul_g - (fun r => by simp [g_one, f_one, Algebra.algebraMap_eq_smul_one, Algebra.TensorProduct.one_def]) - (fun a b _ _ ha hb => by simp [map_add, ha, hb]) - (fun a b _ _ ha hb => ?_) (adjoin_eq_top ▸ Algebra.mem_top : x ∈ Algebra.adjoin R s) + ext x; refine adjoin_le + (S := (eqLocus (toConv f * toConv g).ofConv (ofConv 1)).toSubalgebra ?_ fun a b ha hb => ?_) + f_convMul_g (adjoin_eq_top ▸ mem_top : x ∈ adjoin R s) + · simp [g_one, f_one, TensorProduct.one_def] let 𝓡a := ℛ R a; let 𝓡b := ℛ R b - simp only [𝓡a.convMul_apply, 𝓡b.convMul_apply, convOne_apply] at ha hb - rw [convOne_apply] + simp only [mem_eqLocus, 𝓡a.convMul_apply, 𝓡b.convMul_apply, convOne_apply] at ha hb ⊢ calc (toConv f * toConv g) (a * b) - _ = ∑ p ∈ 𝓡a.index, ∑ q ∈ 𝓡b.index, - f (𝓡a.left p * 𝓡b.left q) * g (𝓡a.right p * 𝓡b.right q) := by - simp [← 𝓡a.eq, ← 𝓡b.eq, Finset.sum_mul_sum] _ = ∑ p ∈ 𝓡a.index, ∑ q ∈ 𝓡b.index, f (𝓡a.left p) * (f (𝓡b.left q) * g (𝓡b.right q)) * g (𝓡a.right p) := by - simp_rw [g_mul, f_mul, mul_assoc] + simp [← 𝓡a.eq, ← 𝓡b.eq, Finset.sum_mul_sum, g_mul, f_mul, mul_assoc] _ = ∑ p ∈ 𝓡a.index, algebraMap R B (counit b) * f (𝓡a.left p) * g (𝓡a.right p) := by - simp_rw [← Finset.sum_mul, ← Finset.mul_sum, hb, ← Algebra.commutes] + simp_rw [← Finset.sum_mul, ← Finset.mul_sum, hb, ← commutes] _ = algebraMap R B (counit (a * b)) := by simp_rw [mul_assoc, ← Finset.mul_sum, ha, ← map_mul, mul_comm (counit b), ← Bialgebra.counit_mul] @@ -109,7 +101,7 @@ variable (S₀) in that is a two-sided convolution inverse of the identity pointwise on an algebra-generating set. -/ noncomputable abbrev ofGenerators (S₀_one : S₀ 1 = 1) (S₀_mul : ∀ x y, S₀ (x * y) = S₀ y * S₀ x) - (adjoin_eq_top : Algebra.adjoin R s = ⊤) + (adjoin_eq_top : adjoin R s = ⊤) (S₀_convMul_id : ∀ p ∈ s, (toConv S₀ * toConv (.id : A →ₗ[R] A)) p = (1 : WithConv (A →ₗ[R] A)) p) (id_convMul_S₀ : ∀ p ∈ s, @@ -135,7 +127,7 @@ variable (S₀) in /-- A unital antimultiplicative map that is a left convolution inverse of the identity on an algebra-generating set is the antipode. -/ theorem eq_antipode_of_adjoin_eq_top (S₀_one : S₀ 1 = 1) - (S₀_mul : ∀ x y, S₀ (x * y) = S₀ y * S₀ x) (adjoin_eq_top : Algebra.adjoin R s = ⊤) + (S₀_mul : ∀ x y, S₀ (x * y) = S₀ y * S₀ x) (adjoin_eq_top : adjoin R s = ⊤) (S₀_convMul_id : ∀ p ∈ s, (toConv S₀ * toConv (.id : A →ₗ[R] A)) p = (1 : WithConv (A →ₗ[R] A)) p) : S₀ = antipode R := From 9947f248043edab9d8f0b63c55cf136e9d43101c Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Wed, 24 Jun 2026 14:48:38 -0700 Subject: [PATCH 06/17] refactor(RingTheory/HopfAlgebra): merge calc rungs in generator extension --- Mathlib/RingTheory/HopfAlgebra/Generators.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Mathlib/RingTheory/HopfAlgebra/Generators.lean b/Mathlib/RingTheory/HopfAlgebra/Generators.lean index 6a8ebffee7ce99..520387fc304330 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Generators.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Generators.lean @@ -62,9 +62,8 @@ theorem convMul_eq_one_of_adjoin_eq_top_left _ = ∑ p ∈ 𝓡a.index, ∑ q ∈ 𝓡b.index, g (𝓡b.left q) * (g (𝓡a.left p) * f (𝓡a.right p)) * f (𝓡b.right q) := by simp [← 𝓡a.eq, ← 𝓡b.eq, Finset.sum_mul_sum, g_mul, f_mul, mul_assoc] - _ = ∑ q ∈ 𝓡b.index, algebraMap R B (counit a) * g (𝓡b.left q) * f (𝓡b.right q) := by - rw [Finset.sum_comm]; simp_rw [← Finset.sum_mul, ← Finset.mul_sum, ha, ← commutes] _ = algebraMap R B (counit (a * b)) := by + rw [Finset.sum_comm]; simp_rw [← Finset.sum_mul, ← Finset.mul_sum, ha, ← commutes] simp_rw [mul_assoc, ← Finset.mul_sum, hb, ← map_mul, ← Bialgebra.counit_mul] /-- Analogue of `convMul_eq_one_of_adjoin_eq_top_left` for `toConv f * toConv g = 1`: @@ -85,9 +84,8 @@ theorem convMul_eq_one_of_adjoin_eq_top_right _ = ∑ p ∈ 𝓡a.index, ∑ q ∈ 𝓡b.index, f (𝓡a.left p) * (f (𝓡b.left q) * g (𝓡b.right q)) * g (𝓡a.right p) := by simp [← 𝓡a.eq, ← 𝓡b.eq, Finset.sum_mul_sum, g_mul, f_mul, mul_assoc] - _ = ∑ p ∈ 𝓡a.index, algebraMap R B (counit b) * f (𝓡a.left p) * g (𝓡a.right p) := by - simp_rw [← Finset.sum_mul, ← Finset.mul_sum, hb, ← commutes] _ = algebraMap R B (counit (a * b)) := by + simp_rw [← Finset.sum_mul, ← Finset.mul_sum, hb, ← commutes] simp_rw [mul_assoc, ← Finset.mul_sum, ha, ← map_mul, mul_comm (counit b), ← Bialgebra.counit_mul] From c7e59604967ce82c623ce8b4399ee85d78efa6d4 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 17 Jul 2026 11:34:38 -0700 Subject: [PATCH 07/17] style(RingTheory/Bialgebra/Primitive): open IsPrimitiveElem namespace, golf proofs --- Mathlib/RingTheory/Bialgebra/Primitive.lean | 48 +++++++++++---------- 1 file changed, 25 insertions(+), 23 deletions(-) diff --git a/Mathlib/RingTheory/Bialgebra/Primitive.lean b/Mathlib/RingTheory/Bialgebra/Primitive.lean index 50b16645d4c587..bdda0a01243981 100644 --- a/Mathlib/RingTheory/Bialgebra/Primitive.lean +++ b/Mathlib/RingTheory/Bialgebra/Primitive.lean @@ -45,27 +45,25 @@ structure IsPrimitiveElem (a : A) : Prop where attribute [simp] IsPrimitiveElem.counit_eq_zero IsPrimitiveElem.comul_eq_tmul_add_tmul +namespace IsPrimitiveElem + /-- In a bialgebra, `0` is a primitive element. -/ -lemma IsPrimitiveElem.zero : IsPrimitiveElem R (0 : A) where - counit_eq_zero := map_zero _ - comul_eq_tmul_add_tmul := by simp +lemma zero : IsPrimitiveElem R (0 : A) := by simp [isPrimitiveElem_iff] /-- Primitive elements in a bialgebra are stable under addition. -/ -lemma IsPrimitiveElem.add (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) : - IsPrimitiveElem R (a + b) where - counit_eq_zero := by simp [ha, hb] - comul_eq_tmul_add_tmul := by simp [ha, hb, add_tmul, tmul_add]; abel +lemma add (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) : IsPrimitiveElem R (a + b) := + ⟨by simp [ha, hb], by simp [ha, hb, add_tmul, tmul_add]; abel⟩ /-- Primitive elements in a bialgebra are stable under scalar multiplication. -/ -lemma IsPrimitiveElem.smul (ha : IsPrimitiveElem R a) (r : R) : IsPrimitiveElem R (r • a) where - counit_eq_zero := by simp [ha] - comul_eq_tmul_add_tmul := by simp [ha, smul_add, smul_tmul'] +lemma smul (ha : IsPrimitiveElem R a) (r : R) : IsPrimitiveElem R (r • a) := + ⟨by simp [ha], by simp [ha, smul_add, smul_tmul']⟩ /-- A bialgebra homomorphism sends primitive elements to primitive elements. -/ -lemma IsPrimitiveElem.map [FunLike F A B] [BialgHomClass F R A B] (f : F) - (ha : IsPrimitiveElem R a) : IsPrimitiveElem R (f a) where - counit_eq_zero := by simp [ha] - comul_eq_tmul_add_tmul := by rw [← CoalgHomClass.map_comp_comul_apply]; simp [ha] +lemma map [FunLike F A B] [BialgHomClass F R A B] (f : F) (ha : IsPrimitiveElem R a) : + IsPrimitiveElem R (f a) := + ⟨by simp [ha], by rw [← CoalgHomClass.map_comp_comul_apply]; simp [ha]⟩ + +end IsPrimitiveElem variable (R A) in /-- The primitive elements form a submodule. -/ @@ -82,19 +80,23 @@ end Semiring section Ring variable [CommSemiring R] [Ring A] [Bialgebra R A] {a b : A} +namespace IsPrimitiveElem + /-- Primitive elements in a bialgebra are stable under negation. -/ -lemma IsPrimitiveElem.neg (ha : IsPrimitiveElem R a) : IsPrimitiveElem R (-a) where - counit_eq_zero := by simpa [ha] using (map_add (counit (R := R)) (-a) a).symm - comul_eq_tmul_add_tmul := by rw [map_neg, ha.comul_eq_tmul_add_tmul, neg_add, neg_tmul, tmul_neg] +lemma neg (ha : IsPrimitiveElem R a) : IsPrimitiveElem R (-a) := + ⟨by simpa [ha] using (map_add (counit (R := R)) (-a) a).symm, + by rw [map_neg, ha.comul_eq_tmul_add_tmul, neg_add, neg_tmul, tmul_neg]⟩ /-- Primitive elements in a bialgebra are stable under subtraction. -/ -lemma IsPrimitiveElem.sub (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) : - IsPrimitiveElem R (a - b) := sub_eq_add_neg a b ▸ ha.add hb.neg +lemma sub (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) : IsPrimitiveElem R (a - b) := + sub_eq_add_neg a b ▸ ha.add hb.neg /-- The commutator `[a, b] = a * b - b * a` of two primitive elements is primitive. -/ -lemma IsPrimitiveElem.commutator (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) : - IsPrimitiveElem R (a * b - b * a) where - counit_eq_zero := by simpa [ha] using (map_add (counit (R := R)) (a * b - b * a) (b * a)).symm - comul_eq_tmul_add_tmul := by simp [ha, hb, add_mul, mul_add, sub_tmul, tmul_sub]; abel +lemma commutator (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) : + IsPrimitiveElem R (a * b - b * a) := + ⟨by simpa [ha] using (map_add (counit (R := R)) (a * b - b * a) (b * a)).symm, + by simp [ha, hb, add_mul, mul_add, sub_tmul, tmul_sub]; abel⟩ + +end IsPrimitiveElem end Ring From 9a88ee185aaf3280c27e47fd0c933dc461c612f8 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 17 Jul 2026 11:42:29 -0700 Subject: [PATCH 08/17] style(RingTheory/Bialgebra/Primitive): dotted lemma names, golf map --- Mathlib/RingTheory/Bialgebra/Primitive.lean | 28 ++++++++------------- 1 file changed, 11 insertions(+), 17 deletions(-) diff --git a/Mathlib/RingTheory/Bialgebra/Primitive.lean b/Mathlib/RingTheory/Bialgebra/Primitive.lean index bdda0a01243981..3e52508596945b 100644 --- a/Mathlib/RingTheory/Bialgebra/Primitive.lean +++ b/Mathlib/RingTheory/Bialgebra/Primitive.lean @@ -45,25 +45,22 @@ structure IsPrimitiveElem (a : A) : Prop where attribute [simp] IsPrimitiveElem.counit_eq_zero IsPrimitiveElem.comul_eq_tmul_add_tmul -namespace IsPrimitiveElem - /-- In a bialgebra, `0` is a primitive element. -/ -lemma zero : IsPrimitiveElem R (0 : A) := by simp [isPrimitiveElem_iff] +lemma IsPrimitiveElem.zero : IsPrimitiveElem R (0 : A) := by simp [isPrimitiveElem_iff] /-- Primitive elements in a bialgebra are stable under addition. -/ -lemma add (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) : IsPrimitiveElem R (a + b) := +lemma IsPrimitiveElem.add (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) : + IsPrimitiveElem R (a + b) := ⟨by simp [ha, hb], by simp [ha, hb, add_tmul, tmul_add]; abel⟩ /-- Primitive elements in a bialgebra are stable under scalar multiplication. -/ -lemma smul (ha : IsPrimitiveElem R a) (r : R) : IsPrimitiveElem R (r • a) := +lemma IsPrimitiveElem.smul (ha : IsPrimitiveElem R a) (r : R) : IsPrimitiveElem R (r • a) := ⟨by simp [ha], by simp [ha, smul_add, smul_tmul']⟩ /-- A bialgebra homomorphism sends primitive elements to primitive elements. -/ -lemma map [FunLike F A B] [BialgHomClass F R A B] (f : F) (ha : IsPrimitiveElem R a) : - IsPrimitiveElem R (f a) := - ⟨by simp [ha], by rw [← CoalgHomClass.map_comp_comul_apply]; simp [ha]⟩ - -end IsPrimitiveElem +lemma IsPrimitiveElem.map [FunLike F A B] [BialgHomClass F R A B] (f : F) + (ha : IsPrimitiveElem R a) : IsPrimitiveElem R (f a) := + ⟨by simp [ha], by simp [ha, ← CoalgHomClass.map_comp_comul_apply]⟩ variable (R A) in /-- The primitive elements form a submodule. -/ @@ -80,23 +77,20 @@ end Semiring section Ring variable [CommSemiring R] [Ring A] [Bialgebra R A] {a b : A} -namespace IsPrimitiveElem - /-- Primitive elements in a bialgebra are stable under negation. -/ -lemma neg (ha : IsPrimitiveElem R a) : IsPrimitiveElem R (-a) := +lemma IsPrimitiveElem.neg (ha : IsPrimitiveElem R a) : IsPrimitiveElem R (-a) := ⟨by simpa [ha] using (map_add (counit (R := R)) (-a) a).symm, by rw [map_neg, ha.comul_eq_tmul_add_tmul, neg_add, neg_tmul, tmul_neg]⟩ /-- Primitive elements in a bialgebra are stable under subtraction. -/ -lemma sub (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) : IsPrimitiveElem R (a - b) := +lemma IsPrimitiveElem.sub (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) : + IsPrimitiveElem R (a - b) := sub_eq_add_neg a b ▸ ha.add hb.neg /-- The commutator `[a, b] = a * b - b * a` of two primitive elements is primitive. -/ -lemma commutator (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) : +lemma IsPrimitiveElem.commutator (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) : IsPrimitiveElem R (a * b - b * a) := ⟨by simpa [ha] using (map_add (counit (R := R)) (a * b - b * a) (b * a)).symm, by simp [ha, hb, add_mul, mul_add, sub_tmul, tmul_sub]; abel⟩ -end IsPrimitiveElem - end Ring From 78265c15d981496aee3706cd4263f481423946e6 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 17 Jul 2026 11:48:45 -0700 Subject: [PATCH 09/17] style(RingTheory/Bialgebra/Primitive): golf neg, compact sub --- Mathlib/RingTheory/Bialgebra/Primitive.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Mathlib/RingTheory/Bialgebra/Primitive.lean b/Mathlib/RingTheory/Bialgebra/Primitive.lean index 3e52508596945b..e5b64fe1ee9be5 100644 --- a/Mathlib/RingTheory/Bialgebra/Primitive.lean +++ b/Mathlib/RingTheory/Bialgebra/Primitive.lean @@ -80,12 +80,11 @@ variable [CommSemiring R] [Ring A] [Bialgebra R A] {a b : A} /-- Primitive elements in a bialgebra are stable under negation. -/ lemma IsPrimitiveElem.neg (ha : IsPrimitiveElem R a) : IsPrimitiveElem R (-a) := ⟨by simpa [ha] using (map_add (counit (R := R)) (-a) a).symm, - by rw [map_neg, ha.comul_eq_tmul_add_tmul, neg_add, neg_tmul, tmul_neg]⟩ + by simp [ha, neg_tmul, tmul_neg, add_comm]⟩ /-- Primitive elements in a bialgebra are stable under subtraction. -/ lemma IsPrimitiveElem.sub (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) : - IsPrimitiveElem R (a - b) := - sub_eq_add_neg a b ▸ ha.add hb.neg + IsPrimitiveElem R (a - b) := sub_eq_add_neg a b ▸ ha.add hb.neg /-- The commutator `[a, b] = a * b - b * a` of two primitive elements is primitive. -/ lemma IsPrimitiveElem.commutator (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) : From fb784abc654d6c770534d48a505a4d6194e90522 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 17 Jul 2026 11:56:42 -0700 Subject: [PATCH 10/17] feat(RingTheory/Bialgebra/Primitive): ne_one, map_equiv, docstring polish --- Mathlib/RingTheory/Bialgebra/Primitive.lean | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/Bialgebra/Primitive.lean b/Mathlib/RingTheory/Bialgebra/Primitive.lean index e5b64fe1ee9be5..aa0523fbe82dea 100644 --- a/Mathlib/RingTheory/Bialgebra/Primitive.lean +++ b/Mathlib/RingTheory/Bialgebra/Primitive.lean @@ -5,7 +5,7 @@ Authors: Robert Hawkins -/ module -public import Mathlib.RingTheory.Bialgebra.Hom +public import Mathlib.RingTheory.Bialgebra.Equiv /-! # Primitive elements in a bialgebra @@ -21,8 +21,12 @@ This file defines primitive elements in a bialgebra, i.e. elements `a` such that ## TODO * `primitiveSubmodule` is a `LieSubalgebra` with bracket `[a, b] = a * b - b * a`. + (`IsPrimitiveElem.commutator` is stated with `a * b - b * a` rather than `⁅a, b⁆` to avoid + importing Lie theory into this file.) * In characteristic 0 over a field, the primitive elements of a cocommutative connected bialgebra generate it as the universal enveloping of a Lie algebra. +* Generalize to `(g, h)`-skew-primitive elements `Δ a = a ⊗ₜ g + h ⊗ₜ a` for group-like `g`, `h` + over a plain coalgebra, of which primitivity is the `(1, 1)` case over a bialgebra. -/ public section @@ -35,7 +39,8 @@ section Semiring variable [CommSemiring R] [Semiring A] [Bialgebra R A] [Semiring B] [Bialgebra R B] {a b : A} variable (R) in -/-- An element `a` of a bialgebra is *primitive* if `Δ a = a ⊗ₜ 1 + 1 ⊗ₜ a` and `ε a = 0`. -/ +/-- An element `a` of a bialgebra is *primitive* if `Δ a = a ⊗ₜ 1 + 1 ⊗ₜ a` and `ε a = 0`, +where `ε` and `Δ` are the counit and comultiplication respectively. -/ @[mk_iff] structure IsPrimitiveElem (a : A) : Prop where /-- A primitive element `a` satisfies `ε(a) = 0`. -/ @@ -48,6 +53,9 @@ attribute [simp] IsPrimitiveElem.counit_eq_zero IsPrimitiveElem.comul_eq_tmul_ad /-- In a bialgebra, `0` is a primitive element. -/ lemma IsPrimitiveElem.zero : IsPrimitiveElem R (0 : A) := by simp [isPrimitiveElem_iff] +lemma IsPrimitiveElem.ne_one [Nontrivial R] (ha : IsPrimitiveElem R a) : a ≠ 1 := by + rintro rfl; simpa using ha.counit_eq_zero + /-- Primitive elements in a bialgebra are stable under addition. -/ lemma IsPrimitiveElem.add (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) : IsPrimitiveElem R (a + b) := @@ -62,6 +70,12 @@ lemma IsPrimitiveElem.map [FunLike F A B] [BialgHomClass F R A B] (f : F) (ha : IsPrimitiveElem R a) : IsPrimitiveElem R (f a) := ⟨by simp [ha], by simp [ha, ← CoalgHomClass.map_comp_comul_apply]⟩ +/-- A bialgebra isomorphism preserves primitive elements. -/ +@[simp] lemma isPrimitiveElem_map_equiv [EquivLike F A B] [BialgEquivClass F R A B] (f : F) : + IsPrimitiveElem R (f a) ↔ IsPrimitiveElem R a where + mp ha := (BialgEquivClass.toBialgEquiv f).symm_apply_apply a ▸ ha.map _ + mpr := .map f + variable (R A) in /-- The primitive elements form a submodule. -/ def primitiveSubmodule : Submodule R A where From 68ba6c047b3d425fc56fafaf0cc62dc860b23925 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 17 Jul 2026 11:59:06 -0700 Subject: [PATCH 11/17] style(RingTheory/Bialgebra/Primitive): compact add, golf ne_one --- Mathlib/RingTheory/Bialgebra/Primitive.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/RingTheory/Bialgebra/Primitive.lean b/Mathlib/RingTheory/Bialgebra/Primitive.lean index aa0523fbe82dea..3495684ad22347 100644 --- a/Mathlib/RingTheory/Bialgebra/Primitive.lean +++ b/Mathlib/RingTheory/Bialgebra/Primitive.lean @@ -53,13 +53,13 @@ attribute [simp] IsPrimitiveElem.counit_eq_zero IsPrimitiveElem.comul_eq_tmul_ad /-- In a bialgebra, `0` is a primitive element. -/ lemma IsPrimitiveElem.zero : IsPrimitiveElem R (0 : A) := by simp [isPrimitiveElem_iff] -lemma IsPrimitiveElem.ne_one [Nontrivial R] (ha : IsPrimitiveElem R a) : a ≠ 1 := by - rintro rfl; simpa using ha.counit_eq_zero +/-- In a bialgebra over a nontrivial semiring, primitive elements are not `1`. -/ +lemma IsPrimitiveElem.ne_one [Nontrivial R] (ha : IsPrimitiveElem R a) : a ≠ 1 := + ne_of_apply_ne (counit (R := R)) (by simp [ha]) /-- Primitive elements in a bialgebra are stable under addition. -/ lemma IsPrimitiveElem.add (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) : - IsPrimitiveElem R (a + b) := - ⟨by simp [ha, hb], by simp [ha, hb, add_tmul, tmul_add]; abel⟩ + IsPrimitiveElem R (a + b) := ⟨by simp [ha, hb], by simp [ha, hb, add_tmul, tmul_add]; abel⟩ /-- Primitive elements in a bialgebra are stable under scalar multiplication. -/ lemma IsPrimitiveElem.smul (ha : IsPrimitiveElem R a) (r : R) : IsPrimitiveElem R (r • a) := From f17a87715004713f76ea6bf4c4a18d8468b9fd4c Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 17 Jul 2026 12:18:36 -0700 Subject: [PATCH 12/17] refactor(RingTheory/HopfAlgebra/Generators): LinearMap namespace, right-handed twins --- Mathlib/RingTheory/Bialgebra/Primitive.lean | 4 +- .../RingTheory/HopfAlgebra/Generators.lean | 52 +++++++++++++------ Mathlib/RingTheory/HopfAlgebra/Primitive.lean | 3 +- 3 files changed, 39 insertions(+), 20 deletions(-) diff --git a/Mathlib/RingTheory/Bialgebra/Primitive.lean b/Mathlib/RingTheory/Bialgebra/Primitive.lean index 3495684ad22347..ba915abc6220a1 100644 --- a/Mathlib/RingTheory/Bialgebra/Primitive.lean +++ b/Mathlib/RingTheory/Bialgebra/Primitive.lean @@ -23,8 +23,8 @@ This file defines primitive elements in a bialgebra, i.e. elements `a` such that * `primitiveSubmodule` is a `LieSubalgebra` with bracket `[a, b] = a * b - b * a`. (`IsPrimitiveElem.commutator` is stated with `a * b - b * a` rather than `⁅a, b⁆` to avoid importing Lie theory into this file.) -* In characteristic 0 over a field, the primitive elements of a cocommutative connected - bialgebra generate it as the universal enveloping of a Lie algebra. +* (Cartier–Milnor–Moore) In characteristic 0 over a field, the primitive elements of a + cocommutative connected bialgebra generate it as the universal enveloping of a Lie algebra. * Generalize to `(g, h)`-skew-primitive elements `Δ a = a ⊗ₜ g + h ⊗ₜ a` for group-like `g`, `h` over a plain coalgebra, of which primitivity is the `(1, 1)` case over a bialgebra. -/ diff --git a/Mathlib/RingTheory/HopfAlgebra/Generators.lean b/Mathlib/RingTheory/HopfAlgebra/Generators.lean index 520387fc304330..6ffc80cabe97ed 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Generators.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Generators.lean @@ -19,23 +19,25 @@ antimultiplicative antipode data on generators. ## Main results -* `HopfAlgebra.convMul_eq_one_of_adjoin_eq_top_left` and - `HopfAlgebra.convMul_eq_one_of_adjoin_eq_top_right`: a pointwise one-sided convolution inverse of +* `LinearMap.convMul_eq_one_of_adjoin_eq_top_left` and + `LinearMap.convMul_eq_one_of_adjoin_eq_top_right`: a pointwise one-sided convolution inverse of a multiplicative map on generators is a global one. -* `HopfAlgebra.eq_antipode_of_convMul_id_eq_one` : a left convolution inverse of `id` is the +* `HopfAlgebra.eq_antipode_of_convMul_id_eq_one` and + `HopfAlgebra.eq_antipode_of_id_convMul_eq_one`: a one-sided convolution inverse of `id` is the antipode. -* `HopfAlgebra.eq_antipode_of_adjoin_eq_top` : a left convolution inverse of `id` on a generating - set is the antipode. +* `HopfAlgebra.eq_antipode_of_adjoin_eq_top_left` and + `HopfAlgebra.eq_antipode_of_adjoin_eq_top_right`: a one-sided convolution inverse of `id` on a + generating set is the antipode. -/ public section -namespace HopfAlgebra - open Algebra Coalgebra LinearMap WithConv variable {R A B : Type*} [CommSemiring R] +namespace LinearMap + section ExtensionPrinciple /-! ### Extension principle from algebra generators -/ @@ -43,9 +45,8 @@ section ExtensionPrinciple variable [Semiring A] [Bialgebra R A] [Semiring B] [Algebra R B] {g f : A →ₗ[R] B} {s : Set A} -/-- If a unital antimultiplicative map `g` and a unital multiplicative map `f` satisfy -`toConv g * toConv f = 1` pointwise on an algebra-generating set, then they do so globally: -a left convolution inverse on generators is a left convolution inverse. -/ +/-- If a unital antimultiplicative map `g` is a left convolution inverse of a unital +multiplicative map `f` pointwise on an algebra-generating set, then `toConv g * toConv f = 1`. -/ theorem convMul_eq_one_of_adjoin_eq_top_left (g_one : g 1 = 1) (g_mul : ∀ x y, g (x * y) = g y * g x) (f_one : f 1 = 1) (f_mul : ∀ x y, f (x * y) = f x * f y) @@ -54,7 +55,7 @@ theorem convMul_eq_one_of_adjoin_eq_top_left toConv g * toConv f = 1 := by ext x; refine adjoin_le (S := (eqLocus (toConv g * toConv f).ofConv (ofConv 1)).toSubalgebra ?_ fun a b ha hb => ?_) - g_convMul_f (adjoin_eq_top ▸ mem_top : x ∈ adjoin R s) + g_convMul_f (adjoin_eq_top.ge mem_top) · simp [g_one, f_one, TensorProduct.one_def] let 𝓡a := ℛ R a; let 𝓡b := ℛ R b simp only [mem_eqLocus, 𝓡a.convMul_apply, 𝓡b.convMul_apply, convOne_apply] at ha hb ⊢ @@ -66,8 +67,8 @@ theorem convMul_eq_one_of_adjoin_eq_top_left rw [Finset.sum_comm]; simp_rw [← Finset.sum_mul, ← Finset.mul_sum, ha, ← commutes] simp_rw [mul_assoc, ← Finset.mul_sum, hb, ← map_mul, ← Bialgebra.counit_mul] -/-- Analogue of `convMul_eq_one_of_adjoin_eq_top_left` for `toConv f * toConv g = 1`: -a right convolution inverse on generators is a right convolution inverse. -/ +/-- If a unital antimultiplicative map `g` is a right convolution inverse of a unital +multiplicative map `f` pointwise on an algebra-generating set, then `toConv f * toConv g = 1`. -/ theorem convMul_eq_one_of_adjoin_eq_top_right (g_one : g 1 = 1) (g_mul : ∀ x y, g (x * y) = g y * g x) (f_one : f 1 = 1) (f_mul : ∀ x y, f (x * y) = f x * f y) @@ -76,7 +77,7 @@ theorem convMul_eq_one_of_adjoin_eq_top_right toConv f * toConv g = 1 := by ext x; refine adjoin_le (S := (eqLocus (toConv f * toConv g).ofConv (ofConv 1)).toSubalgebra ?_ fun a b ha hb => ?_) - f_convMul_g (adjoin_eq_top ▸ mem_top : x ∈ adjoin R s) + f_convMul_g (adjoin_eq_top.ge mem_top) · simp [g_one, f_one, TensorProduct.one_def] let 𝓡a := ℛ R a; let 𝓡b := ℛ R b simp only [mem_eqLocus, 𝓡a.convMul_apply, 𝓡b.convMul_apply, convOne_apply] at ha hb ⊢ @@ -91,6 +92,10 @@ theorem convMul_eq_one_of_adjoin_eq_top_right end ExtensionPrinciple +end LinearMap + +namespace HopfAlgebra + section Construction variable [Semiring A] [Bialgebra R A] {S₀ : A →ₗ[R] A} {s : Set A} @@ -121,10 +126,14 @@ theorem eq_antipode_of_convMul_id_eq_one (h : toConv S₀ * toConv LinearMap.id S₀ = antipode R := toConv_injective (left_inv_eq_right_inv h id_mul_antipode) -variable (S₀) in +/-- A right convolution inverse of the identity is the antipode. -/ +theorem eq_antipode_of_id_convMul_eq_one (h : toConv LinearMap.id * toConv S₀ = 1) : + S₀ = antipode R := + toConv_injective (left_inv_eq_right_inv antipode_mul_id h).symm + /-- A unital antimultiplicative map that is a left convolution inverse of the identity on an algebra-generating set is the antipode. -/ -theorem eq_antipode_of_adjoin_eq_top (S₀_one : S₀ 1 = 1) +theorem eq_antipode_of_adjoin_eq_top_left (S₀_one : S₀ 1 = 1) (S₀_mul : ∀ x y, S₀ (x * y) = S₀ y * S₀ x) (adjoin_eq_top : adjoin R s = ⊤) (S₀_convMul_id : ∀ p ∈ s, (toConv S₀ * toConv (.id : A →ₗ[R] A)) p = (1 : WithConv (A →ₗ[R] A)) p) : @@ -133,6 +142,17 @@ theorem eq_antipode_of_adjoin_eq_top (S₀_one : S₀ 1 = 1) (convMul_eq_one_of_adjoin_eq_top_left S₀_one S₀_mul rfl (fun _ _ => rfl) adjoin_eq_top S₀_convMul_id) +/-- A unital antimultiplicative map that is a right convolution inverse of the identity on an +algebra-generating set is the antipode. -/ +theorem eq_antipode_of_adjoin_eq_top_right (S₀_one : S₀ 1 = 1) + (S₀_mul : ∀ x y, S₀ (x * y) = S₀ y * S₀ x) (adjoin_eq_top : adjoin R s = ⊤) + (id_convMul_S₀ : ∀ p ∈ s, + (toConv (.id : A →ₗ[R] A) * toConv S₀) p = (1 : WithConv (A →ₗ[R] A)) p) : + S₀ = antipode R := + eq_antipode_of_id_convMul_eq_one + (convMul_eq_one_of_adjoin_eq_top_right S₀_one S₀_mul rfl (fun _ _ => rfl) + adjoin_eq_top id_convMul_S₀) + end Uniqueness end HopfAlgebra diff --git a/Mathlib/RingTheory/HopfAlgebra/Primitive.lean b/Mathlib/RingTheory/HopfAlgebra/Primitive.lean index 0a06d2a2b9739a..c6823c6d1c37fd 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Primitive.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Primitive.lean @@ -61,8 +61,7 @@ theorem eq_antipode_of_primitives [Ring A] [HopfAlgebra R A] (S : A →ₐ[R] A (adjoin_eq_top : Algebra.adjoin R s = ⊤) (prim : ∀ p ∈ s, IsPrimitiveElem R p) (S_apply : ∀ p ∈ s, S p = op (-p)) : (opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap = antipode R := - eq_antipode_of_adjoin_eq_top ((opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap) - (by simp) (fun _ _ => by simp) adjoin_eq_top + eq_antipode_of_adjoin_eq_top_left (by simp) (fun _ _ => by simp) adjoin_eq_top (fun p hp => by simp [convMul_apply, prim p hp, S_apply p hp]) end HopfAlgebra From b788da7192800a6d0e480f9b48ea5eff7ece9302 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 17 Jul 2026 12:23:28 -0700 Subject: [PATCH 13/17] docs(RingTheory/HopfAlgebra/Generators): trim module docstring --- Mathlib/RingTheory/HopfAlgebra/Generators.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/Mathlib/RingTheory/HopfAlgebra/Generators.lean b/Mathlib/RingTheory/HopfAlgebra/Generators.lean index 6ffc80cabe97ed..51ae14e441e5e8 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Generators.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Generators.lean @@ -22,9 +22,6 @@ antimultiplicative antipode data on generators. * `LinearMap.convMul_eq_one_of_adjoin_eq_top_left` and `LinearMap.convMul_eq_one_of_adjoin_eq_top_right`: a pointwise one-sided convolution inverse of a multiplicative map on generators is a global one. -* `HopfAlgebra.eq_antipode_of_convMul_id_eq_one` and - `HopfAlgebra.eq_antipode_of_id_convMul_eq_one`: a one-sided convolution inverse of `id` is the - antipode. * `HopfAlgebra.eq_antipode_of_adjoin_eq_top_left` and `HopfAlgebra.eq_antipode_of_adjoin_eq_top_right`: a one-sided convolution inverse of `id` on a generating set is the antipode. From 2fba8f200ed338740b297b118e4c6b64d4e188b8 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 17 Jul 2026 12:43:37 -0700 Subject: [PATCH 14/17] refactor(RingTheory/HopfAlgebra/Primitive): AlgHom-level uniqueness, term-mode body --- .../RingTheory/HopfAlgebra/Generators.lean | 14 +++---- Mathlib/RingTheory/HopfAlgebra/Primitive.lean | 37 ++++++++++++------- 2 files changed, 30 insertions(+), 21 deletions(-) diff --git a/Mathlib/RingTheory/HopfAlgebra/Generators.lean b/Mathlib/RingTheory/HopfAlgebra/Generators.lean index 51ae14e441e5e8..9eefb28178c03b 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Generators.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Generators.lean @@ -15,7 +15,7 @@ antimultiplicative antipode data on generators. ## Main definitions -* `HopfAlgebra.ofGenerators` : construct a Hopf algebra from data on a generating set. +* `HopfAlgebra.ofGenerators`: construct a Hopf algebra from data on a generating set. ## Main results @@ -51,7 +51,7 @@ theorem convMul_eq_one_of_adjoin_eq_top_left (g_convMul_f : ∀ p ∈ s, (toConv g * toConv f) p = (1 : WithConv (A →ₗ[R] B)) p) : toConv g * toConv f = 1 := by ext x; refine adjoin_le - (S := (eqLocus (toConv g * toConv f).ofConv (ofConv 1)).toSubalgebra ?_ fun a b ha hb => ?_) + (S := (eqLocus (toConv g * toConv f).ofConv (ofConv 1)).toSubalgebra ?_ fun a b ha hb ↦ ?_) g_convMul_f (adjoin_eq_top.ge mem_top) · simp [g_one, f_one, TensorProduct.one_def] let 𝓡a := ℛ R a; let 𝓡b := ℛ R b @@ -73,7 +73,7 @@ theorem convMul_eq_one_of_adjoin_eq_top_right (f_convMul_g : ∀ p ∈ s, (toConv f * toConv g) p = (1 : WithConv (A →ₗ[R] B)) p) : toConv f * toConv g = 1 := by ext x; refine adjoin_le - (S := (eqLocus (toConv f * toConv g).ofConv (ofConv 1)).toSubalgebra ?_ fun a b ha hb => ?_) + (S := (eqLocus (toConv f * toConv g).ofConv (ofConv 1)).toSubalgebra ?_ fun a b ha hb ↦ ?_) f_convMul_g (adjoin_eq_top.ge mem_top) · simp [g_one, f_one, TensorProduct.one_def] let 𝓡a := ℛ R a; let 𝓡b := ℛ R b @@ -108,9 +108,9 @@ noncomputable abbrev ofGenerators (S₀_one : S₀ 1 = 1) (S₀_mul : ∀ x y, S (toConv (.id : A →ₗ[R] A) * toConv S₀) p = (1 : WithConv (A →ₗ[R] A)) p) : HopfAlgebra R A := ofConvInverse S₀ - (convMul_eq_one_of_adjoin_eq_top_left S₀_one S₀_mul rfl (fun _ _ => rfl) + (convMul_eq_one_of_adjoin_eq_top_left S₀_one S₀_mul rfl (fun _ _ ↦ rfl) adjoin_eq_top S₀_convMul_id) - (convMul_eq_one_of_adjoin_eq_top_right S₀_one S₀_mul rfl (fun _ _ => rfl) + (convMul_eq_one_of_adjoin_eq_top_right S₀_one S₀_mul rfl (fun _ _ ↦ rfl) adjoin_eq_top id_convMul_S₀) end Construction @@ -136,7 +136,7 @@ theorem eq_antipode_of_adjoin_eq_top_left (S₀_one : S₀ 1 = 1) (toConv S₀ * toConv (.id : A →ₗ[R] A)) p = (1 : WithConv (A →ₗ[R] A)) p) : S₀ = antipode R := eq_antipode_of_convMul_id_eq_one - (convMul_eq_one_of_adjoin_eq_top_left S₀_one S₀_mul rfl (fun _ _ => rfl) + (convMul_eq_one_of_adjoin_eq_top_left S₀_one S₀_mul rfl (fun _ _ ↦ rfl) adjoin_eq_top S₀_convMul_id) /-- A unital antimultiplicative map that is a right convolution inverse of the identity on an @@ -147,7 +147,7 @@ theorem eq_antipode_of_adjoin_eq_top_right (S₀_one : S₀ 1 = 1) (toConv (.id : A →ₗ[R] A) * toConv S₀) p = (1 : WithConv (A →ₗ[R] A)) p) : S₀ = antipode R := eq_antipode_of_id_convMul_eq_one - (convMul_eq_one_of_adjoin_eq_top_right S₀_one S₀_mul rfl (fun _ _ => rfl) + (convMul_eq_one_of_adjoin_eq_top_right S₀_one S₀_mul rfl (fun _ _ ↦ rfl) adjoin_eq_top id_convMul_S₀) end Uniqueness diff --git a/Mathlib/RingTheory/HopfAlgebra/Primitive.lean b/Mathlib/RingTheory/HopfAlgebra/Primitive.lean index c6823c6d1c37fd..0a7587202b361e 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Primitive.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Primitive.lean @@ -16,11 +16,11 @@ a constructor for Hopf algebras generated as algebras by primitive elements. ## Main declarations -* `IsPrimitiveElem.antipode_eq_neg` : the antipode sends primitive elements to their negation. -* `IsPrimitiveElem.antipode` : the antipode preserves primitivity. -* `HopfAlgebra.ofPrimitives` : construct a Hopf algebra from a primitive-element generating set. -* `HopfAlgebra.eq_antipode_of_primitives` : the antipode is the unique anti-algebra hom negating a - primitive generating set. +* `IsPrimitiveElem.antipode_eq_neg`: the antipode sends primitive elements to their negation. +* `IsPrimitiveElem.antipode`: the antipode preserves primitivity. +* `HopfAlgebra.ofPrimitives`: construct a Hopf algebra from a primitive-element generating set. +* `HopfAlgebra.eq_antipodeAlgHomOp_of_primitives`: the antipode is the unique anti-algebra hom + negating a primitive generating set. -/ public section @@ -40,6 +40,11 @@ variable [Ring A] [HopfAlgebra R A] {a : A} protected lemma IsPrimitiveElem.antipode (ha : IsPrimitiveElem R a) : IsPrimitiveElem R (antipode R a) := ha.antipode_eq_neg ▸ ha.neg +/-- The antipode is involutive on primitive elements. -/ +lemma IsPrimitiveElem.antipode_antipode (ha : IsPrimitiveElem R a) : + antipode R (antipode R a) = a := by + simp [ha.antipode_eq_neg, ha.neg.antipode_eq_neg] + end Ring namespace HopfAlgebra @@ -50,18 +55,22 @@ noncomputable abbrev ofPrimitives [Ring A] [Bialgebra R A] (S : A →ₐ[R] Aᵐ (adjoin_eq_top : Algebra.adjoin R s = ⊤) (prim : ∀ p ∈ s, IsPrimitiveElem R p) (S_apply : ∀ p ∈ s, S p = op (-p)) : - HopfAlgebra R A := by - refine ofGenerators ((opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap) - (by simp) (fun _ _ => by simp) adjoin_eq_top ?_ ?_ <;> - exact fun p hp => by simp [convMul_apply, prim p hp, S_apply p hp] + HopfAlgebra R A := + ofGenerators ((opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap) + (by simp) (fun _ _ ↦ by simp) adjoin_eq_top + (fun p hp ↦ by simp [convMul_apply, prim p hp, S_apply p hp]) + (fun p hp ↦ by simp [convMul_apply, prim p hp, S_apply p hp]) /-- On a Hopf algebra generated by primitive elements, the antipode is the unique anti-algebra hom negating the generators. -/ -theorem eq_antipode_of_primitives [Ring A] [HopfAlgebra R A] (S : A →ₐ[R] Aᵐᵒᵖ) {s : Set A} - (adjoin_eq_top : Algebra.adjoin R s = ⊤) (prim : ∀ p ∈ s, IsPrimitiveElem R p) +theorem eq_antipodeAlgHomOp_of_primitives [Ring A] [HopfAlgebra R A] (S : A →ₐ[R] Aᵐᵒᵖ) + {s : Set A} (adjoin_eq_top : Algebra.adjoin R s = ⊤) (prim : ∀ p ∈ s, IsPrimitiveElem R p) (S_apply : ∀ p ∈ s, S p = op (-p)) : - (opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap = antipode R := - eq_antipode_of_adjoin_eq_top_left (by simp) (fun _ _ => by simp) adjoin_eq_top - (fun p hp => by simp [convMul_apply, prim p hp, S_apply p hp]) + S = antipodeAlgHomOp R A := by + have h := eq_antipode_of_adjoin_eq_top_left (S₀ := (opLinearEquiv R).symm.toLinearMap ∘ₗ + S.toLinearMap) (by simp) (fun _ _ ↦ by simp) adjoin_eq_top + (fun p hp ↦ by simp [convMul_apply, prim p hp, S_apply p hp]) + ext a + simpa using congr(op ($h a)) end HopfAlgebra From ef27405dd4e45ed7ac0827c6aa2bbb112906416d Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 17 Jul 2026 12:46:48 -0700 Subject: [PATCH 15/17] style(RingTheory/HopfAlgebra/Primitive): compact antipode_antipode --- Mathlib/RingTheory/HopfAlgebra/Primitive.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/HopfAlgebra/Primitive.lean b/Mathlib/RingTheory/HopfAlgebra/Primitive.lean index 0a7587202b361e..ecab71220ea302 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Primitive.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Primitive.lean @@ -42,8 +42,7 @@ protected lemma IsPrimitiveElem.antipode (ha : IsPrimitiveElem R a) : /-- The antipode is involutive on primitive elements. -/ lemma IsPrimitiveElem.antipode_antipode (ha : IsPrimitiveElem R a) : - antipode R (antipode R a) = a := by - simp [ha.antipode_eq_neg, ha.neg.antipode_eq_neg] + antipode R (antipode R a) = a := by simp [ha.antipode_eq_neg, ha.neg.antipode_eq_neg] end Ring From ce4355b078e9f9e53cf3aea828a00999df497d26 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 17 Jul 2026 12:47:34 -0700 Subject: [PATCH 16/17] style(RingTheory/HopfAlgebra/Primitive): lift shared Ring binder --- Mathlib/RingTheory/HopfAlgebra/Primitive.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/Mathlib/RingTheory/HopfAlgebra/Primitive.lean b/Mathlib/RingTheory/HopfAlgebra/Primitive.lean index ecab71220ea302..a186cb0e2bc244 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Primitive.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Primitive.lean @@ -48,9 +48,11 @@ end Ring namespace HopfAlgebra +variable [Ring A] + /-- Upgrade a bialgebra generated by primitive elements to a Hopf algebra by specifying the antipode-on-generators formula `S p = op (-p)`. -/ -noncomputable abbrev ofPrimitives [Ring A] [Bialgebra R A] (S : A →ₐ[R] Aᵐᵒᵖ) {s : Set A} +noncomputable abbrev ofPrimitives [Bialgebra R A] (S : A →ₐ[R] Aᵐᵒᵖ) {s : Set A} (adjoin_eq_top : Algebra.adjoin R s = ⊤) (prim : ∀ p ∈ s, IsPrimitiveElem R p) (S_apply : ∀ p ∈ s, S p = op (-p)) : @@ -62,8 +64,8 @@ noncomputable abbrev ofPrimitives [Ring A] [Bialgebra R A] (S : A →ₐ[R] Aᵐ /-- On a Hopf algebra generated by primitive elements, the antipode is the unique anti-algebra hom negating the generators. -/ -theorem eq_antipodeAlgHomOp_of_primitives [Ring A] [HopfAlgebra R A] (S : A →ₐ[R] Aᵐᵒᵖ) - {s : Set A} (adjoin_eq_top : Algebra.adjoin R s = ⊤) (prim : ∀ p ∈ s, IsPrimitiveElem R p) +theorem eq_antipodeAlgHomOp_of_primitives [HopfAlgebra R A] (S : A →ₐ[R] Aᵐᵒᵖ) {s : Set A} + (adjoin_eq_top : Algebra.adjoin R s = ⊤) (prim : ∀ p ∈ s, IsPrimitiveElem R p) (S_apply : ∀ p ∈ s, S p = op (-p)) : S = antipodeAlgHomOp R A := by have h := eq_antipode_of_adjoin_eq_top_left (S₀ := (opLinearEquiv R).symm.toLinearMap ∘ₗ From ae973d539dc3c11cbbfbc9f9088b264b202b80a9 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 17 Jul 2026 12:48:57 -0700 Subject: [PATCH 17/17] style(RingTheory/HopfAlgebra/Primitive): file-level Ring binder --- Mathlib/RingTheory/HopfAlgebra/Primitive.lean | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/Mathlib/RingTheory/HopfAlgebra/Primitive.lean b/Mathlib/RingTheory/HopfAlgebra/Primitive.lean index a186cb0e2bc244..8d62d446eb88d6 100644 --- a/Mathlib/RingTheory/HopfAlgebra/Primitive.lean +++ b/Mathlib/RingTheory/HopfAlgebra/Primitive.lean @@ -27,10 +27,10 @@ public section open HopfAlgebra LinearMap MulOpposite -variable {R A : Type*} [CommSemiring R] +variable {R A : Type*} [CommSemiring R] [Ring A] -section Ring -variable [Ring A] [HopfAlgebra R A] {a : A} +section +variable [HopfAlgebra R A] {a : A} /-- The antipode of a Hopf algebra sends primitive elements to their negation. -/ @[simp] theorem IsPrimitiveElem.antipode_eq_neg (ha : IsPrimitiveElem R a) : antipode R a = -a := by @@ -44,12 +44,10 @@ protected lemma IsPrimitiveElem.antipode (ha : IsPrimitiveElem R a) : lemma IsPrimitiveElem.antipode_antipode (ha : IsPrimitiveElem R a) : antipode R (antipode R a) = a := by simp [ha.antipode_eq_neg, ha.neg.antipode_eq_neg] -end Ring +end namespace HopfAlgebra -variable [Ring A] - /-- Upgrade a bialgebra generated by primitive elements to a Hopf algebra by specifying the antipode-on-generators formula `S p = op (-p)`. -/ noncomputable abbrev ofPrimitives [Bialgebra R A] (S : A →ₐ[R] Aᵐᵒᵖ) {s : Set A}