Skip to content

Commit 1323ee5

Browse files
eric-wieserkim-emnomeata
committed
feat: MonoidalCategory (QuadraticModuleCat R) (#7244)
Together with #7130, this now results in a `CommMonoid (Skeleton (QuadraticModuleCat R))`, which is similar to the multiplicative part of the [Grothendieck-Witt ring](https://en.wikipedia.org/wiki/Witt_group#Grothendieck-Witt_ring) of quadratic forms. (Strictly the Grothendieck-Witt ring would introduce a subcategory of QuadraticModuleCat for the non-singular forms) This is largely a copy-and-paste from #7598 (though it was written first) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
1 parent 2da494d commit 1323ee5

File tree

5 files changed

+158
-6
lines changed

5 files changed

+158
-6
lines changed

‎Mathlib.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2344,6 +2344,8 @@ import Mathlib.LinearAlgebra.QuadraticForm.Isometry
23442344
import Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
23452345
import Mathlib.LinearAlgebra.QuadraticForm.Prod
23462346
import Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
2347+
import Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
2348+
import Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric
23472349
import Mathlib.LinearAlgebra.QuadraticForm.Real
23482350
import Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
23492351
import Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries

‎Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat.lean‎

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -30,12 +30,6 @@ open QuadraticForm
3030
instance : CoeSort (QuadraticModuleCat.{v} R) (Type v) :=
3131
⟨(·.carrier)⟩
3232

33-
instance (V : QuadraticModuleCat.{v} R) : AddCommGroup V :=
34-
V.isAddCommGroup
35-
36-
instance (V : QuadraticModuleCat.{v} R) : Module R V :=
37-
V.isModule
38-
3933
/-- The object in the category of quadratic R-modules associated to a quadratic R-module. -/
4034
@[simps form]
4135
def of {X : Type v} [AddCommGroup X] [Module R X] (Q : QuadraticForm R X) :

‎Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean‎

Lines changed: 102 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,102 @@
1+
/-
2+
Copyright (c) 2023 Eric Wieser. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Eric Wieser
5+
-/
6+
import Mathlib.CategoryTheory.Monoidal.Braided
7+
import Mathlib.CategoryTheory.Monoidal.Transport
8+
import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
9+
import Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
10+
import Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
11+
12+
/-!
13+
# The monoidal category structure on quadratic R-modules
14+
15+
The monoidal structure is simply the structure on the underlying modules, where the tensor product
16+
of two modules is equipped with the form constructed via `QuadraticForm.tmul`.
17+
18+
As with the monoidal structure on `ModuleCat`,
19+
the universe level of the modules must be at least the universe level of the ring,
20+
so that we have a monoidal unit.
21+
For now, we simplify by insisting both universe levels are the same.
22+
23+
## Implementation notes
24+
25+
This file essentially mirrors `Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean`.
26+
-/
27+
28+
suppress_compilation
29+
30+
open CategoryTheory
31+
32+
universe v u
33+
34+
variable {R : Type u} [CommRing R] [Invertible (2 : R)]
35+
36+
namespace QuadraticModuleCat
37+
38+
open QuadraticForm
39+
40+
namespace instMonoidalCategory
41+
42+
/-- Auxiliary definition used to build `QuadraticModuleCat.instMonoidalCategory`. -/
43+
@[simps! form]
44+
noncomputable abbrev tensorObj (X Y : QuadraticModuleCat.{u} R) : QuadraticModuleCat.{u} R :=
45+
of (X.form.tmul Y.form)
46+
47+
/-- Auxiliary definition used to build `QuadraticModuleCat.instMonoidalCategory`.
48+
49+
We want this up front so that we can re-use it to define `whiskerLeft` and `whiskerRight`. -/
50+
noncomputable abbrev tensorHom {W X Y Z : QuadraticModuleCat.{u} R} (f : W ⟶ X) (g : Y ⟶ Z) :
51+
tensorObj W Y ⟶ tensorObj X Z :=
52+
⟨f.toIsometry.tmul g.toIsometry⟩
53+
54+
/-- Auxiliary definition used to build `QuadraticModuleCat.instMonoidalCategory`. -/
55+
noncomputable abbrev associator (X Y Z : QuadraticModuleCat.{u} R) :
56+
tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z) :=
57+
ofIso (tensorAssoc X.form Y.form Z.form)
58+
59+
open MonoidalCategory
60+
61+
theorem forget₂_map_associator_hom (X Y Z : QuadraticModuleCat.{u} R) :
62+
(forget₂ (QuadraticModuleCat R) (ModuleCat R)).map (associator X Y Z).hom =
63+
(α_ X.toModuleCat Y.toModuleCat Z.toModuleCat).hom := rfl
64+
65+
theorem forget₂_map_associator_inv (X Y Z : QuadraticModuleCat.{u} R) :
66+
(forget₂ (QuadraticModuleCat R) (ModuleCat R)).map (associator X Y Z).inv =
67+
(α_ X.toModuleCat Y.toModuleCat Z.toModuleCat).inv := rfl
68+
69+
end instMonoidalCategory
70+
71+
open instMonoidalCategory
72+
73+
set_option maxHeartbeats 400000 in
74+
noncomputable instance instMonoidalCategory : MonoidalCategory (QuadraticModuleCat.{u} R) :=
75+
Monoidal.induced
76+
(forget₂ (QuadraticModuleCat R) (ModuleCat R))
77+
{ tensorObj := instMonoidalCategory.tensorObj
78+
μIsoSymm := fun X Y => Iso.refl _
79+
whiskerLeft := fun X _ _ f => tensorHom (𝟙 _) f
80+
whiskerRight := @fun X₁ X₂ (f : X₁ ⟶ X₂) Y => tensorHom f (𝟙 _)
81+
tensorHom := tensorHom
82+
tensorUnit' := of (sq (R := R))
83+
εIsoSymm := Iso.refl _
84+
associator := associator
85+
associator_eq := fun X Y Z => by
86+
dsimp only [forget₂_obj, forget₂_map_associator_hom]
87+
simp only [eqToIso_refl, Iso.refl_trans, Iso.refl_symm, Iso.trans_hom, tensorIso_hom,
88+
Iso.refl_hom, MonoidalCategory.tensor_id]
89+
erw [Category.id_comp, Category.comp_id, MonoidalCategory.tensor_id, Category.comp_id]
90+
rfl
91+
leftUnitor := fun X => ofIso (tensorLId X.form)
92+
rightUnitor := fun X => ofIso (tensorRId X.form) }
93+
94+
variable (R) in
95+
/-- `forget₂ (QuadraticModuleCat R) (ModuleCat R)` as a monoidal functor. -/
96+
def toModuleCatMonoidalFunctor : MonoidalFunctor (QuadraticModuleCat.{u} R) (ModuleCat.{u} R) :=
97+
Monoidal.fromInduced (forget₂ (QuadraticModuleCat R) (ModuleCat R)) _
98+
99+
instance : Faithful (toModuleCatMonoidalFunctor R).toFunctor :=
100+
forget₂_faithful _ _
101+
102+
end QuadraticModuleCat

