Skip to content

Commit 3cd5cf9

Browse files
hawkrobeeric-wieser
hawkrobe
and
eric-wieser
committed
feat(RingTheory): quotients of coalgebra/bialgebra/Hopf algebras (leanprover-community#39790)
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
1 parent 6a37ffc commit 3cd5cf9

4 files changed

Lines changed: 296 additions & 0 deletions

File tree

‎Mathlib.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6419,6 +6419,7 @@ public import Mathlib.RingTheory.Bialgebra.Equiv
64196419
public import Mathlib.RingTheory.Bialgebra.GroupLike
64206420
public import Mathlib.RingTheory.Bialgebra.Hom
64216421
public import Mathlib.RingTheory.Bialgebra.MonoidAlgebra
6422+
public import Mathlib.RingTheory.Bialgebra.Quotient
64226423
public import Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
64236424
public import Mathlib.RingTheory.Bialgebra.TensorProduct
64246425
public import Mathlib.RingTheory.Binomial
@@ -6434,6 +6435,7 @@ public import Mathlib.RingTheory.Coalgebra.GroupLike
64346435
public import Mathlib.RingTheory.Coalgebra.Hom
64356436
public import Mathlib.RingTheory.Coalgebra.MonoidAlgebra
64366437
public import Mathlib.RingTheory.Coalgebra.MulOpposite
6438+
public import Mathlib.RingTheory.Coalgebra.Quotient
64376439
public import Mathlib.RingTheory.Coalgebra.TensorProduct
64386440
public import Mathlib.RingTheory.Complex
64396441
public import Mathlib.RingTheory.Conductor
@@ -6576,6 +6578,7 @@ public import Mathlib.RingTheory.HopfAlgebra.Basic
65766578
public import Mathlib.RingTheory.HopfAlgebra.Convolution
65776579
public import Mathlib.RingTheory.HopfAlgebra.GroupLike
65786580
public import Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
6581+
public import Mathlib.RingTheory.HopfAlgebra.Quotient
65796582
public import Mathlib.RingTheory.HopfAlgebra.TensorProduct
65806583
public import Mathlib.RingTheory.HopkinsLevitzki
65816584
public import Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

‎Mathlib/RingTheory/Bialgebra/Quotient.lean‎

Lines changed: 82 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
1+
/-
2+
Copyright (c) 2026 Robert Hawkins. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Robert Hawkins
5+
-/
6+
module
7+
8+
public import Mathlib.RingTheory.Bialgebra.Hom
9+
public import Mathlib.RingTheory.Coalgebra.Quotient
10+
public import Mathlib.RingTheory.Ideal.Quotient.Operations
11+
public import Mathlib.RingTheory.TensorProduct.Maps
12+
13+
/-!
14+
# Bialgebra structure on quotients
15+
16+
If `I` is a two-sided ideal of an `R`-bialgebra `A` whose underlying `R`-submodule is a
17+
coideal, then the quotient `A ⧸ I` inherits a bialgebra structure.
18+
19+
## Main definitions
20+
21+
* `Bialgebra.Quotient.counitAlgHom` : the counit on `A ⧸ I`, as an `R`-algebra homomorphism.
22+
* `Bialgebra.Quotient.comulAlgHom` : comultiplication on `A ⧸ I` as an `R`-algebra homomorphism.
23+
* `Bialgebra.Quotient.mkBialgHom` : `Ideal.Quotient.mkₐ` as a bialgebra homomorphism.
24+
25+
## Main results
26+
27+
* `Bialgebra R (A ⧸ I)` instance when `[I.IsTwoSided]` and `[(I.restrictScalars R).IsCoideal]`.
28+
-/
29+
30+
@[expose] public section
31+
32+
open Bialgebra Coalgebra LinearMap TensorProduct
33+
34+
variable {R A : Type*} [CommRing R] [Ring A] [Bialgebra R A]
35+
variable (I : Ideal A) [I.IsTwoSided] [(I.restrictScalars R).IsCoideal]
36+
37+
namespace Bialgebra.Quotient
38+
39+
/-- The counit on `A ⧸ I`, as an `R`-algebra homomorphism. -/
40+
def counitAlgHom : (A ⧸ I) →ₐ[R] R :=
41+
Ideal.Quotient.liftₐ I (Bialgebra.counitAlgHom R A)
42+
(Submodule.IsCoideal.counit_eq_zero (I := I.restrictScalars R))
43+
44+
/-- The comultiplication on `A ⧸ I`, as an `R`-algebra homomorphism. -/
45+
def comulAlgHom : (A ⧸ I) →ₐ[R] (A ⧸ I) ⊗[R] (A ⧸ I) :=
46+
Ideal.Quotient.liftₐ I
47+
((Algebra.TensorProduct.map (Ideal.Quotient.mkₐ R I) (Ideal.Quotient.mkₐ R I)).comp
48+
(Bialgebra.comulAlgHom R A))
49+
(Submodule.IsCoideal.map_mkQ_comul_eq_zero (I := I.restrictScalars R))
50+
51+
lemma counit_comp_mkₐ :
52+
(counitAlgHom I).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap = counit := rfl
53+
54+
lemma comul_comp_mkₐ :
55+
(comulAlgHom (R := R) I).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap =
56+
map (Ideal.Quotient.mkₐ R I).toLinearMap (Ideal.Quotient.mkₐ R I).toLinearMap ∘ₗ comul := rfl
57+
58+
/-- The bialgebra structure on `A ⧸ I` when `I` is a biideal. -/
59+
instance : Bialgebra R (A ⧸ I) := by
60+
refine .ofAlgHom (comulAlgHom I) (counitAlgHom I) ?_ ?_ ?_ <;>
61+
refine Ideal.Quotient.algHom_ext R (AlgHom.toLinearMap_injective ?_) <;>
62+
simp only [coassoc_simps, AlgHom.comp_toLinearMap, Algebra.TensorProduct.toLinearMap_map,
63+
comul_comp_mkₐ, counit_comp_mkₐ]
64+
· simp [coassoc_simps]
65+
· rw [CoassocSimps.map_counit_comp_comul_left]; rfl
66+
· rw [CoassocSimps.map_counit_comp_comul_right]; rfl
67+
68+
@[simp] lemma counit_mk (a : A) :
69+
counit (R := R) (Ideal.Quotient.mk I a) = counit a := rfl
70+
71+
@[simp] lemma comul_mk (a : A) :
72+
comul (R := R) (Ideal.Quotient.mk I a) =
73+
map (Ideal.Quotient.mkₐ R I).toLinearMap (Ideal.Quotient.mkₐ R I).toLinearMap (comul a) :=
74+
rfl
75+
76+
/-- `Ideal.Quotient.mkₐ` as a bialgebra homomorphism. -/
77+
def mkBialgHom : A →ₐc[R] A ⧸ I := .ofAlgHom (Ideal.Quotient.mkₐ R I) rfl rfl
78+
79+
@[simp] lemma mkBialgHom_apply (a : A) :
80+
mkBialgHom (R := R) I a = Ideal.Quotient.mk I a := rfl
81+
82+
end Bialgebra.Quotient

‎Mathlib/RingTheory/Coalgebra/Quotient.lean‎

Lines changed: 92 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,92 @@
1+
/-
2+
Copyright (c) 2026 Robert Hawkins. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Robert Hawkins
5+
-/
6+
module
7+
8+
public import Mathlib.LinearAlgebra.Quotient.Basic
9+
public import Mathlib.LinearAlgebra.TensorProduct.RightExactness
10+
public import Mathlib.RingTheory.Coalgebra.CoassocSimps
11+
public import Mathlib.RingTheory.Coalgebra.Hom
12+
13+
/-!
14+
# Coalgebra structure on the quotient by a coideal
15+
16+
## Main definitions
17+
18+
* `Submodule.IsCoideal I` : the submodule `I : Submodule R C` is a coideal.
19+
* `Coalgebra.Quotient.mkQCoalgHom` : `Submodule.mkQ` as a coalgebra homomorphism.
20+
21+
## Main results
22+
23+
* `Coalgebra` instance on `C ⧸ I` when `[I.IsCoideal]`.
24+
-/
25+
26+
public section
27+
28+
open Coalgebra LinearMap TensorProduct
29+
30+
variable {R C : Type*} [CommRing R] [AddCommGroup C] [Module R C]
31+
32+
section CoalgebraStruct
33+
34+
variable [CoalgebraStruct R C]
35+
36+
/-- An `R`-submodule `I` of an `R`-coalgebra `C` is a *coideal* if the counit vanishes on
37+
`I` and the comultiplication descends through the module quotient `C ⧸ I`. -/
38+
@[mk_iff]
39+
class Submodule.IsCoideal (I : Submodule R C) : Prop where
40+
counit_eq_zero : ∀ ⦃x : C⦄, x ∈ I → counit (R := R) x = 0
41+
map_mkQ_comul_eq_zero : ∀ ⦃x : C⦄, x ∈ I → TensorProduct.map I.mkQ I.mkQ (comul x) = 0
42+
43+
/-- A submodule is a coideal iff the counit vanishes on it and its comultiplication image lies
44+
in `I ⊗ C + C ⊗ I`, the textbook form of the coideal condition. -/
45+
lemma Submodule.isCoideal_iff_comul_mem (I : Submodule R C) :
46+
I.IsCoideal ↔ (∀ x ∈ I, counit (R := R) x = 0) ∧
47+
∀ x ∈ I, comul x ∈
48+
LinearMap.range (lTensor C I.subtype) ⊔ LinearMap.range (rTensor C I.subtype) := by
49+
simp_rw [isCoideal_iff, ← LinearMap.mem_ker,
50+
TensorProduct.map_ker (LinearMap.exact_subtype_mkQ I) I.mkQ_surjective
51+
(LinearMap.exact_subtype_mkQ I) I.mkQ_surjective]
52+
53+
end CoalgebraStruct
54+
55+
namespace Coalgebra.Quotient
56+
57+
section CoalgebraStruct
58+
59+
variable [CoalgebraStruct R C] (I : Submodule R C) [I.IsCoideal]
60+
61+
instance : CoalgebraStruct R (C ⧸ I) where
62+
comul := I.liftQ (map I.mkQ I.mkQ ∘ₗ comul) Submodule.IsCoideal.map_mkQ_comul_eq_zero
63+
counit := I.liftQ counit Submodule.IsCoideal.counit_eq_zero
64+
65+
lemma comul_comp_mkQ : comul ∘ₗ I.mkQ = map I.mkQ I.mkQ ∘ₗ (comul : C →ₗ[R] _) := rfl
66+
67+
lemma counit_comp_mkQ : counit ∘ₗ I.mkQ = (counit : C →ₗ[R] R) := rfl
68+
69+
@[simp]
70+
lemma counit_mk (x : C) : counit (R := R) (Submodule.Quotient.mk (p := I) x) = counit x := rfl
71+
72+
@[simp]
73+
lemma comul_mk (x : C) :
74+
comul (R := R) (Submodule.Quotient.mk (p := I) x) = map I.mkQ I.mkQ (comul x) := rfl
75+
76+
/-- `Submodule.mkQ` as a coalgebra homomorphism. -/
77+
@[expose] def mkQCoalgHom : C →ₗc[R] C ⧸ I := ⟨I.mkQ, rfl, rfl⟩
78+
79+
@[simp] lemma mkQCoalgHom_apply (x : C) :
80+
mkQCoalgHom (R := R) I x = Submodule.Quotient.mk x := rfl
81+
82+
end CoalgebraStruct
83+
84+
variable [Coalgebra R C] (I : Submodule R C) [I.IsCoideal]
85+
86+
instance : Coalgebra R (C ⧸ I) := by
87+
constructor <;> ext : 1 <;>
88+
simp only [coassoc_simps, comul_comp_mkQ, counit_comp_mkQ]
89+
· rw [CoassocSimps.map_counit_comp_comul_left]; rfl
90+
· rw [CoassocSimps.map_counit_comp_comul_right]; rfl
91+
92+
end Coalgebra.Quotient

‎Mathlib/RingTheory/HopfAlgebra/Quotient.lean‎

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,119 @@
1+
/-
2+
Copyright (c) 2026 Robert Hawkins. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Robert Hawkins
5+
-/
6+
module
7+
8+
public import Mathlib.RingTheory.Bialgebra.Quotient
9+
public import Mathlib.RingTheory.HopfAlgebra.Convolution
10+
11+
/-!
12+
# Hopf algebra structure on quotients by Hopf ideals
13+
14+
A *Hopf ideal* of an `R`-Hopf algebra `A` is a biideal stable under the antipode. The quotient
15+
by a Hopf ideal inherits a Hopf algebra structure.
16+
17+
## Main definitions
18+
19+
* `Ideal.IsHopfIdeal R I` : `I` is a coideal (as an `R`-submodule) stable under the antipode.
20+
21+
## Main results
22+
23+
* `HopfAlgebra.ofSurjective` : the Hopf algebra axioms transfer along a surjective bialgebra
24+
homomorphism intertwining the antipodes.
25+
* `HopfAlgebra R (A ⧸ I)` instance when `[I.IsTwoSided]` and `[I.IsHopfIdeal R]`.
26+
-/
27+
28+
public section
29+
30+
open Bialgebra Bialgebra.Quotient Coalgebra HopfAlgebra Ideal.Quotient LinearMap
31+
TensorProduct WithConv
32+
33+
namespace HopfAlgebra
34+
35+
section ofSurjective
36+
37+
variable {R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B]
38+
[HopfAlgebra R A] [HopfAlgebraStruct R B]
39+
40+
/-- Post-composition by an algebra homomorphism preserves the convolution unit. -/
41+
lemma _root_.LinearMap.algHom_comp_convOne (g : A →ₐ[R] B) :
42+
g.toLinearMap ∘ₗ (1 : WithConv (A →ₗ[R] A)).ofConv = (1 : WithConv (A →ₗ[R] B)).ofConv := by
43+
ext a; simp
44+
45+
/-- Pre-composition by a coalgebra homomorphism preserves the convolution unit. -/
46+
lemma _root_.LinearMap.convOne_comp_coalgHom (g : A →ₗc[R] B) :
47+
(1 : WithConv (B →ₗ[R] B)).ofConv ∘ₗ g.toLinearMap = (1 : WithConv (A →ₗ[R] B)).ofConv := by
48+
ext a; simp
49+
50+
/-- Transfer the Hopf algebra axioms along a surjective bialgebra homomorphism intertwining
51+
the antipodes. -/
52+
noncomputable abbrev ofSurjective (f : A →ₐc[R] B) (hf : Function.Surjective f)
53+
(hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R) : HopfAlgebra R B := by
54+
refine .ofConvInverse (antipode R) (ofConv_injective ?_) (ofConv_injective ?_) <;>
55+
rw [← LinearMap.cancel_right (show Function.Surjective f.toLinearMap from hf)]
56+
· calc (toConv (antipode R) * toConv .id : WithConv (B →ₗ[R] B)).ofConv ∘ₗ
57+
f.toCoalgHom.toLinearMap
58+
= (toConv (f.toLinearMap ∘ₗ antipode R) * toConv f.toLinearMap).ofConv := by
59+
rw [convMul_comp_coalgHom_distrib, hS]; rfl
60+
_ = (AlgHomClass.toAlgHom f).toLinearMap ∘ₗ
61+
(toConv (antipode R) * toConv .id : WithConv (A →ₗ[R] A)).ofConv := by
62+
rw [algHom_comp_convMul_distrib]; rfl
63+
_ = (1 : WithConv (B →ₗ[R] B)).ofConv ∘ₗ f.toLinearMap := by
64+
rw [antipode_mul_id, algHom_comp_convOne, ← convOne_comp_coalgHom f.toCoalgHom]
65+
· calc (toConv .id * toConv (antipode R) : WithConv (B →ₗ[R] B)).ofConv ∘ₗ
66+
f.toCoalgHom.toLinearMap
67+
= (toConv f.toLinearMap * toConv (f.toLinearMap ∘ₗ antipode R)).ofConv := by
68+
rw [convMul_comp_coalgHom_distrib, hS]; rfl
69+
_ = (AlgHomClass.toAlgHom f).toLinearMap ∘ₗ
70+
(toConv .id * toConv (antipode R) : WithConv (A →ₗ[R] A)).ofConv := by
71+
rw [algHom_comp_convMul_distrib]; rfl
72+
_ = (1 : WithConv (B →ₗ[R] B)).ofConv ∘ₗ f.toLinearMap := by
73+
rw [id_mul_antipode, algHom_comp_convOne, ← convOne_comp_coalgHom f.toCoalgHom]
74+
75+
end ofSurjective
76+
77+
end HopfAlgebra
78+
79+
variable {R A : Type*} [CommRing R] [Ring A]
80+
81+
section HopfAlgebraStruct
82+
83+
variable [HopfAlgebraStruct R A]
84+
85+
variable (R) in
86+
/-- An ideal whose underlying `R`-submodule is a coideal and which is stable under the
87+
antipode (`S(I) ⊆ I`). Together with `I.IsTwoSided`, this makes `I` a *Hopf ideal*. -/
88+
@[mk_iff]
89+
class Ideal.IsHopfIdeal (I : Ideal A) : Prop extends (I.restrictScalars R).IsCoideal where
90+
antipode_mem : ∀ ⦃x : A⦄, x ∈ I → antipode R x ∈ I
91+
92+
end HopfAlgebraStruct
93+
94+
namespace HopfAlgebra.Quotient
95+
96+
section HopfAlgebraStruct
97+
98+
variable [HopfAlgebraStruct R A] (I : Ideal A) [I.IsTwoSided] [I.IsHopfIdeal R]
99+
100+
instance : HopfAlgebraStruct R (A ⧸ I) where
101+
antipode := Submodule.mapQ (I.restrictScalars R) (I.restrictScalars R)
102+
(antipode R) (Ideal.IsHopfIdeal.antipode_mem (R := R))
103+
104+
@[simp]
105+
lemma antipode_mk (a : A) :
106+
antipode R (Ideal.Quotient.mk I a) = Ideal.Quotient.mk I (antipode R a) := rfl
107+
108+
lemma antipode_comp_mkₐ :
109+
antipode R ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap =
110+
(Ideal.Quotient.mkₐ R I).toLinearMap ∘ₗ antipode R := by ext; simp
111+
112+
end HopfAlgebraStruct
113+
114+
variable [HopfAlgebra R A] (I : Ideal A) [I.IsTwoSided] [I.IsHopfIdeal R]
115+
116+
noncomputable instance : HopfAlgebra R (A ⧸ I) :=
117+
.ofSurjective (mkBialgHom I) mk_surjective (antipode_comp_mkₐ I)
118+
119+
end HopfAlgebra.Quotient

0 commit comments

Comments
 (0)