Skip to content

Commit 04f438a

Browse files
Amelia Livingston101damnationseric-wieser
committed
feat: tensor products of bialgebras (#11977)
We define the data in the monoidal structure on bialgebras - e.g. the bialgebra instance on a tensor product of bialgebras, and the tensor product of two `BialgHom`s as a `BialgHom`. This is done by combining the corresponding API for coalgebras and algebras. Co-authored-by: Amelia Livingston <al3717@ic.ac.uk> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
1 parent b420076 commit 04f438a

File tree

3 files changed

+230
-0
lines changed

3 files changed

+230
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3975,6 +3975,7 @@ import Mathlib.RingTheory.Bezout
39753975
import Mathlib.RingTheory.Bialgebra.Basic
39763976
import Mathlib.RingTheory.Bialgebra.Equiv
39773977
import Mathlib.RingTheory.Bialgebra.Hom
3978+
import Mathlib.RingTheory.Bialgebra.TensorProduct
39783979
import Mathlib.RingTheory.Binomial
39793980
import Mathlib.RingTheory.ChainOfDivisors
39803981
import Mathlib.RingTheory.ClassGroup

‎Mathlib/RingTheory/Bialgebra/TensorProduct.lean‎

Lines changed: 180 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,180 @@
1+
/-
2+
Copyright (c) 2024 Amelia Livingston. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Amelia Livingston
5+
-/
6+
import Mathlib.RingTheory.Bialgebra.Equiv
7+
import Mathlib.RingTheory.Coalgebra.TensorProduct
8+
import Mathlib.RingTheory.TensorProduct.Basic
9+
10+
/-!
11+
# Tensor products of bialgebras
12+
13+
We define the data in the monoidal structure on the category of bialgebras - e.g. the bialgebra
14+
instance on a tensor product of bialgebras, and the tensor product of two `BialgHom`s as a
15+
`BialgHom`. This is done by combining the corresponding API for coalgebras and algebras.
16+
17+
## Implementation notes
18+
19+
Since the coalgebra instance on a tensor product of coalgebras is defined using a universe
20+
monomorphic monoidal category structure on `ModuleCat R`, we require our bialgebras to be in the
21+
same universe as the base ring `R` here too. Any contribution that achieves universe polymorphism
22+
would be welcome. For instance, the tensor product of bialgebras in the
23+
[FLT repo](https://github.com/ImperialCollegeLondon/FLT/blob/eef74b4538c8852363936dfaad23e6ffba72eca5/FLT/mathlibExperiments/Coalgebra/TensorProduct.lean)
24+
is already universe polymorphic since it does not go via category theory.
25+
26+
-/
27+
28+
universe v u
29+
30+
open scoped TensorProduct
31+
32+
namespace Bialgebra.TensorProduct
33+
34+
variable (R A B : Type*) [CommRing R] [Ring A] [Ring B] [Bialgebra R A] [Bialgebra R B]
35+
36+
lemma counit_eq_algHom_toLinearMap :
37+
Coalgebra.counit (R := R) (A := A ⊗[R] B) =
38+
((Algebra.TensorProduct.lmul' R).comp (Algebra.TensorProduct.map
39+
(Bialgebra.counitAlgHom R A) (Bialgebra.counitAlgHom R B))).toLinearMap := by
40+
rfl
41+
42+
lemma comul_eq_algHom_toLinearMap :
43+
Coalgebra.comul (R := R) (A := A ⊗[R] B) =
44+
((Algebra.TensorProduct.tensorTensorTensorComm R A A B B).toAlgHom.comp
45+
(Algebra.TensorProduct.map (Bialgebra.comulAlgHom R A)
46+
(Bialgebra.comulAlgHom R B))).toLinearMap := by
47+
rfl
48+
49+
end Bialgebra.TensorProduct
50+
51+
noncomputable instance TensorProduct.instBialgebra
52+
{R A B : Type u} [CommRing R] [Ring A] [Ring B]
53+
[Bialgebra R A] [Bialgebra R B] : Bialgebra R (A ⊗[R] B) := by
54+
have hcounit := congr(DFunLike.coe $(Bialgebra.TensorProduct.counit_eq_algHom_toLinearMap R A B))
55+
have hcomul := congr(DFunLike.coe $(Bialgebra.TensorProduct.comul_eq_algHom_toLinearMap R A B))
56+
refine Bialgebra.mk' R (A ⊗[R] B) ?_ (fun {x y} => ?_) ?_ (fun {x y} => ?_) <;>
57+
simp_all only [AlgHom.toLinearMap_apply] <;>
58+
simp only [_root_.map_one, _root_.map_mul]
59+
60+
namespace Bialgebra.TensorProduct
61+
62+
variable {R A B C D : Type u} [CommRing R] [Ring A] [Ring B] [Ring C] [Ring D]
63+
[Bialgebra R A] [Bialgebra R B] [Bialgebra R C] [Bialgebra R D]
64+
65+
/-- The tensor product of two bialgebra morphisms as a bialgebra morphism. -/
66+
noncomputable def map (f : A →ₐc[R] B) (g : C →ₐc[R] D) :
67+
A ⊗[R] C →ₐc[R] B ⊗[R] D :=
68+
{ Coalgebra.TensorProduct.map (f : A →ₗc[R] B) (g : C →ₗc[R] D),
69+
Algebra.TensorProduct.map (f : A →ₐ[R] B) (g : C →ₐ[R] D) with }
70+
71+
@[simp]
72+
theorem map_tmul (f : A →ₐc[R] B) (g : C →ₐc[R] D) (x : A) (y : C) :
73+
map f g (x ⊗ₜ y) = f x ⊗ₜ g y :=
74+
rfl
75+
76+
@[simp]
77+
theorem map_toCoalgHom (f : A →ₐc[R] B) (g : C →ₐc[R] D) :
78+
map f g = Coalgebra.TensorProduct.map (f : A →ₗc[R] B) (g : C →ₗc[R] D) := rfl
79+
80+
@[simp]
81+
theorem map_toAlgHom (f : A →ₐc[R] B) (g : C →ₐc[R] D) :
82+
(map f g : A ⊗[R] C →ₐ[R] B ⊗[R] D) =
83+
Algebra.TensorProduct.map (f : A →ₐ[R] B) (g : C →ₐ[R] D) :=
84+
rfl
85+
86+
variable (R A B C) in
87+
/-- The associator for tensor products of R-bialgebras, as a bialgebra equivalence. -/
88+
protected noncomputable def assoc :
89+
(A ⊗[R] B) ⊗[R] C ≃ₐc[R] A ⊗[R] (B ⊗[R] C) :=
90+
{ Coalgebra.TensorProduct.assoc R A B C, Algebra.TensorProduct.assoc R A B C with }
91+
92+
@[simp]
93+
theorem assoc_tmul (x : A) (y : B) (z : C) :
94+
Bialgebra.TensorProduct.assoc R A B C ((x ⊗ₜ y) ⊗ₜ z) = x ⊗ₜ (y ⊗ₜ z) :=
95+
rfl
96+
97+
@[simp]
98+
theorem assoc_symm_tmul (x : A) (y : B) (z : C) :
99+
(Bialgebra.TensorProduct.assoc R A B C).symm (x ⊗ₜ (y ⊗ₜ z)) = (x ⊗ₜ y) ⊗ₜ z :=
100+
rfl
101+
102+
@[simp]
103+
theorem assoc_toCoalgEquiv :
104+
(Bialgebra.TensorProduct.assoc R A B C : _ ≃ₗc[R] _) =
105+
Coalgebra.TensorProduct.assoc R A B C := rfl
106+
107+
@[simp]
108+
theorem assoc_toAlgEquiv :
109+
(Bialgebra.TensorProduct.assoc R A B C : _ ≃ₐ[R] _) =
110+
Algebra.TensorProduct.assoc R A B C := rfl
111+
112+
variable (R A) in
113+
/-- The base ring is a left identity for the tensor product of bialgebras, up to
114+
bialgebra equivalence. -/
115+
protected noncomputable def lid : R ⊗[R] A ≃ₐc[R] A :=
116+
{ Coalgebra.TensorProduct.lid R A, Algebra.TensorProduct.lid R A with }
117+
118+
@[simp]
119+
theorem lid_toCoalgEquiv :
120+
(Bialgebra.TensorProduct.lid R A : R ⊗[R] A ≃ₗc[R] A) = Coalgebra.TensorProduct.lid R A := rfl
121+
122+
@[simp]
123+
theorem lid_toAlgEquiv :
124+
(Bialgebra.TensorProduct.lid R A : R ⊗[R] A ≃ₐ[R] A) = Algebra.TensorProduct.lid R A := rfl
125+
126+
@[simp]
127+
theorem lid_tmul (r : R) (a : A) : Bialgebra.TensorProduct.lid R A (r ⊗ₜ a) = r • a := rfl
128+
129+
@[simp]
130+
theorem lid_symm_apply (a : A) : (Bialgebra.TensorProduct.lid R A).symm a = 1 ⊗ₜ a := rfl
131+
132+
/- TODO: make this defeq, which would involve adding a heterobasic version of
133+
`Coalgebra.TensorProduct.rid`. -/
134+
theorem coalgebra_rid_eq_algebra_rid_apply (x : A ⊗[R] R) :
135+
Coalgebra.TensorProduct.rid R A x = Algebra.TensorProduct.rid R R A x :=
136+
congr($((TensorProduct.AlgebraTensorModule.rid_eq_rid R A).symm) x)
137+
138+
variable (R A) in
139+
/-- The base ring is a right identity for the tensor product of bialgebras, up to
140+
bialgebra equivalence. -/
141+
protected noncomputable def rid : A ⊗[R] R ≃ₐc[R] A where
142+
toCoalgEquiv := Coalgebra.TensorProduct.rid R A
143+
map_mul' x y := by
144+
simp only [CoalgEquiv.toCoalgHom_eq_coe, CoalgHom.toLinearMap_eq_coe, AddHom.toFun_eq_coe,
145+
LinearMap.coe_toAddHom, CoalgHom.coe_toLinearMap, CoalgHom.coe_coe,
146+
coalgebra_rid_eq_algebra_rid_apply, map_mul]
147+
148+
@[simp]
149+
theorem rid_toCoalgEquiv :
150+
(Bialgebra.TensorProduct.rid R A : A ⊗[R] R ≃ₗc[R] A) = Coalgebra.TensorProduct.rid R A := rfl
151+
152+
@[simp]
153+
theorem rid_toAlgEquiv :
154+
(Bialgebra.TensorProduct.rid R A : A ⊗[R] R ≃ₐ[R] A) = Algebra.TensorProduct.rid R R A := by
155+
ext x
156+
exact coalgebra_rid_eq_algebra_rid_apply x
157+
158+
@[simp]
159+
theorem rid_tmul (r : R) (a : A) : Bialgebra.TensorProduct.rid R A (a ⊗ₜ r) = r • a := rfl
160+
161+
@[simp]
162+
theorem rid_symm_apply (a : A) : (Bialgebra.TensorProduct.rid R A).symm a = a ⊗ₜ 1 := rfl
163+
164+
end Bialgebra.TensorProduct
165+
namespace BialgHom
166+
167+
variable {R A B C : Type u} [CommRing R] [Ring A] [Ring B] [Ring C]
168+
[Bialgebra R A] [Bialgebra R B] [Bialgebra R C]
169+
170+
variable (A)
171+
172+
/-- `lTensor A f : A ⊗ B →ₐc A ⊗ C` is the natural bialgebra morphism induced by `f : B →ₐc C`. -/
173+
noncomputable abbrev lTensor (f : B →ₐc[R] C) : A ⊗[R] B →ₐc[R] A ⊗[R] C :=
174+
Bialgebra.TensorProduct.map (BialgHom.id R A) f
175+
176+
/-- `rTensor A f : B ⊗ A →ₐc C ⊗ A` is the natural bialgebra morphism induced by `f : B →ₐc C`. -/
177+
noncomputable abbrev rTensor (f : B →ₐc[R] C) : B ⊗[R] A →ₐc[R] C ⊗[R] A :=
178+
Bialgebra.TensorProduct.map f (BialgHom.id R A)
179+
180+
end BialgHom

‎Mathlib/RingTheory/TensorProduct/Basic.lean‎

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -956,6 +956,55 @@ theorem congr_trans [Algebra S C] [IsScalarTower R S C]
956956

957957
theorem congr_symm (f : A ≃ₐ[S] B) (g : C ≃ₐ[R] D) : congr f.symm g.symm = (congr f g).symm := rfl
958958

959+
variable (R A B C) in
960+
/-- Tensor product of algebras analogue of `mul_left_comm`.
961+
962+
This is the algebra version of `TensorProduct.leftComm`. -/
963+
def leftComm : A ⊗[R] B ⊗[R] C ≃ₐ[R] B ⊗[R] A ⊗[R] C :=
964+
let e₁ := (Algebra.TensorProduct.assoc R A B C).symm
965+
let e₂ := congr (Algebra.TensorProduct.comm R A B) (1 : C ≃ₐ[R] C)
966+
let e₃ := Algebra.TensorProduct.assoc R B A C
967+
e₁.trans (e₂.trans e₃)
968+
969+
@[simp]
970+
theorem leftComm_tmul (m : A) (n : B) (p : C) :
971+
leftComm R A B C (m ⊗ₜ (n ⊗ₜ p)) = n ⊗ₜ (m ⊗ₜ p) :=
972+
rfl
973+
974+
@[simp]
975+
theorem leftComm_symm_tmul (m : A) (n : B) (p : C) :
976+
(leftComm R A B C).symm (n ⊗ₜ (m ⊗ₜ p)) = m ⊗ₜ (n ⊗ₜ p) :=
977+
rfl
978+
979+
@[simp]
980+
theorem leftComm_toLinearEquiv :
981+
(leftComm R A B C : _ ≃ₗ[R] _) = _root_.TensorProduct.leftComm R A B C := rfl
982+
983+
variable (R A B C D) in
984+
/-- Tensor product of algebras analogue of `mul_mul_mul_comm`.
985+
986+
This is the algebra version of `TensorProduct.tensorTensorTensorComm`. -/
987+
def tensorTensorTensorComm : (A ⊗[R] B) ⊗[R] C ⊗[R] D ≃ₐ[R] (A ⊗[R] C) ⊗[R] B ⊗[R] D :=
988+
let e₁ := Algebra.TensorProduct.assoc R A B (C ⊗[R] D)
989+
let e₂ := congr (1 : A ≃ₐ[R] A) (leftComm R B C D)
990+
let e₃ := (Algebra.TensorProduct.assoc R A C (B ⊗[R] D)).symm
991+
e₁.trans (e₂.trans e₃)
992+
993+
@[simp]
994+
theorem tensorTensorTensorComm_tmul (m : A) (n : B) (p : C) (q : D) :
995+
tensorTensorTensorComm R A B C D (m ⊗ₜ n ⊗ₜ (p ⊗ₜ q)) = m ⊗ₜ p ⊗ₜ (n ⊗ₜ q) :=
996+
rfl
997+
998+
@[simp]
999+
theorem tensorTensorTensorComm_symm :
1000+
(tensorTensorTensorComm R A B C D).symm = tensorTensorTensorComm R A C B D := by
1001+
ext; rfl
1002+
1003+
@[simp]
1004+
theorem tensorTensorTensorComm_toLinearEquiv :
1005+
(tensorTensorTensorComm R A B C D : _ ≃ₗ[R] _) =
1006+
_root_.TensorProduct.tensorTensorTensorComm R A B C D := rfl
1007+
9591008
end
9601009

9611010
end Monoidal

0 commit comments

Comments
 (0)