‎Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Symmetric.lean‎

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
/-
2+
Copyright (c) 2023 Eric Wieser. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Eric Wieser
5+
-/
6+
import Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
7+
import Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
8+
9+
/-!
10+
# The monoidal structure on `QuadraticModuleCat` is symmetric.
11+
12+
In this file we show:
13+
14+
* `QuadraticModuleCat.instSymmetricCategory : SymmetricCategory (QuadraticModuleCat.{u} R)`
15+
16+
## Implementation notes
17+
18+
This file essentially mirrors `Mathlib/Algebra/Category/AlgebraCat/Symmetric.lean`.
19+
-/
20+
21+
suppress_compilation
22+
23+
open CategoryTheory
24+
25+
universe v u
26+
27+
variable {R : Type u} [CommRing R] [Invertible (2 : R)]
28+
29+
namespace QuadraticModuleCat
30+
31+
open QuadraticForm
32+
33+
instance : BraidedCategory (QuadraticModuleCat.{u} R) :=
34+
braidedCategoryOfFaithful (toModuleCatMonoidalFunctor R)
35+
(fun X Y => ofIso <| tensorComm X.form Y.form)
36+
(by aesop_cat)
37+
38+
variable (R) in
39+
/-- `forget₂ (QuadraticModuleCat R) (ModuleCat R)` as a braided functor. -/
40+
@[simps toMonoidalFunctor]
41+
def toModuleCatBraidedFunctor : BraidedFunctor (QuadraticModuleCat.{u} R) (ModuleCat.{u} R) where
42+
toMonoidalFunctor := toModuleCatMonoidalFunctor R
43+
44+
instance : Faithful (toModuleCatBraidedFunctor R).toFunctor :=
45+
forget₂_faithful _ _
46+
47+
instance instSymmetricCategory : SymmetricCategory (QuadraticModuleCat.{u} R) :=
48+
symmetricCategoryOfFaithful (toModuleCatBraidedFunctor R)
49+
50+
end QuadraticModuleCat

‎Mathlib/LinearAlgebra/QuadraticForm/TensorProduct/Isometries.lean‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -92,6 +92,7 @@ theorem tmul_tensorComm_apply
9292
FunLike.congr_fun (tmul_comp_tensorComm Q₁ Q₂) x
9393

9494
/-- `TensorProduct.comm` preserves tensor products of quadratic forms. -/
95+
@[simps toLinearEquiv]
9596
def tensorComm (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) :
9697
(Q₁.tmul Q₂).IsometryEquiv (Q₂.tmul Q₁) where
9798
toLinearEquiv := TensorProduct.comm R M₁ M₂
@@ -129,6 +130,7 @@ theorem tmul_tensorAssoc_apply
129130
FunLike.congr_fun (tmul_comp_tensorAssoc Q₁ Q₂ Q₃) x
130131

131132
/-- `TensorProduct.assoc` preserves tensor products of quadratic forms. -/
133+
@[simps toLinearEquiv]
132134
def tensorAssoc (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (Q₃ : QuadraticForm R M₃) :
133135
((Q₁.tmul Q₂).tmul Q₃).IsometryEquiv (Q₁.tmul (Q₂.tmul Q₃)) where
134136
toLinearEquiv := TensorProduct.assoc R M₁ M₂ M₃
@@ -166,6 +168,7 @@ theorem tmul_tensorRId_apply
166168
FunLike.congr_fun (comp_tensorRId_eq Q₁) x
167169

168170
/-- `TensorProduct.rid` preserves tensor products of quadratic forms. -/
171+
@[simps toLinearEquiv]
169172
def tensorRId (Q₁ : QuadraticForm R M₁):
170173
(Q₁.tmul (sq (R := R))).IsometryEquiv Q₁ where
171174
toLinearEquiv := TensorProduct.rid R M₁
@@ -199,6 +202,7 @@ theorem tmul_tensorLId_apply
199202
FunLike.congr_fun (comp_tensorLId_eq Q₂) x
200203

201204
/-- `TensorProduct.lid` preserves tensor products of quadratic forms. -/
205+
@[simps toLinearEquiv]
202206
def tensorLId (Q₂ : QuadraticForm R M₂):
203207
((sq (R := R)).tmul Q₂).IsometryEquiv Q₂ where
204208
toLinearEquiv := TensorProduct.lid R M₂

0 commit comments

Comments
 (0)